essential of Lambda

essential of Lambda是《Lambda-Calculus and Combinators : An Introduction》的摘要版本昼激，提供了lambda部分的內(nèi)容摘要，實(shí)現(xiàn)了一個(gè)lambda解釋器對(duì)例題進(jìn)行自動(dòng)解答抬旺，最后描述不可判定性刹孔。

解釋器github地址：https://github.com/wangdxh/essential-of-Lambda

1A lambda定義
1B 替換 substitution
- 范圍scope的定義
- 自由變量和綁定變量
- 修改綁定變量
- Substitution
1C β歸約 β-reduction
β相等
3B 不動(dòng)點(diǎn)理論
丘奇數(shù) Church Numerals
遞歸 Y組合子的應(yīng)用
不可判定性 undecidable
- 羅素悖論
- 哥德?tīng)枖?shù)
- 丘奇數(shù)
- closed under conversion
- Scott–Curry undecidability theorem

1A lambda定義

假設(shè)給出了

1.一個(gè)無(wú)限的變量（variables）表達(dá)式序列：v0,v00,v000,v0000,...瑞侮；
2.還有一個(gè)不同于變量的原子常量（atomic constants）表達(dá)式序列收擦，可能是有限的鞋既，無(wú)限的力九，或者空（如果該序列是空的，那么系統(tǒng)叫做pure邑闺，不為空叫做applied）跌前；
那么λ-terms的表達(dá)式集合遞歸地定義如下：

a. 所有的變量和原子常量都是λ-terms(叫做atoms)
b. 如果M和N是任何λ-terms，那么 (MN) 是一個(gè)λ-term陡舅，叫做application
c. 如果M是任何λ-term抵乓，并且x是任何變量，那么 (λx.M) 是一個(gè)λ-term蹭沛，叫做abstraction

舉例：
(λv0.(v0 v00))是λ-term
如果x,y,z是互相不同的變量臂寝，那么如下都是λ-terms

(λx.xy)
(x(λx.(λx.x)))
((λy.y)(λx.(xy)))
(λx.(yz))

在2中有兩個(gè)λx在一個(gè)term中，定義中允許摊灭，實(shí)際過(guò)程中不鼓勵(lì)這樣使用咆贬；4展示了無(wú)意義的抽象：(λx.M)格式，x并沒(méi)有在M中出現(xiàn)帚呼，對(duì)任何的輸入掏缎，函數(shù)返回相同結(jié)果。

application應(yīng)用相當(dāng)于函數(shù)調(diào)用煤杀，M是調(diào)用函數(shù)眷蜈，N是參數(shù)
abstraction抽象 (λx.M)相當(dāng)于函數(shù)定義，x是參數(shù)沈自，M是函數(shù)體酌儒；當(dāng)抽象被調(diào)用時(shí)指的是將M內(nèi)的x替換成參數(shù)，(λx.M)N 指將M內(nèi)的x替換成N
(λx.x(xy))N = N(Ny)
(λx.y)N = y

‘λ’字符本身不是一個(gè)term枯途，‘λx’也不是一個(gè)term忌怎。
在本文中大寫字母M，N等代表任意的λ-terms酪夷；字母x,y,z,u,v,w代表變量榴啸，默認(rèn)不同的字母表示不同的變量。

兩側(cè)括號(hào)有時(shí)可以省略晚岭，例如：MNPQ指的是(((MN)P)Q), 使用左關(guān)聯(lián)
其他縮寫如下：
λx.PQ ---> (λx.(PQ))
λxyz.M ---> (λx.(λy.(λz.M)))

≡符號(hào)表示語(yǔ)法格式上的相等 Syntactic identity鸥印，指的是語(yǔ)句格式相同
M ≡ N指的是M是和N精確地相同，
如果MN ≡ PQ，那么M ≡ P库说，N ≡ Q
如果λx.M ≡ λy.P狂鞋，那么x ≡ y，M ≡ P
默認(rèn)假設(shè)：變量和常量是不同的璃弄，應(yīng)用和抽象是不同的要销，其句法格式不同。這種假設(shè)在任何語(yǔ)言定義的時(shí)候都是成立的夏块，將來(lái)不會(huì)明確聲明疏咐。
P ≡ M N1 N2 ... Nk(k>=0) 當(dāng)k==0時(shí)，指的是 P ≡ M
T有格式：λx1 x2 ... xn.PQ (n>=0) 當(dāng)n==0時(shí)脐供，指的是T有格式 PQ
Iff指的是if and only if

對(duì)λ-terms補(bǔ)齊括號(hào)和‘λ’浑塞，λ在程序中使用^進(jìn)行代替
java -jar ./lambda-1.0-SNAPSHOT.jar fullformat d:\github\essential-Lambda\fullformat.txt

abcdef
  ->  (((((ab)c)d)e)f)
xyz(yx)
  ->  (((xy)z)(yx))
(^u.vuu)zy
  ->  (((^u.((vu)u))z)y)
^x.uxy
  ->  (^x.((ux)y))
ux(yz)(^v.vy)
  ->  (((ux)(yz))(^v.(vy)))
^u.u(^x.y)
  ->  (^u.(u(^x.y)))
(^xyz.xz(yz))uvw
  ->  ((((^x.(^y.(^z.((xz)(yz)))))u)v)w)
(^xy.xyy)(^u.uyx)  ->  ((^x.(^y.((xy)y)))(^u.((uy)x)))

1B 替換 substitution

對(duì)于λ-terms P和Q，出現(xiàn)關(guān)系(occur)指的是P出現(xiàn)在Q中政己，或者P是Q的一個(gè)subterm酌壕，或者Q包含(contains)P，遞歸地定義如下：

P出現(xiàn)在P中
如果P出現(xiàn)在M歇由，或者N中葵硕，那么P出現(xiàn)在(MN)中
如果P出現(xiàn)在M中挑辆，或者P ≡ x，那么P出現(xiàn)在(λx.M)中
例如((xy)(λx.(xy))) xy出現(xiàn)了2次，x出現(xiàn)了3次

