再帰ラムダ計算関数

Question

が((x y)(x P)(P z))というようなラムダ微積分関数Pを作成したいと思います。私はYコンビネータ/チューリングコンビネータの変種、すなわち形λg.(g g)の関数を使用しようとしました。なぜなら、関数自体を再現する必要があるからですが、私は前方を見ることができません。どんな助けでも大歓迎です。

Answer 1

を使用してのように見えるかもしれないものです"β-方程式" 01を解く。 式M = ... M ...の方程式を解く一般的な方法があります。 あなただけMのすべての出現がmによって置き換えられている用語L、形成、ラムダに右辺をラップ：固定小数点を使用して次に

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

をあなたの解決策を得るコンビネータ。あなたの例でそれを説明しましょう。

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

その後、YとLを展開P = Y Lは、我々が得る：

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) 

Q.E.D.を：

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は、私たちが何をしたいんかどうかをチェックしてみましょう

Answer 2

U-combinatorは、自己参照ラムダ抽象化を作成するのに役立ちます。

ここで、Ωは、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