I'm dev

https://i-m.dev

《计算模型导引》（2019）课后习题答案（三）：λ-演算

发表于 分类于

个人答案，仅供参考。

查看全部

页面含有超多数学公式，打开后需要等待很长时间才能彻底完成渲染和排版，尤其是移动设备。

3.1 证明括号引理：对于任何M∈Λ，在M中出现的左括号个数等于在M中出现的右括号个数。

证明：记l(M)表示M的左括号数目，r(M)为M的右括号数，以下即证l(M)=r(M)。

只需对M的结构做归纳：

  • M=x，l(M)=0=r(M)
  • M=(N1N2)，l(M)=1+l(N1)+l(N2)=1+r(N1)+r(N2)=r(M)
  • M=λx.N，l(M)=l(N)=r(N)=r(M)

3.2 试求SSSS的β-nf。

解： 为了使得λ-项与变量间能互相区分，下文约定可以对其添加下标作为记号，如λxiyizi.xizi(yizi)。

S1S2=β(λx1y1z1.x1z1(y1z1))S2=βλy1z1.S2z1(y1z1)=βλy1z1.((λx2y2z2.x2z2(y2z2))z1(y1z1))=βλy1z1.(λz2.z1z2(y1z1z2))=βλy1z1z2.z1z2(y1z1z2)

可记S=SS=λxyz.yz(xyz)，且S1S2S3S4=βS2S4(S3S4)，所以SSSS=βS(S)。

SSSS=βS1(S2)=β(λx1y1z1.y1z1(x1y1z1))S2=βλy1z1.y1z1(S2y1z1)=βλy1z1.y1z1((λx2y2z2.y2z2(x2y2z2))y1z1)=βλy1z1.y1z1(λz2.z1z2(y1z1z2))

所以SSSS=βλxy.xy(λz.yz(xyz))

3.3 证明：(λx.xxx)(λx.xxx)没有β-nf。

证明：简记t=λx.xxx。

tt≡α(λx.xxx)t=βttt≡α(λx.xxx)tt=βtttt=β⋯

其具有唯一的β归约分支：无穷β-化归链。

3.4 设F∈Λ呈形λx.M，证明：

（1）λz.Fz=βF

（2）λz.yz≠βy

注意，对于一般的F，λz.Fz≠βF，但λz.Fz=ηF。

证明： （1）λz.Fz≡λz.(λx.M)z=βλz.M[x:=z]≡αλx.M≡F⟹λz.Fz=βF

（2）反证法，假设λz.yz=βy，不妨取y,z∈∇，此时yz就不能进行归约，并且λz.yz∈β-nf,y∈β-nf，由命题3.14和定理3.20，

∃T∈Λ,y↠βT∨λz.yz↠βT⟹∃T∈Λ,y≡T∨λz.yz≡T⟹y≡λz.yz∵y∈∇∴λz.yz≡y∈∇

与λz.yz∉∇的事实矛盾。

3.5 证明二元不动点定理：对于任何F,G∈Λ，存在X,Y∈Λ，满足

FXY=X,GXY=Y.

证明： 存在组合子Y∈Λ∘可以使得∀M∈Λ,M(YM)=YM。

取Y=Y(GX)即可保证GXY=Y。

然后第一个公式可写为FX(Y(GX))=X，取X=Y(λx.Fx(Y(Gx)))即可。

3.6 证明：对任何M,N∈Λ∘，方程xN=Mx对于x有解。

证明： 取x=λr.R，其中R∈Λ∘，则xN≡(λr.R)N=βR

原命题转化为R=M(λr.R)有解，直接由不动点定理得，取R=Y(λs.M(λr.s))，其中Y∈Λ∘为不动点组合子。

并且Y,M∈Λ∘，所以R∈Λ∘验证通过。

因此，x=λt.Y(λs.M(λr.s))便是方程解。

3.7 证明：对于任意的P,Q∈Λ，若P↠βQ，则存在n≥0以及P0,⋯,Pn∈Λ，满足

（1）P≡P0，

（2）Q≡Pn，

（3）对任何i<n，Pi→βPi+1。

证明：↠β是→β的自反和传递闭包，即↠β=⋃k=0∞(→β)k，其中k=0时表示自反的情况。