范圍scope的定義

對(duì)于一個(gè)特定的λx.M出現(xiàn)在P中寒瓦，那么出現(xiàn)的M叫做其左邊的λx的范圍鹤盒。
類似函數(shù)定義時(shí)參數(shù)的作用范圍孩饼，參數(shù)作用的范圍是函數(shù)體
P ≡ (λy.yx(λx.y(λy.z)x))vw
最左邊的λy的范圍是yx(λx.y(λy.z)x)愿阐；λx的范圍是y(λy.z)x；左右的λy的范圍是z

自由變量和綁定變量

變量x在P中的一次出現(xiàn)被叫做：
bound綁定的回挽，如果它出現(xiàn)在P中的一個(gè)λx的范圍內(nèi)
bound and binding 綁定的且正在綁定没咙，當(dāng)前僅當(dāng)x指的是λx中的x，即參數(shù)
free自由的千劈，如果其他情況

如果x在P中至少有一次binding正在綁定形式的出現(xiàn)祭刚，那么x叫做P的一個(gè)綁定變量 bound variable；如果x在P中至少有一次自由形式的出現(xiàn)墙牌，那么x叫做P的一個(gè)自由變量 free varibale
P中自由變量的集合簡(jiǎn)寫為：FV(P)
一個(gè)閉項(xiàng)closed term指的是沒(méi)有任何自由變量的term袁梗。

考慮如下term：
xv(λyz.yv)w 全括號(hào)形式如下：
(((xv)(λy.(λz.(yv))))w)
最左邊的x，v是自由的憔古，最左邊的y是綁定且正在綁定的，z也是一樣淋袖，最右邊的y是綁定的鸿市，但不是正在綁定，v和w是自由的

P ≡ (λy.yx(λx.y(λy.z)x))vw
所有的四個(gè)y是bound綁定的，最左邊和最右邊的y也是binding的焰情，最左邊的x是自由的陌凳，中間的x是bound and binding的，最右邊的x是綁定的bound内舟，不是binding的合敦，所以P中的自由變量的集合是FV(P)={x,z,v,w}。
在P中x即使自由的验游，也是綁定的充岛。

獲取λterm的自由變量
java -jar ./lambda-1.0-SNAPSHOT.jar freevariables d:\github\essential-Lambda\freevariables.txt

abcdef
  ->  {a,b,c,d,e,f}
xyz(yx)
  ->  {x,y,z}
(^u.vuu)zy
  ->  {v,z,y}
^x.uxy
  ->  {u,y}
ux(yz)(^v.vy)
  ->  {u,x,y,z}
^u.u(^x.y)
  ->  {y}
(^xyz.xz(yz))uvw
  ->  {u,v,w}

修改綁定變量

Change of bound variables, congruence
P包含λx.M的一個(gè)出現(xiàn)，y不屬于FV(M)
那么替換λx.M為λy.[y/x]M叫做 α-conversion in P 或者 P的改變綁定變量

P ≡α Q 或者P α-converts to Q：
當(dāng)且僅當(dāng)P可以經(jīng)過(guò)有限的或者空的α轉(zhuǎn)換序列變成Q
λxy.x(xy) ≡ λx.(λy.x(xy))
≡α λx.(λv.x(xv))
≡α λu.(λv.u(uv))
≡ λuv.u(uv)

如果P ≡α Q耕蝉，那么 FV(P) = FV(Q)
≡α 關(guān)系是反射崔梗，傳遞和對(duì)稱的
P ≡α P
P ≡α Q，Q ≡α R 那么 P ≡α R
P ≡α Q 那么 Q ≡α P
事實(shí)上多數(shù)的作品里面≡的意思就是≡α垒在，本書后續(xù)章節(jié)即為這種意義

Substitution

對(duì)于任何M蒜魄，N，x场躯，定義[N/x]M為替換M中的所有以自由形式出現(xiàn)的x為N谈为，并且為了避免沖突改變bound綁定變量，后的結(jié)果
遞歸的定義如下：

[N/x]x ≡ N
[N/x]a ≡ a                 對(duì)于所有的原子a 不等于≡ x
[N/x](PQ) ≡ ([N/x]P [N/x]Q)
[N/x](λx.P) ≡ (λx.P)       P中的如果出現(xiàn)x踢关，也會(huì)是綁定的伞鲫，不是自由的
[N/x](λy.P) ≡ (λy.P)        x不屬于 FV(P)
[N/x](λy.P) ≡ (λy.[N/x]P) x屬于FV(P)并且y不屬于FV(N)
[N/x](λy.P) ≡ (λz.[N/x][z/y]P)  x屬于FV(P)并且y屬于FV(N)

其中x 不等于≡ y，z是不屬于FV(NP)的第一個(gè)變量

考慮 [w/x](λw.x)耘成，λw.x表示的是常量函數(shù)榔昔，返回的是x的值；所以[w/x](λw.x) 替換后的結(jié)果應(yīng)該是一個(gè)常量函數(shù)瘪菌，返回w的值撒会；如果直接替換x為w得到的是λw.w，返回的是恒等式师妙，輸入w诵肛，返回w；根據(jù)最后一條規(guī)則來(lái)計(jì)算： N為w默穴， y為w怔檩，N ≡ w ≡ y ，y屬于FV(N)
[w/x](λw.x) ≡ λz.[w/x][z/w]x
≡ λz.[w/x]x
≡ λz.w

引理：
對(duì)于任意的term M蓄诽，N薛训，變量x
[x/x]M ≡ M
x 不屬于FV(M)，那么[N/x]M ≡ M
x 屬于FV(M)仑氛，那么FV([N/x]M) = FV(N) ∪ (FV(M) - {x})

一個(gè)自動(dòng)替換的程序
java -jar ./lambda-1.0-SNAPSHOT.jar subst d:\github\essential-Lambda\subst.txt

[(uv)/x](^y.x(^w.vwx))
apply(^x.(^y.x(^w.vwx)))->(uv)
to:(^y.(uv)(^w.vw(uv)))

