?

Log in

No account? Create an account

Previous Entry | Next Entry

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

Задача: написать λ-терм для итерационного процесса 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

Comments

( 4 comments — Leave a comment )
xoposhiy
Jan. 21st, 2010 05:08 pm (UTC)
> Семантика верная, но из-за явной рекурсии такой терм не свернуть к нормальной форме: получим бесконечное число замен.

Сдается мне это не совсем так. Что мы получим зависит от порядка редукции. Если я ничего не путаю, с этим справится даже нормальный порядок.

Проблема не в редукции, а в том, что в лямбда синтаксисе нельзя дать лямбде имя. А как ее вызвать рекурсивно, если нет имени? Никак!

Edited at 2010-01-21 05:14 pm (UTC)
vitaly_kosenko
Jan. 22nd, 2010 03:51 am (UTC)
Имена реализуются за счет абстракций, на примере твоего or'а:
λtrue. λ.false. λa. λb. (a true (b true false) (λt. λf. t) (λt. λf. f)

Вот. Но если таким вот образом попытаться записать
g = λ n f x . zero? n x ( g ( pred n ) f ( f x ) )
то получится бесконечная строчка. Для того, чтобы это побороть нужно либо в редукцию вставить вычисления, либо искать неподвижную точку
xoposhiy
Jan. 21st, 2010 05:12 pm (UTC)
И кстати лямбда терм не соответствует исходному определению g(n, f, x) = f ( g(n-1, f, x) )

Edited at 2010-01-21 05:13 pm (UTC)
vitaly_kosenko
Jan. 22nd, 2010 03:53 am (UTC)
Где косяк?
( 4 comments — Leave a comment )