数学归纳法证明之：

  • 当k=0时，显然取P≡P0≡Q，原命题成立

  • 若已知P(→β)kQ，原命题成立，对P(→β)k+1Q的情况进行分析

    必然存在（不必唯一）一个中间项M使得P(→β)kM→βQ

    又因为存在P≡P0→β⋯→βPk≡M，显然取Pk+1≡M可使P≡P0→β⋯→βPk→βPk+1≡Q成立

综上，原命题得证。

3.8 证明：对于任意P,Q∈Λ，若P↠βQ，则λz.P↠βλz.Q。

证明： 由题3.7，存在归约链P≡P0→β⋯→βPn≡Q

由于→β是合拍闭包的，因此有λz.P≡λz.P0→β⋯→βλz.Pn≡λz.Q，因此λz.P↠βλz.Q

3.9 证明：对于任意P,Q∈Λ，若P=βQ，则存在n∈N以及P0,⋯,Pn∈Λ，满足

（1）P≡P0，

（2）Q≡Pn，

（3）对任何i<n，Pi→βPi+1或Pi+1→βP1。

证明：=β是→β的自反、传递和对称闭包，即(=β)=⋃k=0∞(→β∨←β)k。

与题3.7类似完成证明，唯一不同在于该“链条”有允许两个方向。

3.10 证明定理3.12：

对于任何M,N∈Λ，M=βN⟺λβ⊢M=N

证明：二元关系β≡{((λx.M)N,M[x:=N]):M,N∈Λ∧x∈∇}，=β是β的合拍、自反、对称和传递闭包。

=β有且只有以下几种形式：

（记号约定L,M,N∈Λ,x∈∇）

(β′)二元关系定义(λx.M)N=βM[x:=N](ρ′)自反闭包M=βM(σ′)对称闭包N=βM⇒M=βN(τ′)传递闭包M=βL∧L=βN⇒M=βN(μ′)合拍闭包-1M=βN⇒LM=βLN(ν′)合拍闭包-2M=βN⇒ML=βNL(ξ′)合拍闭包-3M=βN⇒λx.M=βλx.N

显而易见，上述=β的形式∗′与形式理论λβ中的公理或者规则∗互相等价，如β⟺β′,rho⟺ρ′,⋯，既无遗漏也无多余。

因此M=βN⟺λβ⊢M=N。

3.11 证明定理3.13：

对于任何M,N∈Λ，M=βηN⟺λβη⊢M=N

证明：同题3.10，=βη是β∪η的合拍、自反、对称和传递闭包，因此类似地，再引入一条表现形式：

(η′)二元关系定义λx.Mx=βηM

且有η′⟺η，即该条转换形式与λβη形式理论中的公理η等价，同理原命题亦得证。

3.12 证明：对于任何的M,n∈Λ，若M=βN，则存在T使M↠βT且N↠βT。这就是对于=β的CR性质。

证明：已知，↠β具有CR性质

利用题3.9中的结论，即M=βN时有M(→β∨←β)kN，对其长度k应用数学归纳法：

  • 当k=0，即M≡N，由自反性M↠βM,M↠βN，则存在T∈Λ使M↠βT且N↠βT。

  • 若k=i时结论成立，试验证k=i+1时结论成立，即考虑M(→β∨←β)kL(→β∨←β)N的情况

    故存在T′使得M↠βT′,L↠βT′

    • 若L→βN，即L↠βN,L↠βT′，故存在T″使得N↠βT″,T′↠βT″，进而N↠βT″,M↠βT″
    • 若L←βN，利用↠β的传递性，M↠βT′,N↠βT′

综上，原命题成立。

3.13 证明：若在系统λβ中加入下述公理

(A)λxy.x=λxy.y,

则对任何的M,N∈Λ,λβ+(A)⊢M=N。

证明：

∀M,N∈Λλxy.x=λxy.y⟹(λxy.x)MN=(λxy.y)MN⟹M=N∴∀M,N∈Λ,λβ+(A)⊢M=N

3.14 证明命题3.14：

设R是Λ上的一个二元关系，M∈NFR，则

（1）不存在N∈Λ使得M→RN

（2）M↠βN⟹M≡N

证明：（1）反证法，假设存在N∈Λ使得M→RN，即(M,N)∈R，与M∈NFR矛盾

（2）反证法，因为↠β=⋃k=0∞(→β)k，假设M≢N，即排除k=0的情况，则存在项L使得M→βL，同样也导致矛盾

3.15 证明引理3.16：