[(^y.xy)/x] (^y.x(^x.x))
apply(^x.(^y.x(^x.x)))->(^y.xy)
to:(^y.(^y.xy)(^x.x))

[(^y.vy)/x] (y(^v.xv))
apply(^x.(y(^v.xv)))->(^y.vy)
to:(y(^a.(^y.vy)a))

[(uv)/x](^x.zy)
apply(^x.(^x.zy))->(uv)
to:(^x.zy)

[(^z.zwvy)/x] (^y.yx(^y.xvy))y
apply(^x.(^y.yx(^y.xvy))y)->(^z.zwvy)
to:(^a.a(^z.zwvy)(^b.(^z.zwvy)vb))y

[(^z.zwvy)/x] (^y.yx(^x.xvy))y
apply(^x.(^y.yx(^x.xvy))y)->(^z.zwvy)
to:(^a.a(^z.zwvy)(^x.xva))y

[(^z.zwvy)/x] (^x.xv(^y.xvy))y
apply(^x.(^x.xv(^y.xvy))y)->(^z.zwvy)
to:(^x.xv(^y.xvy))y

[(^z.zwvy)/x] (^x.xv(^x.xvy))y
apply(^x.(^x.xv(^x.xvy))y)->(^z.zwvy)
to:(^x.xv(^x.xvy))y

1C β歸約 β-reduction

(λx.M)N 表示的是一個(gè)函數(shù)(λx.M)調(diào)用乙埃，參數(shù)是N闸英，

β-contracting,β-reducing
任何 (λx.M)N 形式的term叫做β-redex并且對(duì)應(yīng)的 [N/x]M 叫做它的contractum。
β-redex看著像是β-reduce和index結(jié)合體介袜，一個(gè)可以做β轉(zhuǎn)換的索引

當(dāng)且僅當(dāng)P包含一個(gè) (λx.M)N 的出現(xiàn)甫何，并且替換這個(gè)出現(xiàn)為 [N/x]M，得到P'遇伞，
我們稱為 P β-contracts to P' 或者 P ?1β P′  P經(jīng)過(guò)一次β 轉(zhuǎn)換得到P'

當(dāng)且僅當(dāng)P經(jīng)過(guò)一系列有限的或者空的β轉(zhuǎn)換和改變綁定變量得到Q辙喂，我們成為P β歸約到Q 記為：P ?β Q

β相等

當(dāng)且僅當(dāng)P經(jīng)過(guò)一系列有限的（可能為空）β轉(zhuǎn)換或者反向β轉(zhuǎn)換，或者改變綁定變量得到Q鸠珠，我們稱：P是β-equal 或者β-convertible to Q巍耗，標(biāo)記為 P =β Q

(? i ≤ n?1)(Pi ?1β Pi+1 或者 Pi+1 ?1β Pi 或者 Pi ≡α Pi+1),P0 ≡ P, Pn ≡ Q.
舉例：
Pi到Pi+1 正向變化為Pi ?1β Pi+1
Pi到Pi+1 反向變化為Pi+1 ?1β Pi
P0 ≡(λy.yv)z，P1 ≡ zv跳芳，P2 ≡(λx.x)zv
(λy.yv)z ?β zv 正向
(λx.x)zv ?β zv 反向
(λy.yv)z =β (λx.x)zv

P經(jīng)過(guò)一次β變化得到Q 記為 P ?1β Q
P經(jīng)過(guò)一系列 β變化得到Q 記為 P ?β Q
P經(jīng)過(guò)一系列β變化或者反向β變化得到Q 記為 P =β Q

β歸約的例子：
java -jar ./lambda-1.0-SNAPSHOT.jar d:\github\essential-Lambda\reduce.txt

expresson reduce:(^x.xy)(^u.vuu)
(^x.xy)(^u.vuu)
(^u.vuu)y
vyy
expresson reduce:(^xy.yx)uv
(^x.(^y.yx))uv
(^y.yu)v
vu
expresson reduce:(^x.x(x(yz))x)(^u.uv)
(^x.x(x(yz))x)(^u.uv)
(^u.uv)((^u.uv)(yz))(^u.uv)
((^u.uv)(yz))v(^u.uv)
((yz)v)v(^u.uv)
expresson reduce:(^x.xxy)(^y.yz)
(^x.xxy)(^y.yz)
(^y.yz)(^y.yz)y
(^y.yz)zy
zzy
expresson reduce:(^xy.xyy)(^u.uyx)
(^x.(^y.xyy))(^u.uyx)
(^a.(^u.uyx)aa)
(^a.ayxa)
expresson reduce:(^xyz.xz(yz))((^xy.yx)u)((^xy.yx)v)w
(^x.(^y.(^z.xz(yz))))((^x.(^y.yx))u)((^x.(^y.yx))v)w
(^y.(^z.((^x.(^y.yx))u)z(yz)))((^x.(^y.yx))v)w
(^z.((^x.(^y.yx))u)z(((^x.(^y.yx))v)z))w
((^x.(^y.yx))u)w(((^x.(^y.yx))v)w)
(^y.yu)w(((^x.(^y.yx))v)w)
wu(((^x.(^y.yx))v)w)
wu((^y.yv)w)
wu(wv)
expresson reduce:(^xyz.xzy)(^xy.x)
(^x.(^y.(^z.xzy)))(^x.(^y.x))
(^y.(^z.(^x.(^y.x))zy))
(^y.(^z.(^y.z)y))
(^y.(^z.z))
expresson reduce:(^xy.x)(^x.x)
(^x.(^y.x))(^x.x)
(^y.(^x.x))

3B 不動(dòng)點(diǎn)理論

一個(gè)操作或者函數(shù)的不動(dòng)點(diǎn)指的是芍锦，將改不動(dòng)點(diǎn)作為參數(shù)進(jìn)行計(jì)算，得到的結(jié)果沒(méi)有改變飞盆。例如對(duì)于x的平方函數(shù)娄琉，0和1就是不動(dòng)點(diǎn)，0和1的平方也還是0和1吓歇，2就不是不動(dòng)點(diǎn)孽水。
combinator組合子，簡(jiǎn)單地講城看，組合子就是指不包含自由變量的λ-term女气。

