Рекурсивная функция лямбда-исчисления

Question

Я хотел бы создать функцию лямбда-исчисления P такую, что дает ((x y)(x P)(P z)). Я пробовал использовать варианты комбинатора Y-combinator/Turing, то есть функции формы λg.(g g), так как мне нужно воспроизвести эту функцию, но я не вижу никакого выхода вперед. Любая помощь будет принята с благодарностью.

Answer 1

В основном вы хотите для решения «β-уравнения» P x y z = (x y) (x P) (P z). Существует общий метод решения уравнений вида M = ... M .... Вы просто обернуть правую в лямбда, образуя термин L, где все вхождения M заменяются m:

L = λm. ... m ... 

Затем, используя комбинатор неподвижной точки вы получите ваше решение. Позвольте мне проиллюстрировать это на вашем примере.

L = λp. (λxyz. (x y) (x p) (p z)), 
    where λxyz. is a shorthand for λx. λy. λz. 

Затем P = Y L, разворачивая Y и L мы получаем:

P = (λf. (λg. f (g g)) (λg. f (g g))) (λp. (λxyz. (x y) (x p) (p z))) 
    ->β 
(λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) 
// the previous line is our "unfolded" P 

Давайте проверим, если P делает то, что мы хотим:

P x y z 
    = // unfolding definition of P 
(λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) x y z 
    ->β 
((λp. (λxyz. (x y) (x p) (p z))) ((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)))) x y z 
    ->β 
(λxyz. (x y) (x ((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)))) (((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g))) z)) x y z 
    ->β 
(x y) (x ((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)))) (((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g))) z) 
    = // folding 1st occurrence of P 
(x y) (x P) (((λg. (λp. (λxyz. (x y) (x p) (p z))) (g g)) (λg. (λp. (λxyz. (x y) (x p) (p z))) (g g))) z) 
    = // folding 2nd occurrence of P 
(x y) (x P) (P z) 

что и требовалось доказать

Answer 2

U-combinator должен помочь вам создать самореферентную абстракцию лямбда.

Здесь Ω, самая маленькая программа без конца, которая хорошо проявляет U-combinator.

((λf. (f f)) 
(λf. (f f))) 

Если вы можете дать ему имя

Ω := λf.(f f) 

Вот что это может выглядеть с абстракцией

((λP. (P P x y z)) 
(λP. λx. λy. λz. ((x y) (x P) (P z)))) 

или с помощью Ом

λx. λy. λz. Ω (λP. λx. λy. λz. ((x y) (x P) (P z))) x y z