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)

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

BLUEBIRDS

重要な鳥としてbluebirdがいる。
bluebird Bについては次が成り立つ。

1
2
3
Bxyz = x(yz)
完全に括弧を表示するとこうかいても同じ意味
(((Bx)y)z) = x(yz)

Problem 1

bluebirdが重要な理由の一つは
森にbluebirdがいると基本的な合成法則が成り立たなければならないから。
任意の鳥CとDについて、CとDを合成したEが存在する。
それはなぜか
注:もしEがCとDの合成なら、各鳥xについてEx=C(Dx)を意味する

1
2
3
Bをbluebirdとして
BCDを考えると
BCDx=C(Dx)となりBCDはCとDを合成した鳥になる

Problem 2

森にBとmockingbird Mがいるとする。
すると、合成法則がなりたつので、各鳥xは何らかの鳥が好きである。
B,M,xを用いてそのような鳥を表現することができるか

1
2
3
4
BxM(BxM)
=x(M(BxM))
=x(BxM)(BxM)
よってxは(BxM)(BxM)=M(BxM)が好きである

Problem 3

BとMが森にいるとき、egocentricな鳥はどのように書き下せるか

1
2
3
4
5
Mがある鳥Eを好きな時
ME=EまたME=EEでもあるのでE=EEよってEはegocentric
鳥xはM(BxM)を好きなのでxにMをとると
MはM(BMM)が好き
よって、M(BMM)はegocentric

Problem 4

森にB,M,K(kestrel)がいるとき
hopelessly egocentric birdを書き下せ

1
2
9章のproblem9より、kestrelが好きな鳥はhopelessly egocentric。
よってxにKをとってM(BKM)はhopelessly egocentric

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

11章では最初に省略記法についての話があります。
(xy)zwとxyzwと((xy)z)wはすべて同じ意味になります。
x(yz)wは(x(yz))wと同じですし
x(yzw)はx((yz)w)と同じです。

Exercises

次のケースで括弧を左結合として完全に表しなさい

1
2
3
4
5
6
7
8
9
10
11
12
13
14
a.xy(zwy)v = ?
b.(xyz)(wvx) = ?
c.xy(zwv)(xz) = ?
d.xy(zwv)xz = ? 注:cとは結果が異なる
e.x(y(zwv))xz = ?
f.次の式は正しいか間違っているか
xyz(AB) = (xyz)(AB)
g.A1=A2だとするとき、BA1=BA2だと結論してよいか
またA1B=A2Bだと結論してよいか
h.xy=zだと仮定する
どちらの結論が有効か
1. xyw = zw
2. wxy = wz
注:トリッキーかつ重要

Answer

1
2
3
4
5
6
7
8
9
10
11
12
a.((xy)((zw)y))v
b.((xcy)z)((wv)x)
c.((xy)((zw)v))(xz)
d.(((xy)((zw)v))x)z
e.((x(y((zw)v)))x)z
f.正しい。どちらも((xy)z)(AB)となる
g.どちらの結論も正しい
h.1が有効
コンビネータの計算は左端か括弧の左端から始まるので
1は(xy)w,2は(wx)yという風に計算がなされるので2は成り立たない
例えばwがw a b = b aという鳥(Tコンビネータ)だった場合
wxy=yxとなりxyという形ではなくなってしまう

研究(1)コンビネータの型と論理学の関係

コンビネータの型について

特殊なものを除いて、コンビネータには型をつけることができます。
そして、型付けられたコンビネータは論理学と深い関係があるのです。
型をつけられないコンビネータは、自己適用をするmockingbirdやLarkなどがそうです。
今回はこれらについては触れません。
ここでは、haskellというプログラミング言語を用いて調査します。
ただし、haskellについての知識はあまり必要ではありません。
以下がプログラムです。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
s :: (x -> y -> z) -> (x -> y) -> x -> z
s x y z = x z (y z)

k :: x -> y -> x
k x y = x

i :: p -> p
i x = x

b :: (x -> y) -> (z ->x) -> z -> y
b x y z = x (y z)

w :: (x -> x -> y) -> x -> y
w x y = x y y

c :: (x -> y -> z) -> y -> x -> z
c x y z = x z y

簡単に解説すると、2行ごとに1つのコンビネータを定義しています。
1行めの::以降が型情報で、2行目がコンビネータの定義になっています。

コンビネータ論理では、sとkだけでチューリング完全なことが知られていますが
bcwkの組み合わせでもチューリング完全になります。
むしろこちらの方が次の意味でわかりやすいと思います。
kは削除
wは複製
bは関数合成
cは引数のスワップ
を担当します。
sコンビネータはこれらのうち、複製、関数合成、引数のスワップを一緒くたにしたものと考えることができます。

コンビネータの型と論理学の公理との関係

上に載せたhaskellのコンビネータの定義に出てくる型は
そのまま命題論理の公理と対応しています。
AB: (B → C) → ((A → B) → (A → C)),
AC: (A → (B → C)) → (B → (A → C)),
AK: A → (B → A),
AW: (A → (A → B)) → (A → B).

また、sとkの組み合わせの場合は
AK: A → (B → A),
AS: (P→(Q→R))→( (P→Q)→(P→R) )
という公理と対応しています。
そして関数適用がモーダス・ポネンス(PとP->QからQを導く)に対応します。

haskellのソースコードのほうではカッコが少し省略されていますが
自動的に推論された型がそのまま公理と対応しているのがわかります。

さらにこれらからいくつかの公理を除去した論理学も研究されています。
例えばBCK論理では、上の公理から複製wを取り除いた論理の体系です。
こうした通常の命題論理より弱い論理体系群は部分構造論理と呼ばれています。

haskellのプログラムは型が命題、プログラムが証明に対応しています。
これをカリー・ハワード同型対応と呼びます。