the fixed-point theorem
在lambda內(nèi)存在，一個(gè)組合子Y测柠，Yx =β x(YX); 更近一步 Yx ?β x(Yx)

阿蘭圖靈Y組合子：
Y ≡ UU, U ≡ λux.x(uux)
Curry-Ros Y組合子：
Y ≡ λx.V V, V ≡ λy.x(yy)
其他組合子：
Y0≡WS(BWB)
Y1≡WI(B(SI)(WI))
組合子驗(yàn)證：對(duì)各個(gè)組合子進(jìn)行驗(yàn)證炼鞠，執(zhí)行Yx，然后得到多次執(zhí)行后的結(jié)果轰胁，從結(jié)果中分析出Yx ?β x(Yx) ?β x(x(Yx)) ?β ....
為了避免名稱沖突谒主，對(duì)各個(gè)Y組合字給了不同的名字，分別為：Y赃阀，A霎肯，E，F(xiàn) 榛斯，如下所示：

I = (^x.x)
K = (^xy.x)
S = (^xyz.xz(yz))
B = (^xyz.x(yz))
B' = (^xyz.y(xz))
C = (^xyz.xzy)
W = (^xy.xyy)

U= (^ux.x(uux))
Y=UU
Yx

V = (^y.x(yy))
A = (^x.VV)
Ax

E = WS(BWB)
E
Ex

F = WI(B(SI)(WI))
F
Fx

java -jar ./lambda-1.0-SNAPSHOT.jar d:\github\essential-Lambda\ycombinator.txt
因?yàn)閅x可以無(wú)限執(zhí)行下去观游，需要把函數(shù)doreduce(String input)的循環(huán)歸約次數(shù)修改為40，默認(rèn)執(zhí)行300次歸約驮俗。

Y和A的結(jié)果比較容易看出來(lái)懂缕，后面兩個(gè)組合字需要?dú)w約的次數(shù)多一些才能看到結(jié)果，E和F的歸約篇幅比較長(zhǎng)王凑，就不展示了

expresson reduce:Yx
(^u.(^x.x(uux)))(^u.(^x.x(uux)))x
(^x.x((^u.(^x.x(uux)))(^u.(^x.x(uux)))x))x
x((^u.(^x.x(uux)))(^u.(^x.x(uux)))x)
x((^x.x((^u.(^x.x(uux)))(^u.(^x.x(uux)))x))x)
x(x((^u.(^x.x(uux)))(^u.(^x.x(uux)))x))
x(x((^x.x((^u.(^x.x(uux)))(^u.(^x.x(uux)))x))x))
x(x(x((^u.(^x.x(uux)))(^u.(^x.x(uux)))x)))
x(x(x((^x.x((^u.(^x.x(uux)))(^u.(^x.x(uux)))x))x)))
expresson reduce:Ax
(^x.(^y.x(yy))(^y.x(yy)))x
(^y.x(yy))(^y.x(yy))
x((^y.x(yy))(^y.x(yy)))
x(x((^y.x(yy))(^y.x(yy))))
x(x(x((^y.x(yy))(^y.x(yy)))))
x(x(x(x((^y.x(yy))(^y.x(yy))))))
x(x(x(x(x((^y.x(yy))(^y.x(yy)))))))
x(x(x(x(x(x((^y.x(yy))(^y.x(yy))))))))
x(x(x(x(x(x(x((^y.x(yy))(^y.x(yy)))))))))

后面會(huì)有Y組合字的應(yīng)用實(shí)例

丘奇數(shù) Church Numerals

對(duì)于任何一個(gè)自然數(shù) n提佣，Church Numerals是一個(gè)λ-term吮蛹， $\overline{n}$ 表示 λxy.xⁿy
xⁿy 應(yīng)為右關(guān)聯(lián)的，即x³y為x(x(xy))拌屏，如果寫為xxxy在計(jì)算時(shí)，結(jié)果不正確术荤。

0,1,3, 4定義如下倚喂，
Z = (^xy.y) # 0 zero
O = (^xy.xy) # 1 one
T = (^xy.(x(x(xy)))) # 3 Three
F = (^xy.(x(x(x(xy))))) # 4 Four

加法：P = (^mnxy.mx(nxy))
PTF 3加4結(jié)果應(yīng)該為7

加一：Q = (^uxy.x(uxy))
QF 4加1 結(jié)果為5

減一：A = (^nxy.n(^gh.h(gx))(^u.y)(^u.u))
AZ 0減一還是0
AO

條件表達(dá)式：如果z為church 0，返回x瓣戚，否則返回y
K = (^xy.x)
D = (^xyz.z(Ky)x)
DXYZ = X
DXYO = Y
DXYT = Y

java -jar ./lambda-1.0-SNAPSHOT.jar d:\github\essential-Lambda\church.txt
用戶可以補(bǔ)充其他的乘法和減法端圈，進(jìn)入church.txt，然后通過(guò)程序進(jìn)行結(jié)果驗(yàn)證

結(jié)果計(jì)算如下：