若M⊳mcdM′且N⊳mcdN′，则MN⊳mcdM′N′

证明：M⊳mcdM′，所以有M通过依次收缩M1,M2,⋯,Mm可以得到M′，

同理N通过依次收缩N1,N2,⋯,Nn可以得到N′。

构造收缩过程M1,M2,⋯,Mm,N1,N2,⋯,Nn，显然其可以将MN归约到M′N′，以下要证明这个过程是一个mcd

  • ∀1≤i≤j≤m，由M⊳mcdM′可知Mi⊅Mj
  • ∀1≤i≤j≤n，由N⊳mcdN′可知Ni⊅Nj
  • ∀1≤i≤m,1≤j≤n，Mi⊅Nj因为二者来自不同的λ-项

所以，MN⊳mcdM′N′。

3.16 试找出A∈Λ∘使A λ-定义函数f(x,y)=x+y

解：取A=λwxyz.wy(xyz)即可

A⌜m⌝⌜n⌝≡(λwxyz.wy(xyz))⌜m⌝⌜n⌝=βλyz.⌜m⌝y(⌜n⌝yz)≡λyz.ym(ynz)≡λyz.ym+nz≡⌜m+n⌝

3.17 试找出F∈Λ∘使F λ-定义函数f(x)=3x

解：取F=λxyz.xy(xy(xyz))即可

F⌜n⌝≡(λxyz.xy(xy(xyz)))⌜n⌝=βλyz.⌜n⌝y(⌜n⌝y(⌜n⌝yz))≡λyz.yn(yn(ynz))≡λyz.y3nz≡⌜3n⌝

3.18 令D≡λxyz.z(Ky)x，证明：对于任意的X,Y∈Λ，

DXY⌜0⌝=X,DXY⌜n+1⌝=Y.

这里，K≡λxy.x,⌜n⌝≡λfx.fnx。

证明：容易证明第一个等式成立，

DXY⌜0⌝=β⌜0⌝(KY)X=βX

接下来证明第二个等式，

DXY⌜n+1⌝=β⌜n+1⌝(KY)X=β(KY)n+1X=βKY((KY)nX)=βY

3.19 设Exp≡λxy.yx，证明：对于任意的n∈N和m∈N∗，

Exp⌜n⌝⌜m⌝=β⌜nm⌝

证明：先代入并归约，

Exp⌜n⌝⌜m⌝≡(λab.ba)⌜n⌝⌜m⌝=β⌜m⌝⌜n⌝≡(λfx.fmx)⌜n⌝=βλx.⌜n⌝mx≡λx.(λyz.ynz)mx

数学归纳法：

  • m=1时，Exp⌜n⌝⌜1⌝=βλx.(λyz.ynz)x=βλx.λz.xnz≡λxz.xnz≡⌜n⌝

  • 若假设有Exp⌜n⌝⌜m⌝=β⌜nm⌝即(λyz.ynz)mx=βλz.xnmz

    (λyz.ynz)m+1x≡(λyz.ynz)((λyz.ynz)mx)=β(λyz.ynz)(λw.xnmw)=βλz.(λw.xnmw)nz=βλz.xn×nmz≡λz.xnm+1z∴Exp⌜n⌝⌜m+1⌝=βλx.λz.xnm+1z≡λxz.xnm+1z≡⌜nm+1⌝

综上，原命题得证。

3.20 构造F∈Λ∘使得对于任何n∈N，

F⌜n⌝=β⌜2n⌝

解：亦即寻找F∈Λ∘ λ-定义2n，由题3.19，取F≡λx.Exp⌜2⌝x=βλx.x⌜2⌝即可。

3.21 设f,g:N→N,f=Itw[g]，即

f(0)=0f(n+1)=g(f(n))

且G∈Λ∘ λ-定义函数g，试求F∈Λ∘使得F λ-定义函数f。

解： 亦即寻找F使F⌜n⌝=β⌜gn(0)⌝成立

F⌜n⌝=β⌜gn(0)⌝≡⌜g(gn−1(0))⌝=βG⌜gn−1(0)⌝=β⋯=βGn⌜0⌝≡⌜n⌝G⌜0⌝

所以，取F≡λx.xG⌜0⌝即可。

3.22 证明引理3.39：

