January 3rd, 2010

Лямбда рекурсия

Задача: написать λ-терм для итерационного процесса g(n, f, x)

g(n, f, x) = f ( g(n-1, f, x) )
g(0, f, x) = x

Решение: построим следующую рекурсивную конструкцию

g = λ n f x . zero? n x ( g ( pred n ) f ( f x ) )

Если n=0, результатом будет x, иначе (n>0) вернется g(n-1, f, f(x)). Семантика верная, но из-за явной рекурсии такой терм не свернуть к нормальной форме: получим бесконечное число замен.

Введем терм S = λ M n f x . zero? n x ( M ( pred n ) f ( f x ) ). Очевидно, что g - неподвижная точка S.

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

Y = ( λ x y . y ( x x y ) )( λ x y . y ( x x y ) )

и это легко проверить:

Y M = Z Z M = (λ x y . y ( x x y ) ) Z M = M ( Z Z M ) = M ( Y M )

Всё! Можем писать ответ.

Ответ: g = Y S.

Замечание: Комбинаторы очень важны. Например в типизированном λ-исчислении нет комбинатора Тьюринга (нет нормальной формы и тип для него сразу не строится) и для полноты по Тьюрингу уже требуется дополнительная константа Yσ - комбинатор неподвижных точек типа σ. Своего рода "внешний" комбинатор :)

Литература:
  1. A short introduction to the Lambda Calculus. Achim Jung. 2004