expresson reduce:PTF
(^m.(^n.(^x.(^y.mx(nxy)))))(^x.(^y.(x(x(xy)))))(^x.(^y.(x(x(x(xy))))))
(^n.(^x.(^y.(^x.(^y.(x(x(xy)))))x(nxy))))(^x.(^y.(x(x(x(xy))))))
(^x.(^y.(^x.(^y.(x(x(xy)))))x((^x.(^y.(x(x(x(xy))))))xy)))
(^x.(^y.(^y.(x(x(xy))))((^x.(^y.(x(x(x(xy))))))xy)))
(^x.(^y.(x(x(x((^x.(^y.(x(x(x(xy))))))xy))))))
(^x.(^y.(x(x(x((^y.(x(x(x(xy)))))y))))))
(^x.(^y.(x(x(x(x(x(x(xy)))))))))
expresson reduce:QF
(^u.(^x.(^y.x(uxy))))(^x.(^y.(x(x(x(xy))))))
(^x.(^y.x((^x.(^y.(x(x(x(xy))))))xy)))
(^x.(^y.x((^y.(x(x(x(xy)))))y)))
(^x.(^y.x(x(x(x(xy))))))
expresson reduce:AZ
(^n.(^x.(^y.n(^g.(^h.h(gx)))(^u.y)(^u.u))))(^x.(^y.y))
(^x.(^y.(^x.(^y.y))(^g.(^h.h(gx)))(^u.y)(^u.u)))
(^x.(^y.(^y.y)(^u.y)(^u.u)))
(^x.(^y.(^u.y)(^u.u)))
(^x.(^y.y))
expresson reduce:AO
(^n.(^x.(^y.n(^g.(^h.h(gx)))(^u.y)(^u.u))))(^x.(^y.xy))
(^x.(^y.(^x.(^y.xy))(^g.(^h.h(gx)))(^u.y)(^u.u)))
(^x.(^y.(^y.(^g.(^h.h(gx)))y)(^u.y)(^u.u)))
(^x.(^y.(^g.(^h.h(gx)))(^u.y)(^u.u)))
(^x.(^y.(^h.h((^u.y)x))(^u.u)))
(^x.(^y.(^u.u)((^u.y)x)))
(^x.(^y.((^u.y)x)))
(^x.(^y.y))
expresson reduce:DXYZ
(^x.(^y.(^z.z((^x.(^y.x))y)x)))XY(^x.(^y.y))
(^y.(^z.z((^x.(^y.x))y)X))Y(^x.(^y.y))
(^z.z((^x.(^y.x))Y)X)(^x.(^y.y))
(^x.(^y.y))((^x.(^y.x))Y)X
(^y.y)X
X
expresson reduce:DXYO
(^x.(^y.(^z.z((^x.(^y.x))y)x)))XY(^x.(^y.xy))
(^y.(^z.z((^x.(^y.x))y)X))Y(^x.(^y.xy))
(^z.z((^x.(^y.x))Y)X)(^x.(^y.xy))
(^x.(^y.xy))((^x.(^y.x))Y)X
(^y.((^x.(^y.x))Y)y)X
((^x.(^y.x))Y)X
(^y.Y)X
Y
expresson reduce:DXYT
(^x.(^y.(^z.z((^x.(^y.x))y)x)))XY(^x.(^y.(x(x(xy)))))
(^y.(^z.z((^x.(^y.x))y)X))Y(^x.(^y.(x(x(xy)))))
(^z.z((^x.(^y.x))Y)X)(^x.(^y.(x(x(xy)))))
(^x.(^y.(x(x(xy)))))((^x.(^y.x))Y)X
(^y.(((^x.(^y.x))Y)(((^x.(^y.x))Y)(((^x.(^y.x))Y)y))))X
(((^x.(^y.x))Y)(((^x.(^y.x))Y)(((^x.(^y.x))Y)X)))
((^y.Y)(((^x.(^y.x))Y)(((^x.(^y.x))Y)X)))
Y

遞歸 Y組合子的應(yīng)用

遞歸表達(dá)式：

Rxyz = Dx(yz(Rxy(Az)))z.

A是減一子库，D是條件表達(dá)式舱权，z是church n ，如果z等于0仑嗅，返回x宴倍，如果z不等于0，返回yz(Rxy(Az))仓技，對(duì)y進(jìn)行調(diào)用鸵贬，參數(shù)是z 和 Rxy(Az)。
舉例：如果y是加法脖捻，x等于church 0阔逼，z是church n，Rxyz返回的是z + z-1 + z-2 + z-3 ... + 0

根據(jù)Yx = x(Yx) 可以得到當(dāng)對(duì)Y調(diào)用x的時(shí)候地沮，返回x(Yx)嗜浮，即應(yīng)用(Yx)到x上，如果x是一個(gè)多參數(shù)的函數(shù)（大于一個(gè)參數(shù)）摩疑，那么Yx調(diào)用執(zhí)行后x(Yx)危融，傳遞給x的第一個(gè)參數(shù)(Yx)繼續(xù)代表最開(kāi)始的Yx調(diào)用本身。簡(jiǎn)單例子如下：

X = (λf. λn. n==0 ? 1 : n*(f n-1))
(YX)4
-> Y (λf. λn. n==0 ? 1 : n*(f n-1))  4
-> X(YX)4 兩個(gè)參數(shù)：代入X未荒，f = (YX)专挪，n = 4
-> 4 * ((YX) 3)
...
-> 4 * 3 * 2 * 1 * ((YX 0))

對(duì)R應(yīng)用Yx，得到如下：

Rxyz = Dx(yz(Rxy(Az)))z.
R' = Y(^uxyz.Dx(yz(uxy(Az)))z)

R有三個(gè)參數(shù)片排，應(yīng)該再增加一個(gè)參數(shù)u寨腔，放在第一個(gè)位置，代表R本身即(Yx),將R內(nèi)的R替換成u率寡，即可迫卢。
Y(^uxyz.Dx(yz(uxy(Az)))z)ZPF，xyz賦值為 church 0冶共，加法乾蛤，church 4每界，計(jì)算的結(jié)果應(yīng)該是4+3+2+1+0=10

java -jar ./lambda-1.0-SNAPSHOT.jar d:\github\essential-Lambda\yapply.txt

