to mock a mockingbirdを読む(23)11章

Problem 35 twice removed

BとCが与えられて、C**,R**,F**,V**を見つけよ。
これらは以下の条件を満たす。

1
2
3
4
C** x y z1 z2 z3 = x y z1 z3 z2
R** x y z1 z2 z3 = x y z2 z3 z1
F** x y z1 z2 z3 = x y z3 z2 z1
V** x y z1 z2 z3 = x y z3 z1 z2

1
2
3
4
5
c** = b c*
r** = b r*
f** = b f*
v** = b v*
である。

Problem 36 Vireo Revisited

VireoはCardinalとFinchで表せることは前に見た。
今度はC*とTを用いてVireoを表せ

1
2
3
4
v x y z = z x y
T x z y = z x y
C* T x y z = z x y
よってV = C*T = BCTである

Queer Birds

ここからは、括弧とpermuteからなる鳥を見ていく
これらは全てBとTから導出できる

Problem 37 Queer Birds

もっとも重要なメンバーの鳥はqueer bird Qである。
これは以下の条件を満たす。

1
Q x y z = y (x z)

これはbluebird Bと、BとTから導ける別の鳥から簡単に導ける。
それは何の鳥で、またどうやって導けるか

1
2
3
4
Q x y z = y (x z)
B y x z = y (x z)
C B x y z = y (x z)
よってもう一つの鳥はCでQ = C Bである

研究(2)コンビネータを学ぶのに便利な一つの方法

コンビネータに型がつけられることは研究(1)で述べました。
これを利用することで、1ステップずつ確かめながら
コンビネータの変換を試すことができます。
以下のコードは等価な変換をしながらsコンビネータをb,c,wであらわしたものです。
コードはhaskellです。
まず最初にsコンビネータの定義をtestで定義します。
その後コンパイルしてghciで:t testとやることでtest :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3という型情報が得られます。
次に等価な変換を行うので型情報は変わらないので、test2を同じ型で定義してから
test2の実装を書いていきます。
test3以降も同様です。
もちろんこれは一つのやり方ではありますが、先にtest2を書いてからghciで型情報をtestとtest2とで比べてみるという方法でも良いです。
もしtest2の等価変換が間違っていたら型エラーとなってコンパイルできません。
test2では、dコンビネータ(b b)を使って括弧を外しています。
test3では、c*コンビネータ(プログラムではcs)を使って引数の順序を入れ替えています。
test4では、w***コンビネータ(プログラムではwsss)を使って二つのzを一つにまとめています。
test5で完成で、test4をイータ変換しています。

csやwsはonce removed,cssやwssはtwice removedなコンビネータです。
cssとcss’,wsssとwsss’は同じものです。
これらを作成するときにも上で述べた手法がもちろん使えます。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
b x y z = x (y z)
c x y z = x z y
cs = b c
css = b cs
css' x y z w u = x y z u w
w x y = x y y
ws = b w
wss = b ws
wsss = b wss
wsss' x y z w u = x y z w u u
-- S combinator
test :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
test x y z = x z ( y z)
test2 :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
test2 x y z = (b b) x z y z
test3 :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
test3 x y z = cs (b b) x y z z
test4 :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
test4 x y z = wsss cs (b b) x y z
test5 :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
test5 = wsss cs (b b)

to mock a mockingbirdを読む(22)11章

Problem 31 The Bird C*

C*はCardinal once removedと読む。
これは次の条件を満たす。

1
C*xyzw = x y w z

C*はCに似ているが、xをスキップするまでアクションが遅延する点で異なる。
C*をBとCを用いて表せ。

1
2
3
4
C* x y z w = x y w z
C (x y) z w = x y w z
B C x y z w = x y w z
よってC* = B Cである

Problem 32 The Bird R*

R*(Robin once removed)は以下の条件を満たす。

1
R* x y z w = x z w y

R*がBとCから導出できることを示せ
(つまりはBとTから導出できる)

1
2
3
4
R* x y z w = x z w y
C* x z y w = x z w y
C* C* x y z w = x z w y
よってR* = C* C*である

Problem 33 The Bird F*

F*(Finch once removed)は以下の条件を満たす。

1
F* x y z w = x w z y

F*をBとCから導出せよ

1
2
3
4
5
F* x y z w = x w z y
R* x y w z = x w z y
C* (R* x) y z w = x w z y
B C* R* x y z w = x w z y
よってF* = B C* R*である

Problem 34 The Bird V*

V*(Vireo once removed)は以下の条件を満たす。

1
V* x y z w = x w y z

本ではV* x y z w = x w z yとなっているが上記の間違いだと思われる。
なぜならこれだとV/はF/とまったく同じになってしまうから。

V* x y z w = x w y z
F* x z y w = x w y z
C* F* x y z w = x w y z
よってV* = C* F*である。

to mock a mockingbirdを読む(21)11章

Problem 27 Vireos

Vireoは以下の条件を満たす。

1
V x y z = z x y

