Интернет магазин китайских планшетных компьютеров



Компьютеры - Лямбда-исчисление - Связь с рекурсивными функциями

23 января 2011


Оглавление:
1. Лямбда-исчисление
2. Чистое
3.
4. Каррирование
5. Связь с рекурсивными функциями
6. В языках программирования



Рекурсия - это определение функции через себя; на первый взгляд, лямбда-исчисление не позволяет этого, но это впечатление обманчиво. Например, рассмотрим рекурсивную функцию, вычисляющую факториал:

f = 1, if n = 0; else n × f.

В лямбда-исчислении, функция не может непосредственно ссылаться на себя. Тем не менее, функции может быть передан параметр, связанный с ней. Как правило, этот аргумент стоит на первом месте. Связав его с функцией, мы получаем новую, уже рекурсивную функцию. Для этого, аргумент, ссылающийся на себя, обязательно должен быть передан в тело функции.

g := λr. λn.)
f := g g

Это решает специфичную проблему вычисления факториала, но решение в общем виде также возможно. Получив лямбда-терм, представляющий тело рекурсивной функции или цикл, передав себя в качестве первого аргумента, комбинатор неподвижной точки возвратит необходимую рекурсивную функцию или цикл. Функции не нуждаются в явной передаче себя каждый раз. Т.к. существует несколько определений комбинаторов неподвижной точки. Самый простой из них:

Y = λg.)

В лямбда-исчислении, Y g - неподвижная точка g; продемонстрируем это:

Y g
λh.)) g
)
g)))
g.

Теперь, чтобы определить факториал, как рекурсивную функцию, мы можем просто написать g n, где n - число, для которого вычисляется факториал. Пусть n = 4, получаем:

   g 4
  ), if n>0)) 4
  ), if n>0)) 4
   1, if 4 = 0; and 4·), if 4>0
   4· 3)
   4·), if n>0) 3)
   4·), if 3>0)
   4· 2))
   4·), if n>0) 2))
   4·), if 2>0))
   4· 1)))
   4·), if n>0) 1)))
   4·), if 1>0)))
   4· 0))))
   4·), if n>0) 0))))
   4·), if 0>0))))
   4·)))
   24

Каждое определение рекурсивной функции может быть представлено как неподвижная точка соответствующей функции, следовательно, используя Y, каждое рекурсивное определение может быть выражено как лямбда-выражение. В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно.



Просмотров: 5068


<<< Логика Хоара
Машина Зенона >>>