expresson reduce:Y(^uxyz.Dx(yz(uxy(Az)))z)ZPF
(^x.(^y.x(yy))(^y.x(yy)))(^u.(^x.(^y.(^z.(^x.(^y.(^z.z((^x.(^y.x))y)x)))x(yz(uxy((^n.(^x.(^y.n(^g.(^h.h(gx)))(^u.y)(^u.u))))z)))z))))(^x.(^y.y))(^m.(^n.(^x.(^y.mx(nxy)))))(^x.(^y.(x(x(x(xy))))))
(^y.(^u.(^x.(^y.(^z.(^x.(^y.(^z.z((^x.(^y.x))y)x)))x(yz(uxy((^n.(^x.(^y.n(^g.(^h.h(gx)))(^u.y)(^u.u))))z)))z))))(yy))(^y.(^u.(^x.(^y.(^z.(^x.(^y.(^z.z((^x.(^y.x))y)x)))x(yz(uxy((^n.(^x.(^y.n(^g.(^h.h(gx)))(^u.y)(^u.u))))z)))z))))(yy))(^x.(^y.y))(^m.(^n.(^x.(^y.mx(nxy)))))(^x.(^y.(x(x(x(xy))))))
.........
.........
(^x.(^y.(x(x(x(x(x(x(x(x(x(x((^x.(^y.y))xy)))))))))))))
(^x.(^y.(x(x(x(x(x(x(x(x(x(x((^y.y)y)))))))))))))
(^x.(^y.(x(x(x(x(x(x(x(x(x(xy))))))))))))

不可判定性 undecidable

羅素悖論

羅素悖論指的是由羅素發(fā)現(xiàn)的一個(gè)集合論悖論。設(shè)集合S是由一切不屬于自身的集合所組成家卖，即“S={x|x ? x}”眨层。那么問(wèn)題是：S包含于S是否成立？首先上荡，若S包含于S趴樱，則不符合x?x，則S不包含于S酪捡；其次叁征，若S不包含于S，則符合x?x逛薇，S包含于S捺疼。

要證明不可判定性，就要在被判定的語(yǔ)句中形成一條羅素悖論永罚，這條語(yǔ)句否定了它本身的被判定的結(jié)果啤呼。假設(shè)判定過(guò)程為F，判定語(yǔ)句為J：

J = 如果F(J)為真尤蛮，那么我返回假媳友；F(J)為假，我返回真

這樣一條語(yǔ)句产捞，就形成了羅素悖論醇锚，如果F(J)返回為真，判定J為真坯临，但是J本身又推導(dǎo)出自己為假焊唬；如果F(J)返回為假，判定J為假看靠，J又推導(dǎo)出自己為真赶促。從而形成不可判定。

哥德?tīng)枖?shù)

但是J語(yǔ)句本身是無(wú)法表示的挟炬，因?yàn)橛肍去判定J的時(shí)候鸥滨，又引用到了F對(duì)J的判定結(jié)果，會(huì)形成死循環(huán)谤祖，導(dǎo)致無(wú)法結(jié)束婿滓。所以引入自然數(shù)，作為載體粥喜，將語(yǔ)句編碼成自然數(shù)凸主，然后F判定的時(shí)候輸入自然數(shù)，然后解碼為原來(lái)的語(yǔ)句额湘，再進(jìn)行判定卿吐。

自然數(shù)可以表示從0到無(wú)窮大旁舰，總有一個(gè)自然數(shù)表示的是J的編碼，再或者可以通過(guò)數(shù)的加減乘除得到J的自然數(shù)編碼嗡官，至少提供了一個(gè)構(gòu)造的方向箭窜。這個(gè)編碼的過(guò)程最早由哥德?tīng)栆耄Z(yǔ)句編碼出的數(shù)衍腥，稱為哥德?tīng)枖?shù)绽快。使用gd(X)表示對(duì)X語(yǔ)句進(jìn)行哥德?tīng)柧幋a得到的自然數(shù)。

哥德?tīng)枖?shù)通過(guò)對(duì)字符分配一個(gè)素?cái)?shù)紧阔，比如 (λx.y)，分別給'(', 'λ', 'x', '.', 'y', ')' 這六個(gè)符號(hào)分配2,3,5,7,11,13续担，(λx.y)語(yǔ)句得到的數(shù)值就是235711*13擅耽，然后對(duì)這個(gè)數(shù)值進(jìn)行素?cái)?shù)分解，得到的素?cái)?shù)列表轉(zhuǎn)換成字符列表就是原始的語(yǔ)句物遇。

丘奇數(shù)

自然數(shù)在lambda語(yǔ)義中乖仇，可以使用丘奇數(shù)來(lái)表達(dá)，所以除了語(yǔ)句和哥德?tīng)枖?shù)之前的轉(zhuǎn)換之外询兴，在lambda語(yǔ)義中乃沙，哥德?tīng)枖?shù)（自然數(shù)）要轉(zhuǎn)為丘奇數(shù)進(jìn)行表示。

n的church number 表示為 $\small \overline{n}$ 诗舰，指的是自然數(shù)n在lambda中表示為函數(shù)形式警儒。例如5表示為(λxy.x(x(x(x(xy)))))

將語(yǔ)句編碼為哥德?tīng)枖?shù)的時(shí)候，存在兩個(gè)關(guān)于自然數(shù)的函數(shù)：

$\small \tau(gd(X), gd(Y)) = gd((XY))$
輸入的是兩個(gè)自然數(shù)眶根，對(duì)自然數(shù)進(jìn)行哥德?tīng)柗淳幋a蜀铲，得到語(yǔ)句，對(duì)兩個(gè)語(yǔ)句執(zhí)行apply属百，得到一個(gè)新的語(yǔ)句记劝，然后進(jìn)行哥德?tīng)柧幋a得到對(duì)應(yīng)的新語(yǔ)句的自然數(shù)。

$\small \nu(n) = gd(\overline{n})$
輸入自然數(shù)族扰，首先將改自然數(shù)轉(zhuǎn)換成丘奇數(shù)厌丑，得到數(shù)的函數(shù)表達(dá)語(yǔ)句，然后對(duì)該語(yǔ)句再進(jìn)行哥德?tīng)柧幋a渔呵，得到對(duì)應(yīng)的自然數(shù)怒竿。

因?yàn)樽匀粩?shù)在lambda中使用丘奇數(shù)的函數(shù)形式表示，引入一個(gè)方便的符號(hào)表達(dá)： $\small \lceil \rceil$ 厘肮，對(duì)于λ-term X愧口，對(duì)應(yīng)的X的哥德?tīng)枖?shù)的丘奇數(shù)表示記為 $\small \lceil X \rceil$

