Функция рекурсивного лямбда-исчисления

Question

Я хотел бы создать функцию лямбда-исчисления P, что (P x y z) дает ((x y)(x P)(P z)), Я пытался использовать варианты Y-комбинатор / Тьюринга комбинатор, то есть функции вида λ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)

QED

Answer 2

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

Вот Ω, самая маленькая не завершающая программа, которая хорошо показывает U-комбинатор.

((λ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