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

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という形ではなくなってしまう

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

特殊なものを除いて、コンビネータには型をつけることができます。
そして、型付けられたコンビネータは論理学と深い関係があるのです。
型をつけられないコンビネータは、自己適用をする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のプログラムは型が命題、プログラムが証明に対応しています。
これをカリー・ハワード同型対応と呼びます。

賢人鳥

ある鳥xについて、xへ名前を呼びかけるとxが好きな鳥を返す特別な鳥のことを賢人鳥(Sage bird)と呼ぶ。
ここでギリシャ文字のΘが賢人鳥(Sage bird)を表すことにする。
賢人鳥は時々oracle birdsとも呼ばれる。
さらにコンビネータ論理の世界ではYコンビネータとして有名である。

1
2

xはΘxが好きなので
x(Θx) = Θx

Problem1のC1とC2の元で
森に賢人鳥がいるかどうかわかるだろうか
問題は、Mockingbirdがいて、任意の鳥xについてxとMを合成したyがいる。
この時xはyyが好きであるが、xが与えられてどうやってxとMを合成したyを見つければ良いか？
なんらかの鳥Aがいてその情報を提供してくれるなら問題は解決可能になる

解

ここで出てきた鳥AはLarkに他ならない。

1
2
3
4
5
6
7
8
9

任意の鳥x,yについて
(Ax)y=x(My)=x(yy)
これはLarkに他ならない

これで、MとLと条件C1の元で森に賢人鳥がいるかどうかを判定する問題に帰着された。  
Problem25で任意の鳥xは(Lx)(Lx)が好きだと示したので  
xはM(Lx)=(Lx)(Lx)が好きである。
ML(x)=Θx
xはΘxが好きであるのでΘは賢人鳥に他ならない。

ここで出てきた賢人鳥はコンビネータ論理の世界では不動点コンビネータ(fixed point combinator)と呼ばれるものです。

プライバシーポリシー

当サイトに掲載されている広告について

当サイトでは、第三者配信の広告サービス（Googleアドセンス）を利用しています。
広告配信事業者は、ユーザーの興味に応じた商品やサービスの広告を表示するため、当サイトや他サイトへのアクセスに関する情報 『Cookie』(氏名、住所、メール アドレス、電話番号は含まれません) を使用することがあります。
またGoogleアドセンスに関して、このプロセスの詳細やこのような情報が広告配信事業者に使用されないようにする方法については、www.aboutads.infoを参照ください。
当サイトでは、cookieから得た情報は広告表示のみに利用いたします。それ以外の目的で利用することはありません。

免責事項
当サイトからリンクやバナーなどによって他のサイトに移動された場合、移動先サイトで提供される情報、サービス等について一切の責任を負いません。

Larks

鳥Lは次の条件を満たすときLarkと呼ばれる

1

(Lx)y = x(yy)

Problem 24

LarkとIdentity birdのいる森にはMockingbirdがいることを証明せよ

解

1
2

LIx=I(xx)=xx
よってM=LIである

Problem 25

森にLarkがいれば、各鳥は少なくとも1つの鳥を好きである
Larkの存在はすべての鳥をnormalにする
すべてのnormal birdは幸せ(happy)である by problem 7
よってLarkが森にいればすべての鳥が幸せになる
なぜこれが正しいか

解

1
2
3
4
5
6

(Lx)y=x(yy)=x(My)
Lx = xM
任意の鳥xについて
(Lx)(Lx)=xM(xM)
=x(xM)(xM)
=x(Lx)(Lx)

Problem 26

なぜ絶望的に自己中心的なLarkは非常に魅力的か

解

1
2
3

Problem 25より各鳥は少なくとも1つの鳥が好きであるが
Larkが絶望的に自己中心的な時、その鳥もLarkになる
よってすべての鳥はLarkが好きである

Problem 27

どんな鳥もLarkかつKestrelにはなれないと仮定する
LarkがKestrelを好きになるのは不可能であることを証明せよ

解

1
2
3
4
5
6
7
8
9
10

LK=Kが成り立っていると仮定する
LKxy=K(xx)y=xx
Kxy = x
よってxx = xとなり
任意のxは自己中心的である
特にKも自己中心的であるため
[Problem11](/2019/01/14/tmm08)より
Kは絶望的に自己中心的である
しかるにそこには1種類の鳥しかいないことになり
これはLとKが異なるという仮定に反する

Problem 28

しかしながらKrdytrlがLarkを好きな時、
各鳥はLがすきなことを示せ

解

1
2
3
4

KL=L
KLx=L=Lx
よってLは絶望的に自己中心的
Problem26よりすべての鳥はLarkが好き

Problem 29

森にLarkがいるというその条件だけで、
少なくとも一つの鳥が自己中心的(egocentric)であることを示せる
Lが与えられて実際に自己中心的な鳥を書き下すことができるが
かっこを除いて12個ものLが必要になる
これを見つけよ

解

1
2
3
4
5
6
7
8
9
10
11
12
13
14

Lには好きな鳥yが存在するので
LLy=y
また
LLy=L(yy)
よって
L(yy)=y
L(yy)y=yy
また
L(yy)y=yy(yy)
よって(yy)は自己中心的
yはLLが好きな鳥なので
Problem 25よりLLは(Lx)(Lx)=(L(LL))(L(LL))が好き
これがyなので
yyは((L(LL))(L(LL)))((L(LL))(L(LL)))

Identity bird(Iコンビネータ)

鳥Iは次の条件を満たすときIdentity bird(Iコンビネータのこと)と呼ばれる

1
2

各鳥xについて
Ix = x