$\small \lceil X \rceil ≡ \overline{gd(X)}$
即先對(duì)X語(yǔ)句求其哥德?tīng)柧幋a后的自然數(shù)，然后再將該自然數(shù)數(shù)值类茂，轉(zhuǎn)成丘奇數(shù)的函數(shù)形式耍属。

$\small \tau$ 和 $\small \nu$ 兩個(gè)關(guān)于自然數(shù)的函數(shù)托嚣，在lambda中分別表示為：

$\small T\lceil X \rceil\lceil Y \rceil =_{β} \lceil (XY) \rceil$
$\small N \overline{n} =_{β} \lceil \overline{n} \rceil$
函數(shù)的意義是一樣的，只是采用了lambda的丘奇數(shù)來(lái)表示自然數(shù)厚骗，將輸入和輸出的參數(shù)改變了表示方式示启。

closed under conversion

一對(duì)自然數(shù)的集合 $\small \mathcal{A，B}$ 被稱為recursively separable领舰，當(dāng)且僅當(dāng)有一個(gè)完全遞歸函數(shù) $\small \phi$ 夫嗓，輸出只有0和1：

$\small n \in \mathcal{A} \Longrightarrow \phi (n) = 0$
$\small n \in \mathcal{B} \Longrightarrow \phi (n) = 1$

一對(duì)包含λ-terms的集合，被稱為recursively separable冲秽，當(dāng)且僅當(dāng)對(duì)將集合內(nèi)的terms編碼成哥德?tīng)枖?shù)之和形成的兩個(gè)自然數(shù)的集合是recursively separable舍咖。

一個(gè)集合，包含自然數(shù)或者λ-terms锉桑，稱為recursive或者decidable排霉，當(dāng)且僅當(dāng)該集合和它的補(bǔ)給是recursively separable。

非正式地講民轴，如果一對(duì)集合 $\small \mathcal{A攻柠，B}$ 是recursively separable，當(dāng)且僅當(dāng) $\small \mathcal{A后裸，B}$ 的交集為空瑰钮，并且有一個(gè)算法能夠判定一個(gè)數(shù)字或者λ-term在 $\small \mathcal{A，}$ 內(nèi)微驶，還是 $\small \mathcal{B浪谴，}$ 內(nèi)。

在lambda內(nèi)祈搜，一個(gè)包含λ-terms的集合被稱為 closed under conversion较店，當(dāng)且僅當(dāng)對(duì)于所有的terms X，Y容燕，
$\small X \in \mathcal{A}梁呈，and，Y =_{β} X \Longrightarrow Y \in \mathcal{A}$

Scott–Curry undecidability theorem

For sets of terms in λ with =β: no pair of non-empty sets which are closed under conversion is recursively separable.

對(duì)于由 =β 形成的λ-terms的集合蘸秘，沒(méi)有一對(duì)非空的closed under conversion 集合官卡，是recursively separable。即存在一個(gè)λ-term無(wú)法判定他是屬于集合A還是集合B的醋虏。

針對(duì)自然數(shù)有：

$\small n \in \mathcal{A} \Longrightarrow \phi(n) = 0$
$\small n \in \mathcal{B} \Longrightarrow \phi(n) = 1$

讓集合 $\small \mathcal{A寻咒，B}$ 包含λ-terms，則：

$\small X \in \mathcal{A} \Longrightarrow \phi(gd(X)) = 0$
$\small Y \in \mathcal{B} \Longrightarrow \phi(gd(Y)) = 1$

在lambda中使用F來(lái)表示 $\small \phi$ 颈嚼，則

$\small X \in \mathcal{A} \Longrightarrow F(\lceil X\rceil) =_{β} \overline{0}$
$\small Y \in \mathcal{B} \Longrightarrow F(\lceil Y\rceil) =_{β} \overline{1}$

我們構(gòu)造一個(gè)悖論λ-term J毛秘，選擇任何一個(gè)term $\small A \in \mathcal{A}, B \in \mathcal{B}$

$\small 當(dāng) F(\lceil J\rceil) =_{β} \overline{0}時(shí)，J =_{β} B$
$\small 當(dāng) F(\lceil J\rceil) =_{β} \overline{1}時(shí)，J =_{β} A$

如果能構(gòu)造J 就證明了不可判定性叫挟。

J如下：

$\small J =_{β} DBA(F\lceil J\rceil)$

D是前面提到的條件組合子艰匙，

$\small DBA\overline{0} =_{β} B$
$\small DBA\overline{1} =_{β} A$

如何構(gòu)造J呢？y 不屬于 AB的自由變量的集合

$\small H≡λy.DBA(F(Ty(Ny)))$
$\small J≡H\lceil H\rceil$

T和N都是之前定義的：

$\small T\lceil X \rceil\lceil Y \rceil =_{β} \lceil (XY) \rceil$
$\small N\overline{n} =_{β} \lceil \overline{n} \rceil$

$\small J ≡ H\lceil H\rceil$
$\small =_{β} DBA(F(T\lceil H\rceil(N\lceil H\rceil)))$
$\small =_{β} DBA(F(T\lceil H\rceil\lceil\lceil H\rceil\rceil))$
$\small =_{β} DBA(F\lceil (H\lceil H\rceil)\rceil)$
$\small ≡DBA(F\lceil J\rceil)$

通過(guò) $\scriptsize H\lceil H\rceil$ 成功構(gòu)造J抹恳，H語(yǔ)句和它的哥德?tīng)枖?shù)是可以準(zhǔn)確計(jì)算的员凝，所以J可以成功得到，形成悖論奋献。

最后編輯于：2018.12.04 11:06:21

?著作權(quán)歸作者所有,轉(zhuǎn)載或內(nèi)容合作請(qǐng)聯(lián)系作者

