to mock a mockingbirdを読む(30)12章

Problem 16

MがTとSから導出できることを証明せよ

1
2
STがWarblerであったので
WT=STTがmockingbirdである

Exercise 1 modeled on Church’s derivation of W

a.BとTを用いて以下の条件を満たすG1を導出せよ

1
G1 x y z w v = xyv(zw)

b.G1とMを用いて以下の条件を満たすG2を導出せよ

1
G2 x y z w = xw(xw)(yz)

c.B,T,Iを用いて以下の条件部ぉ満たすI2を導出せよ

1
任意の鳥xについてI2x = x I I

d.任意の鳥xについてI2(Fx)=xであることを示せ。Fはfinchである

e.G2F(QI2)がwarblerであることを示せ。QはQueer birdである

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
a.G x y z w = x w (y z)であった
BG x y z w v =
G (x y) z w v = x y v(z w)
よってG2=BGである

b.G1 x y z w v = x y v (z w)
G2 x y z w = xw(xw)(yz)
=M2 x w (yz)
=G1 M2 x y z w v
よってG2 = G1 M2 = G1(BM)である

c.I2x = x I I
= T I (x I)
= T I (T I x)
=B(T I)(T I) x

よってI2 = B(T I)(T I)である。

d.I2 (F x) = F x I I
= I I x
= I x
= x
よって目的の式が成り立つ

e.
G2F(QI2) x y
= Fy(Fy)(Qi2x)
=(Qi2x)(Fy)y
=x(i2 (Fy))y
=x y y(前問の結果より)
よって題意を満たす

Exercise 2 the standard starling

B(B(BW)C)(BB)がstarlingであることを示せ

1
2
3
4
5
6
7
s x y z = x z ( y z)
s x y z = (b b) x z y z
s x y z = (b c) (b b) x y z z
s x y z = (b(b(b w))) (b c) (b b) x y z
s x y z = b(b(b w)c)(b b) x y z

よって与式はstarlingである

Exercise 3

phoenix Φは以下の条件を満たす。

1
Φx y z w = x (y w)(z w)

phoenixはコンビネータ論理ではスタンダードなものである。
phoenixをSとBから導出せよ

1
2
3
4
5
Φ x y z w = x (y w)(z w)
=B x y w (z w)
= B (B S) B x y z w

よってΦ=B(BS)Bである