VireoはRobinの逆のような働きをする鳥になる。
VireoもBとTを用いて表すことができ、
一つの方法はCardinalとFinchを使う。これを導け

1
2
3
4
V x y z = z x y
F y x z = z x y
C F x y z = z x y
よってV = CFである

Problem 28

VireoをFinchとRobinを用いて表すにはどうすればよいか。
これは3文字の式からなる

1
2
3
4
Problem 22より
Cx = RxR
よって前問の結果より
V = CF = RFR

Problem 29

FinchはCardinalとVireoから導出できるか

1
2
3
4
F x y z = z y x
V y x z = z y x
C V x y z = z y x
よってF = C Vである

Problem 29

RobinとKestrelを含む森にはIdentity birdがいることを示せ

1
2
3
4
任意の鳥Aについて
RAKx = KxA = x
よってRAKはidentity birdである
より具体的にはRRKやRKKなどがidentity birdになる

some relatives

cardinal,robin,finch,vireoなどは
全てBとTから導けるが、実際BとCからも導ける

to mock a mockingbirdを読む(20)11章

Problem 22 Two Useful Laws

以下の2つの有用な式を証明せよ

1
2
a. Cx = RxR
b. Cx = B(Tx)R

1
2
3
4
5
6
7
8
前問より再掲
C x y z = x z y
R y x z = x z y
R x R y z = x z y
よってC x = R x Rである

またC x = R x R = (BBT) x R
= B(Tx)R

Problem 23

CardinalはRobinから導出できた。
なら逆にRobinはCardinalから導出できるか。

1
2
3
4
R x y z = y z x
C y x z = y z x
C C x y z = y z x
よってR=CCである

Problem 24 Finches

Finch Fは以下の条件を満たす

1
F x y z = z y x

これを導くにはいくつかの方法がある。
finchはbluebird,robin,cardinalから簡単に導ける。
またbluebirdとcardinal,bluebirdとrobinからも。
finchを導け

1
2
3
4
5
6
7
8
9
F x y z = z y x
R x z y = z y x
C (R x) y z = z y x
B C R x y z = z y x

よってF = B C Rである
またF = B C (C C)
= B (RRR) R
である

Problem 25

Finchはthrushとeagleからも導ける。
どうやれば導けるか

1
2
3
4
5
6
7
8
F x y z = z y x
T x (z y)= z y x
T x (T y z) = z y x
E T x T y z = z y x
T T (E T x) y z = z y x
E T T E T x y z = z y x

よってF = E T T E Tである

Problem 26

これで、あなたはfinchを2通りに表せるようになった。
BとTを用いてこれらを2通りで表せ。
一方は他方より短くなる

1
2
3
4
5
6
7
F = BCR = B(B(T(BBT))(BBT))(BBT)
F = ETTET = B(BBB)TTET
= (BBB)(TT)ET
= B(B(TT))ET
= B(TT)(ET)
= B(TT)(B(BBB)T)
ETTET経由のほうが4文字短くなる

to mock a mockingbirdを読む(19)11章

Problem 19

bluebird B, thrush T,mockinbird Mが与えられたとき、
各鳥とcommuteである鳥を求めよ

1
2
3
4
5
6
7
Problem 2より各鳥xはM(BxM)が好きである。
M(BTM)を考えるとTはM(BTM)が好きなので
T(M(BTM))=M(BTM)
各鳥xについて
T(M(BTM))x=M(BTM)x
左辺はx(M(BTM))となり
M(BTM)は各鳥とcommuteである

bluebirdsとthrushes

bluebird Bとthrush Tから多くの種類のpermuting birdsが導ける。
BとTからCardinalが導けることはアロンゾ・チャーチ(Alonzo Church)が1941年に発見した。
チャーチは8文字からなる導出を行ったが、もっと短くできると思われる。

Problem 20 Robins

Robin Rは以下の条件を満たす。

1
R x y z = y z x

BとTを用いてこれを導出せよ

1
2
3
4
R x y z = y z x
T x (yz) = y z x
DTx y z = y z x
よってR = DT = BBTである

Problem 21 Robins and Cardinals

Robin単体を使ってCardinalを導くことができる。
これを示せ。
ボーナス問題:前問とあわせることでCardinalをBとTで表せる。
しかしその場合文字数が9文字になってしまう。
1文字縮めることが加能だがどうやるか

1
2
3
4
5
6
7
8
9
10
11
C x y z = x z y
R y x z = x z y
R x R y z = x z y
R R R x y z = x z y
よってC = RRRであるので
C = (BBT)(BBT)(BBT)

ボーナス問題
RRR = BBTRR = B(TR)R
= B(T(BBT))(BBT)
これがチャーチが発見した8文字の式になる

to mock a mockingbirdを読む(18)11章

Problem 16

コンビネータ論理で基本的な役割をもつ鳥にCardinalがいる
Cardinalは次の条件を満たす。

1
C x y z = x z y

Cardinalはpermuting birdsとして知られる重要な鳥のファミリーに属する。
簡単にいえば、permuting birdsがいれば順番の入れ替えができるようになる。