人面猴
序言：七十年代末健霹，一起剝皮案震驚了整個(gè)濱河市，隨后出現(xiàn)的幾起案子瓶蚂，更是在濱河造成了極大的恐慌糖埋，老刑警劉巖，帶你破解...
沈念sama閱讀 206,214評(píng)論 6贊 481
死咒
序言：濱河連續(xù)發(fā)生了三起死亡事件窃这，死亡現(xiàn)場(chǎng)離奇詭異阶捆，居然都是意外死亡，警方通過(guò)查閱死者的電腦和手機(jī)钦听，發(fā)現(xiàn)死者居然都...
沈念sama閱讀 88,307評(píng)論 2贊 382
救了他兩次的神仙讓他今天三更去死
文/潘曉璐我一進(jìn)店門，熙熙樓的掌柜王于貴愁眉苦臉地迎上來(lái)倍奢，“玉大人朴上，你說(shuō)我怎么就攤上這事∽渖罚” “怎么了痪宰？”我有些...
開(kāi)封第一講書人閱讀 152,543評(píng)論 0贊 341
道士緝兇錄：失蹤的賣姜人
文/不壞的土叔我叫張陵，是天一觀的道長(zhǎng)畔裕。經(jīng)常有香客問(wèn)我衣撬，道長(zhǎng)，這世上最難降的妖魔是什么扮饶？我笑而不...
開(kāi)封第一講書人閱讀 55,221評(píng)論 1贊 279
?港島之戀（遺憾婚禮）
正文為了忘掉前任具练，我火速辦了婚禮，結(jié)果婚禮上甜无，老公的妹妹穿的比我還像新娘扛点。我一直安慰自己，他們只是感情好岂丘，可當(dāng)我...
茶點(diǎn)故事閱讀 64,224評(píng)論 5贊 371
惡毒庶女頂嫁案：這布局不是一般人想出來(lái)的
文/花漫我一把揭開(kāi)白布陵究。她就那樣靜靜地躺著，像睡著了一般奥帘。火紅的嫁衣襯著肌膚如雪铜邮。梳的紋絲不亂的頭發(fā)上，一...
開(kāi)封第一講書人閱讀 49,007評(píng)論 1贊 284
城市分裂傳說(shuō)
那天，我揣著相機(jī)與錄音松蒜，去河邊找鬼扔茅。笑死，一個(gè)胖子當(dāng)著我的面吹牛牍鞠，可吹牛的內(nèi)容都是我干的咖摹。我是一名探鬼主播，決...
沈念sama閱讀 38,313評(píng)論 3贊 399
雙鴛鴦連環(huán)套：你想象不到人心有多黑
文/蒼蘭香墨我猛地睜開(kāi)眼难述，長(zhǎng)吁一口氣：“原來(lái)是場(chǎng)噩夢(mèng)啊……” “哼萤晴！你這毒婦竟也來(lái)了？” 一聲冷哼從身側(cè)響起胁后，我...
開(kāi)封第一講書人閱讀 36,956評(píng)論 0贊 259
萬(wàn)榮殺人案實(shí)錄
序言：老撾萬(wàn)榮一對(duì)情侶失蹤店读，失蹤者是張志新（化名）和其女友劉穎，沒(méi)想到半個(gè)月后攀芯，有當(dāng)?shù)厝嗽跇?shù)林里發(fā)現(xiàn)了一具尸體屯断，經(jīng)...
沈念sama閱讀 43,441評(píng)論 1贊 300
?護(hù)林員之死
正文獨(dú)居荒郊野嶺守林人離奇死亡，尸身上長(zhǎng)有42處帶血的膿包…… 初始之章·張勛以下內(nèi)容為張勛視角年9月15日...
茶點(diǎn)故事閱讀 35,925評(píng)論 2贊 323
?白月光啟示錄
正文我和宋清朗相戀三年侣诺，在試婚紗的時(shí)候發(fā)現(xiàn)自己被綠了殖演。大學(xué)時(shí)的朋友給我發(fā)了我未婚夫和他白月光在一起吃飯的照片。...
茶點(diǎn)故事閱讀 38,018評(píng)論 1贊 333
活死人
序言：一個(gè)原本活蹦亂跳的男人離奇死亡年鸳，死狀恐怖趴久，靈堂內(nèi)的尸體忽然破棺而出，到底是詐尸還是另有隱情搔确，我是刑警寧澤彼棍，帶...
沈念sama閱讀 33,685評(píng)論 4贊 322
?日本核電站爆炸內(nèi)幕
正文年R本政府宣布，位于F島的核電站膳算，受9級(jí)特大地震影響座硕，放射性物質(zhì)發(fā)生泄漏。R本人自食惡果不足惜涕蜂，卻給世界環(huán)境...
茶點(diǎn)故事閱讀 39,234評(píng)論 3贊 307
男人毒藥：我在死后第九天來(lái)索命
文/蒙蒙一华匾、第九天我趴在偏房一處隱蔽的房頂上張望。院中可真熱鬧机隙，春花似錦瘦真、人聲如沸。這莊子的主人今日做“春日...
開(kāi)封第一講書人閱讀 30,240評(píng)論 0贊 19
一樁弒父案诸尽，背后竟有這般陰謀
文/蒼蘭香墨我抬頭看了看天上的太陽(yáng)。三九已至印颤，卻和暖如春您机，著一層夾襖步出監(jiān)牢的瞬間，已是汗流浹背。一陣腳步聲響...
開(kāi)封第一講書人閱讀 31,464評(píng)論 1贊 261
情欲美人皮
我被黑心中介騙來(lái)泰國(guó)打工际看，沒(méi)想到剛下飛機(jī)就差點(diǎn)兒被人妖公主榨干…… 1. 我叫王不留咸产，地道東北人。一個(gè)月前我還...
沈念sama閱讀 45,467評(píng)論 2贊 352
代替公主和親
正文我出身青樓仲闽，卻偏偏與公主長(zhǎng)得像脑溢，于是被迫代替她去往敵國(guó)和親。傳聞我的和親對(duì)象是個(gè)殘疾皇子赖欣，可洞房花燭夜當(dāng)晚...
茶點(diǎn)故事閱讀 42,762評(píng)論 2贊 345