Iはそのまま与えられた鳥を返すだけなので
過去には思慮の無い鳥類学者からはidiot bird(バカな鳥)と呼ばれたこともある。
Identity birdはその特徴から、どんな鳥xも好きである。
また、I自体も好きなのでIdentity birdは自己中心的(egocentric)でもある。

Problem 20

森にはIdentity birdがいるとし、Iがagreeableであるとする。
各鳥は少なくとも一つの鳥を好きであると言えるか
注：以前の条件C1,C2はもはや必要ない

解

1
2
3
4

任意のBについて
Ix = Bx
Iの性質よりBx = x
よって任意の鳥Bはxが好き

Problem 21

森にIdentity birdがいて、各鳥は少なくとも1つの鳥がすきだとする。
この時、Iはagreeableだといえるか

解

1
2
3
4
5

各鳥Bはある鳥xが好きなので
Bx = x
よって
Bx = Ix
が成り立つのでIはagreeableである

Problem 22

森にはIdentity birdがいるとし、Iがagreeableであるかはわからないものとする。
しかし、各鳥のペアはcompatibleだとする。
次の2つのうちどちらが導き出されるか
　1.各鳥はnormal,つまり少なくとも1つの鳥が好き
　2.Iはagreeable

解

1
2
3
4
5
6

IとBがcompatibleだとすると
Ix = yかつBx=y
Ix = yよりx=y
よってBx=xとなりBはxが好き

また、この結論とProblem21よりIはagreeable

Problem 23

Identity birdは自己中心的(egocentric)だが
絶望的に自己中心的(hopelessly egocentric)ではない。
もしIが絶望的に自己中心的であるとすると
状況はとても悲しいものになるがそれはなぜか

解

1
2
3
4

Iの性質よりIx = x
Iが絶望的に自己中心的であるとすると
Ix = I
よってx=Iとなり、この森にはIしかいないことになる

Problem 15

Aが絶望的に自己中心的(hopelessly egocentric)なとき、
各鳥xについてAxも絶望的に自己中心的であることを証明せよ

解

1

(Ax)x = Axより成り立つ

Problem16

一般的にAx=Ayであってもx=yであるとは限らない
ただしKx = Ky ならばx=yであることを証明せよ(left cancellation law for kestrels)

解

1
2
3
4

任意のzについて
Kxz = x
Kyz = y
よってx=y

Problem 17

ある鳥が2つ以上の鳥を好きなことはありうる
しかしある鳥が2つ以上の鳥から固定化されることはない
それを証明せよ

解

1
2
3
4
5
6

ある鳥Aが鳥Bと鳥C(BはCと異なる)に固定化されているとすると
任意の鳥xについて
Ax = B
Ax = C
が成り立つのでB=C
これは初めの条件に反する

Problem 18

任意のKestrel Kと鳥xについて
KがKxを好きならばKはxを好きなことを証明せよ

解

1
2
3
4
5
6
7
8
9

KKx = Kxが成り立っているので
(KKx)x = (Kx)x
Kx = x
よってKはxが好き

別解
KKx = Kx
cancellation lawにより
Kx = x

Problem 19

誰かが言った
どんな自己中心的なKestrelは極端に寂しがり屋
なぜこれが正しいか

解

1
2
3
4
5
6
7

Kはegocentricなので
KK = Kで、任意のxについて
Kx=KKx=x
KxK = KKxK = KK
KxK = xK
よってxK=KKよりx=K
つまりこの森にはKしかいない

Problem 10

xがyに固定化されているとき、xはyを好きだと言えるか

解

1
2

任意のaについてxa = yであるから
xy = yも成り立つ

Problem 11

もしkestrelが自己中心的であるならば
それは絶望的に自己中心的であることを証明せよ

解

1
2
3
4
5

KK = Kが成立しているとすると
任意の鳥xについて
KKx = Kx
K = Kx
よってKは絶望的に自己中心的である

Problem 12

任意のKestrel Kと鳥xについて
もしK xが自己中心的ならばKはxが好きであることを証明せよ

解

1
2
3

(Kx)(Kx) = Kxが成り立つので
左辺= x
よってKx = xが成り立つ

Problem 13

次の文章の真偽を判定せよ
Aが絶望的に自己中心的なとき、
任意のxとyについて次が成り立つ

1

A x = A y

解

1
2
3
4
5

任意のx,yについて
Ax = A
Ay = A
なのでAx = Ayが成り立つ
よって真である

Problem 14

Aが絶望的に自己中心的な時、
次が従うか

1
2

任意の鳥x,yについて
(Ax)y = A

解

1

(Ax)y = Ay = A

ある鳥Bが絶望的に自己中心的(hopelessly egocentric)であるとは
任意の鳥xについて次が成り立つことを言う

1

Bx = B

おさらいとして、鳥Bが自己中心的(egocentric)であるというのは
以下が成り立つことでした

1

B B = B

より一般的に鳥Aが鳥Bに固定化(fixated)されるとは
各鳥xについて次がなりたつことを言う

1

A x = B

kestrel

ある鳥Kはkestrelと呼ばれる
これは次の性質を満たす

1
2

任意のx,yについて
(Kx)y = x

この時、鳥Kxはxに固定化されていると言える

problem 9

Problem1のC1とC2とKestrelの存在の元で
少なくとも一つの鳥が絶望的に自己中心的であることを証明せよ

解

1
2
3
4
5
6
7
8
9

条件の元では任意の鳥はある鳥が好きであるので
Kはある鳥Aが好きである
よってKA = A
任意の鳥xについて
KAx = Ax
KAx = A
でもあるので
Ax = A
Aは絶望的に自己中心的