存在一般递归函数var,app,abs,num:N→N使得：

  1. ∀n∈N,var(n)=♯(v(n))
  2. ∀M,N∈Λ,app(♯M,♯N)=♯(M,N)
  3. ∀x∈∇,M∈Λ,abs(♯x,♯M)=♯(λx.M)
  4. ∀n∈N,num(n)=♯⌜n⌝

证明：

  1. var(n)=[0,n]∈GRF

  2. app(♯M,♯N)=[1,[♯M,♯N]]⟹app(m.n)=[1,[m,n]]∈GRF

  3. abs(♯x,♯M)=[2,[♯x,♯M]]⟹abs(x,m)=[2,[x,m]]∈GRF

  4. ♯(fnx)=[1,[♯f,♯fn−1x]]]=⋯=[1,[♯f,[1,[♯f,⋯[1,[♯f,♯x]]⋯]]]]∈GRF

    ⌜n⌝=λfx.fnx=λf.λx.fnx，可得num(n)=♯⌜n⌝=[2,[f,[2,[x,♯(fnx)]]]]∈GRF

3.23 设f(n)为习题1.16中定义的函数，试构造F∈Λ∘使F⌜n⌝=⌜f(n)⌝对n∈N+成立。

（该函数定义如下）

f(0)=0,f(1)=1,f(2)=22,f(3)=333,⋯f(n)=n⋰n⏟n个n,

解：先定义原始递归函数h(x,y)如下：

h(x,0)=N2(x)h(x,y+1)=xh(x,y)

然后构造H∈Λ∘ λ-定义了h(x,y)

{H⌜x⌝⌜0⌝=βD⌜x⌝⌜0⌝⌜1⌝H⌜x⌝⌜y+1⌝=β⌜xh(x,y)⌝=βExp⌜x⌝(H⌜x⌝⌜y⌝)⟹H⌜x⌝⌜y⌝=βD⌜y⌝(D⌜x⌝⌜0⌝⌜1⌝)(Exp⌜x⌝(H⌜x⌝(pred⌜y⌝)))∴H≡Y(λzxy.D⌜y⌝(D⌜x⌝⌜0⌝⌜1⌝)(Exp⌜x⌝(z⌜x⌝(pred⌜y⌝))))

（其中，Y定义见定理3.23，pred定义见引理3.31，D的定义参考引理3.33，Exp定义见题3.19）

又∀n∈N+,f(n)=h(n,n)，所以应该使F⌜n⌝=βH⌜n⌝⌜n⌝⟹F=λw.Hww

综上，

F≡λw.Y(λzxy.D⌜y⌝(D⌜x⌝⌜0⌝⌜1⌝)(Exp⌜x⌝(z⌜x⌝(pred⌜y⌝))))ww

3.24 构造H∈Λ∘，使得对于任意n∈N,x1,⋯,xn∈Λ，有

H⌜n⌝x1⋯xn=βλz.zx1⋯xn

解：等价于构造Hn=H⌜n⌝=βλx1⋯xnz.zx1⋯xn

h(n)=♯Hn=[2,[♯x1,⋯(♯(zx1⋯xn))⋯]]=[2,[♯x1,⋯,⋯[1,[♯xn−1,♯xn]]⋯,⋯]]

显然h(n)的可以通过递归与复合的方式计算，当然也就是说h∈RF，故存在G使得G⌜n⌝=β⌜h(n)⌝=β⌜♯Hn⌝≡⌜Hn⌝

由定理3.41，存在枚举子E∈Λ∘使得∀Hn∈Λ∘,E⌜Hn⌝=βHn

所以取H≡λx.E(Gx)即可。验证之，H⌜n⌝=βE(G⌜n⌝)=βE(⌜Hn⌝)=βHn，满足条件。

3.25 证明：存在Θ2∈Λ∘，使得对于任意F∈Λ∘有

Θ2⌜F⌝=βF⌜Θ2⌜F⌝⌝

证明：由定理3.41，已知存在枚举子E∈Λ∘，使得对于任何M∈Λ∘，有E⌜M⌝=βM。

因此，构造A≡λxy.Ey(⌜xxy⌝),Θ2≡AA即可，以下验证之，

Θ2⌜F⌝≡AA⌜F⌝=βE⌜F⌝(⌜AA⌜F⌝⌝)=βF(⌜AA⌜F⌝⌝)=βF(⌜Θ2⌜F⌝⌝)

验证通过，总是存在Θ2≡(λxy.Ey(⌜xxy⌝))(λxy.Ey(⌜xxy⌝))符合条件。