問い
CardinalとKestrelがいる森にはIdentity birdがいることを示せ

1
2
3
CKCx = KxC=x
CKKx = KxK=x
よってI=CKCあるいはI=CKKである

Problem 17

もっとも基本的なpermuting birdにthrushがいる。
thrushは以下の条件を満たす。

1
T x y = y x

CardinalとIdentity birdからthrushを導出せよ

1
2
CIxy = Iyx = yx
よってT = CIである

Problem 18

2つの鳥xとyがcommute(可換)であるとは以下の条件を満たすことを言う。

1
x y = y x

森にthrushがおり、森の各鳥はなんらかの鳥が好きであるとする。
すると少なくとも1つの鳥Aが各鳥とcommuteすることを示せ

1
2
3
4
5
6
Tはある鳥Aが好きなので
TA = A
TAx = Ax
またTの性質より
TAx = xA
よってAは各xとcommute

to mock a mockingbirdを読む(17)11章

Problem 13

Warbler Wはコンビネータ論理ではとても重要でスタンダードな鳥である。
Wは以下の条件を満たす。

1
W x y = x y y

LarkはLxy = x(yy)だったので違う鳥であり間違えないように。

問い
WarblerとKestrelがいる森にはmockingbirdがいることを示せ

1
2
3
IがいればWI=Ixx=xx=Mとなりmockingbirdがいることが示せる
ここでWKx=Kxx=xよりWKはIである
よってWI=W(WK)がmockingbirdとなる

Problem 14

WarblerとIdentity birdがいる森にはmockingbirdがいることを示せ

1
Problem13で見たようにM=WIである

Problem 15

WarblerとKestrelがいる森にIdentity birdがいることを示せ

1
Problem13で見たようにI=WKである

to mock a mockingbirdを読む(16)11章

Problem 10

becard B3は次の条件を満たす

1
B3 xyzw = x(y(zw))

B3をbluebirdか、bluebirdから導出した鳥を用いて表せ

1
2
3
4
B3 xyzw = x(y(zw))
これは
B x y (zw) = D1 B xyzw
よってB3 = D1 B = B(BB)B

Problem 11

dovekie D2は次の条件を満たす

1
D2 xyzwv = x(yz)(wv)

D2をbluebirdを用いて導出せよ

1
2
3
4
D2 xyzwv = x(yz)(wv)
これは
B (x(yz)) w v = B3 B x y z w v
=B(BB)BB=BB(BB)

Problem 12

bald eagle E^は次の条件を満たす

1
E^ x y1 y2 y3 z1 z2 z3 = x(y1 y2 y3)(z1 z2 z3)

bluebirdからbald eagleを導出せよ

1
2
3
4
5
6
E^ x y1 y2 y3 z1 z2 z3 = x(y1 y2 y3)(z1 z2 z3)
これは
E x (y1 y2 y3) z1 z2 z3
= EEx y1 y2 y3 z1 z2 z3
よって
E^ = EE = B(BBB)(B(BBB))

compositor

bluebird Bから導出できる鳥を
前回の記事と合わせて8つ導出した
これらは、compositorと呼ばれる。
コンビネータ論理に関して特に覚えておくべき鳥はbluebird Bとdove Dである。
(復習するとD=BBであった)

to mock a mockingbirdを読む(15)11章

Problem 5

bluebird Bの仲間で重要なものの一つにdoveがいる。
dove Dは次の条件を満たす

1
D x y z w = xy(zw)

DはBのみから導出できる。それはどうやるか

1
2
3
4
5
Dxyz=xy(zw)
これは
B(xy)zw=xy(zw)と同じ意味で
B(xy)zw=BBxyzwであるので
D=BBである

Problem 6

blackbird B1は次の条件を満たす。

1
B1 xyzw = x(yzw)

bluebirdがいる森にはblackbirdもいることを示せ。
これを示すのにDも使用してよい

1
2
3
4
5
B1 xyzw = x(yzw)
これは
Bx(yz)w = x(yzw)であるので
Bx(yz)w = DBxyzw
よってB1 = DB = BBBである

Problem 7

eagle Eは次の条件を満たす。

1
Exyzwv = xy(zwv)

EはBのみを用いて表現できるのだがそれはどうやるか

1
2
3
4
Exyzwv = xy(zwv)
これは
B1(xy)zwv=BB1xyzwv
よってE = B B1 = B(BBB)である

Problem 8

bunting B2は次の条件を満たす。

1
B2xyzwv=x(yzwv)

Bを用いてB2を表せ

1
2
3
4
B2xyzwv=x(yzwv)
これは
Bx(yzw)v = EBxyzwv
よってB2 = EB = B(BBB)B

Problem 9

dickcissel D1は次の条件を満たす

1
D1 xyzwv = xyz(wv)

Bを用いてD1を導出せよ

1
2
3
4
D1 xyzwv = xyz(wv)
これは
B(xyz)wv = B1Bxyzwv
D1 = B1B = BBBB = B(BB)