本編

まとめとその他の話題

も のま ね鳥を愛でる
結合子論理と計算
石井大海
筑波大学博士後期課程一年

Monday 6th March, 2017

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

追悼

Raymond M. Smullyan,(1919-2017)
石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

Table Of Contents

1

本編

2

まとめとその他の話題

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

も のま ね鳥をま ねる- 今回の種本

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

も のま ね鳥をま ねる- 今回の種本◎ 訳書 [5] は余り良くないので原書の方が良いかも石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

も のま ね鳥をま ねる- 今回の種本◎ 訳書 [5] は余り良くないので原書の方が良いかも- 結合子を「鳥」に見立てたパズルに親しむうちに不完全性定理に行き着く．

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

も のま ね鳥をま ねる- 今回の種本◎ 訳書 [5] は余り良くないので原書の方が良いかも- 結合子を「鳥」に見立てたパズルに親しむうちに不完全性定理に行き着く．

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

鳥のパズル（設定）
種本の冒頭では次の設定でパズルを考えている：- ある森に棲む鳥は，ある鳥の名前を聞くと別の鳥の名前を
言う．

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

鳥のパズル（設定）
種本の冒頭では次の設定でパズルを考えている：- ある森に棲む鳥は，ある鳥の名前を聞くと別の鳥の名前を言う．
◎ 鳥 A の「B 」に対する反応を AB と書く．括弧は左結合と考えて省略する：ABC = (AB )C.

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

鳥のパズル（設定）
種本の冒頭では次の設定でパズルを考えている：- ある森に棲む鳥は，ある鳥の名前を聞くと別の鳥の名前を言う．
◎ 鳥 A の「B 」に対する反応を AB と書く．括弧は左結合と考えて省略する：ABC = (AB )C.

- この森にはこういう鳥がいる：

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

参考文献

鳥のパズル（設定）
種本の冒頭では次の設定でパズルを考えている：- ある森に棲む鳥は，ある鳥の名前を聞くと別の鳥の名前を言う．
◎ 鳥 A の「B 」に対する反応を AB と書く．括弧は左結合と考えて省略する：ABC = (AB )C.

- この森にはこういう鳥がいる：

1. （合成鳥）任意の鳥 X と Y に対して，そいつらをリレーした
結果を返すような合成鳥 Z が必ずいる．
i.e. ∀X ∀Y ∃Z ∀x Zx = X (Yx ).
X , Y に対しその合成鳥（の一つ）を BXY で表す．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

鳥のパズル（設定）
種本の冒頭では次の設定でパズルを考えている：- ある森に棲む鳥は，ある鳥の名前を聞くと別の鳥の名前を言う．
◎ 鳥 A の「B 」に対する反応を AB と書く．括弧は左結合と考えて省略する：ABC = (AB )C.

- この森にはこういう鳥がいる：

1. （合成鳥）任意の鳥 X と Y に対して，そいつらをリレーした
結果を返すような合成鳥 Z が必ずいる．
i.e. ∀X ∀Y ∃Z ∀x Zx = X (Yx ).

X , Y に対しその合成鳥（の一つ）を BXY で表す．
2. （物まね鳥）Mx = xx を満たすような物まね鳥 M が居る．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

鳥のパズル（設定）
種本の冒頭では次の設定でパズルを考えている：- ある森に棲む鳥は，ある鳥の名前を聞くと別の鳥の名前を言う．
◎ 鳥 A の「B 」に対する反応を AB と書く．括弧は左結合と考えて省略する：ABC = (AB )C.

- この森にはこういう鳥がいる：

1. （合成鳥）任意の鳥 X と Y に対して，そいつらをリレーした
結果を返すような合成鳥 Z が必ずいる．
i.e. ∀X ∀Y ∃Z ∀x Zx = X (Yx ).

X , Y に対しその合成鳥（の一つ）を BXY で表す．
2. （物まね鳥）Mx = xx を満たすような物まね鳥 M が居る．

- AB = B となるとき，「鳥 A は B が好き」と言う．
石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

例
問 1 (不動点定理)

合成鳥 B と物まね鳥 M が居るなら，どんな鳥 A も少なくとも一羽の鳥が好き (i.e. ∀A ∃x Ax = x).

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

例
問 1 (不動点定理)

合成鳥 B と物まね鳥 M が居るなら，どんな鳥 A も少なくとも一羽の鳥が好き (i.e. ∀A ∃x Ax = x).

（答）X = BAM とすると XX がそれ．

XX = A(MX ) = A(XX )石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

例
問 1 (不動点定理)

合成鳥 B と物まね鳥 M が居るなら，どんな鳥 A も少なくとも一羽の鳥が好き (i.e. ∀A ∃x Ax = x).

（答）X = BAM とすると XX がそれ．

XX = A(MX ) = A(XX )- こんな感じで帳尻を合わせていくパズルが沢山．

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

例
問 1 (不動点定理)

合成鳥 B と物まね鳥 M が居るなら，どんな鳥 A も少なくとも一羽の鳥が好き (i.e. ∀A ∃x Ax = x).

（答）X = BAM とすると XX がそれ．

XX = A(MX ) = A(XX )- こんな感じで帳尻を合わせていくパズルが沢山．
- 詳しくは紹介しませんが，次のパズルは言霊がすごい：石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

例
問 1 (不動点定理)

合成鳥 B と物まね鳥 M が居るなら，どんな鳥 A も少なくとも一羽の鳥が好き (i.e. ∀A ∃x Ax = x).

（答）X = BAM とすると XX がそれ．

XX = A(MX ) = A(XX )- こんな感じで帳尻を合わせていくパズルが沢山．
- 詳しくは紹介しませんが，次のパズルは言霊がすごい：

問2
救いがたいほど自己中心的なヒバリは異常に魅力的なのは
なぜか？

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

数学的内容：結合子論理? 「鳥」パズルは数学的には何なのか？

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

数学的内容：結合子論理? 「鳥」パズルは数学的には何なのか？
結合子論理！

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

参考文献

数学的内容：結合子論理? 「鳥」パズルは数学的には何なのか？
結合子論理！

- 結合子と変数の文字列を一定の規則に従って書き換えていく「計算」だと思える．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

数学的内容：結合子論理? 「鳥」パズルは数学的には何なのか？
結合子論理！

- 結合子と変数の文字列を一定の規則に従って書き換えていく「計算」だと思える．
※ ここでは括弧の順番まで込めた文字列を考えている．また，三つ以上の文字が並ぶ時は左から順に二つずつ括弧が省略されていると考える：xyz = (xy )z = ((xy )z ),x (yzw ) = (x ((yz )w )).

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

数学的内容：結合子論理? 「鳥」パズルは数学的には何なのか？
結合子論理！

- 結合子と変数の文字列を一定の規則に従って書き換えていく「計算」だと思える．
※ ここでは括弧の順番まで込めた文字列を考えている．また，三つ以上の文字が並ぶ時は左から順に二つずつ括弧が省略されていると考える：xyz = (xy )z = ((xy )z ),x (yzw ) = (x ((yz )w )).

- 先程の問題は，「Bxyz B x (yz )，Mx B xx という書き換え規則の下で，任意の A に対してその不動点として振る舞うものを見付けよ」という意味だった．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

数学的内容：結合子論理? 「鳥」パズルは数学的には何なのか？
結合子論理！

- 結合子と変数の文字列を一定の規則に従って書き換えていく「計算」だと思える．
※ ここでは括弧の順番まで込めた文字列を考えている．また，三つ以上の文字が並ぶ時は左から順に二つずつ括弧が省略されていると考える：xyz = (xy )z = ((xy )z ),x (yzw ) = (x ((yz )w )).

- 先程の問題は，「Bxyz B x (yz )，Mx B xx という書き換え規則の下で，任意の A に対してその不動点として振る舞うものを見付けよ」という意味だった．
? 自由に「書き換え」出来るにはどんな結合子があればよ
いか？

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

数学的内容：結合子論理? 「鳥」パズルは数学的には何なのか？
結合子論理！

- 結合子と変数の文字列を一定の規則に従って書き換えていく「計算」だと思える．
※ ここでは括弧の順番まで込めた文字列を考えている．また，三つ以上の文字が並ぶ時は左から順に二つずつ括弧が省略されていると考える：xyz = (xy )z = ((xy )z ),x (yzw ) = (x ((yz )w )).

- 先程の問題は，「Bxyz B x (yz )，Mx B xx という書き換え規則の下で，任意の A に対してその不動点として振る舞うものを見付けよ」という意味だった．
? 自由に「書き換え」出来るにはどんな結合子があればよいか？
? 「書き換え」計算でどの程度の事が計算出来るのか（計算
能力）？
石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

自由に「書き 換え」が出来る ために- 各「書き換え」ステップの定義が必要．

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

参考文献

自由に「書き 換え」が出来る ために- 各「書き換え」ステップの定義が必要．

ここではラフに「変数 x1 . . . xn をとって，それらと幾つかの結合子からなる括弧つき文字列を返す操作」と思っておこう．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

自由に「書き 換え」が出来る ために- 各「書き換え」ステップの定義が必要．

ここではラフに「変数 x1 . . . xn をとって，それらと幾つかの結合子からなる括弧つき文字列を返す操作」と思っておこう．

- 変数 x を含む文字列 t に対して，「x を t に書き換える操作」
を “λ x. t” と表すことにする．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

自由に「書き 換え」が出来る ために- 各「書き換え」ステップの定義が必要．

ここではラフに「変数 x1 . . . xn をとって，それらと幾つかの結合子からなる括弧つき文字列を返す操作」と思っておこう．

- 変数 x を含む文字列 t に対して，「x を t に書き換える操作」
を “λ x. t” と表すことにする．
x◎ (λ x. t )A B t [ A].（t [ Ax ] は t で変数 x に A を代入したもの）

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

自由に「書き 換え」が出来る ために- 各「書き換え」ステップの定義が必要．

ここではラフに「変数 x1 . . . xn をとって，それらと幾つかの結合子からなる括弧つき文字列を返す操作」と思っておこう．

- 変数 x を含む文字列 t に対して，「x を t に書き換える操作」
を “λ x. t” と表すことにする．
x◎ (λ x. t )A B t [ A].（t [ Ax ] は t で変数 x に A を代入したもの）- 複数変数を必要とする場合は
λ x1 . . . xn . t ≡ λ x1 . λ x2 . . . . λ xn . t と表す．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

自由に「書き 換え」が出来る ために- 各「書き換え」ステップの定義が必要．

ここではラフに「変数 x1 . . . xn をとって，それらと幾つかの結合子からなる括弧つき文字列を返す操作」と思っておこう．

- 変数 x を含む文字列 t に対して，「x を t に書き換える操作」
を “λ x. t” と表すことにする．
x◎ (λ x. t )A B t [ A].（t [ Ax ] は t で変数 x に A を代入したもの）- 複数変数を必要とする場合は
λ x1 . . . xn . t ≡ λ x1 . λ x2 . . . . λ xn . t と表す．
- この問題は次のように言い換えられる：

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

自由に「書き 換え」が出来る ために- 各「書き換え」ステップの定義が必要．

ここではラフに「変数 x1 . . . xn をとって，それらと幾つかの結合子からなる括弧つき文字列を返す操作」と思っておこう．

- 変数 x を含む文字列 t に対して，「x を t に書き換える操作」
を “λ x. t” と表すことにする．
x◎ (λ x. t )A B t [ A].（t [ Ax ] は t で変数 x に A を代入したもの）- 複数変数を必要とする場合は
λ x1 . . . xn . t ≡ λ x1 . λ x2 . . . . λ xn . t と表す．
- この問題は次のように言い換えられる：

問3~x と t に対して，(λ ~x. t )~x と C~x の簡約結果が一致する文字
列 C が欲しい．どんな結合子があれば十分か？
石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

SK-計算：必要な結合子の見付け方- 今回考える「文字列」t は変数を含む「文字」からはじめて二つずつ括弧で括ったものだった．

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

SK-計算：必要な結合子の見付け方- 今回考える「文字列」t は変数を含む「文字」からはじめて二つずつ括弧で括ったものだった．
この作り方にそって考えてみよう！

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

参考文献

SK-計算：必要な結合子の見付け方- 今回考える「文字列」t は変数を含む「文字」からはじめて二つずつ括弧で括ったものだった．
この作り方にそって考えてみよう！
1. t = x の時：(λ x. x ) に当たるような結合子が欲しい．そこでI ≡ (λ x. x ) とおこう．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

SK-計算：必要な結合子の見付け方- 今回考える「文字列」t は変数を含む「文字」からはじめて二つずつ括弧で括ったものだった．
この作り方にそって考えてみよう！
1. t = x の時：(λ x. x ) に当たるような結合子が欲しい．そこでI ≡ (λ x. x ) とおこう．
2. t が x と異なる文字 y の時：(λ x. y ) は y を返す定数関数．そこで K ≡ (λ yx. y ) とすれば，λ x. y ≡ Ky と書ける．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

SK-計算：必要な結合子の見付け方- 今回考える「文字列」t は変数を含む「文字」からはじめて二つずつ括弧で括ったものだった．
この作り方にそって考えてみよう！
1. t = x の時：(λ x. x ) に当たるような結合子が欲しい．そこでI ≡ (λ x. x ) とおこう．
2. t が x と異なる文字 y の時：(λ x. y ) は y を返す定数関数．そこで K ≡ (λ yx. y ) とすれば，λ x. y ≡ Ky と書ける．
3. t = (uv ) の時：帰納法の仮定から，(λ x. u ) と (λ x. v ) は何
らかの文字列で表せるとしてよい．このときuv ≡ ((λ x. u )x )((λ x. v )x ) となるので，S ≡ λ xyz. (xz )(yz ) とおけば，λ x. uv ≡ S (λ x. u )(λ x. v ).

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

SK-計算：必要な結合子の見付け方- 今回考える「文字列」t は変数を含む「文字」からはじめて二つずつ括弧で括ったものだった．
この作り方にそって考えてみよう！
1. t = x の時：(λ x. x ) に当たるような結合子が欲しい．そこでI ≡ (λ x. x ) とおこう．
2. t が x と異なる文字 y の時：(λ x. y ) は y を返す定数関数．そこで K ≡ (λ yx. y ) とすれば，λ x. y ≡ Ky と書ける．
3. t = (uv ) の時：帰納法の仮定から，(λ x. u ) と (λ x. v ) は何
らかの文字列で表せるとしてよい．このときuv ≡ ((λ x. u )x )((λ x. v )x ) となるので，S ≡ λ xyz. (xz )(yz ) とおけば，λ x. uv ≡ S (λ x. u )(λ x. v ).

以上から上記のような S, K, I があれば十分！

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

SK-計算：必要な結合子の見付け方- 今回考える「文字列」t は変数を含む「文字」からはじめて二つずつ括弧で括ったものだった．
この作り方にそって考えてみよう！
1. t = x の時：(λ x. x ) に当たるような結合子が欲しい．そこでI ≡ (λ x. x ) とおこう．
2. t が x と異なる文字 y の時：(λ x. y ) は y を返す定数関数．そこで K ≡ (λ yx. y ) とすれば，λ x. y ≡ Ky と書ける．
3. t = (uv ) の時：帰納法の仮定から，(λ x. u ) と (λ x. v ) は何
らかの文字列で表せるとしてよい．このときuv ≡ ((λ x. u )x )((λ x. v )x ) となるので，S ≡ λ xyz. (xz )(yz ) とおけば，λ x. uv ≡ S (λ x. u )(λ x. v ).

以上から上記のような S, K, I があれば十分！

? 更に I ≡ SKK と書ける（演習問題！）ので，S と K があれ
ば書き換えは自由に出来る！
石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

実際の例
これまでの議論で次の「SK-変換」規則が得られた：

λ x. x :≡ I ≡ SKK,
λ x. y :≡ Ky(if x 6= y ),λ x. (uv ) :≡ S(λ x. u )(λ x. v ).

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

実際の例
これまでの議論で次の「SK-変換」規則が得られた：

λ x. x :≡ I ≡ SKK,
λ x. y :≡ Ky(if x 6= y ),λ x. (uv ) :≡ S(λ x. u )(λ x. v ).

Example 1
M ≡ λx.xx ≡ S(λ x. x )(λ x. x ) ≡ SII ≡ S(SKK)(SKK).

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

実際の例
これまでの議論で次の「SK-変換」規則が得られた：

λ x. x :≡ I ≡ SKK,
λ x. y :≡ Ky(if x 6= y ),λ x. (uv ) :≡ S(λ x. u )(λ x. v ).

Example 1
M ≡ λx.xx ≡ S(λ x. x )(λ x. x ) ≡ SII ≡ S(SKK)(SKK).
Exercise 1
上の SK-変換には結構無駄があるので，もう少し結果が短かくなる規則を与えよ．それを使って B ≡ λxyz.x (yz ) を S,
K, I で表せ．
石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

計算能力- SK-計算でどの程度の事が計算出来るのか？

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

計算能力- SK-計算でどの程度の事が計算出来るのか？
実は理論上計算機と同じ計算が出来る！

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

計算能力- SK-計算でどの程度の事が計算出来るのか？
実は理論上計算機と同じ計算が出来る！

Theorem 2 (構造化定理)
計算機で計算可能なアルゴリズムを実装するには次の三つの要素があればよい：
逐次実行 f; g 「処理 f の後に g をやる」
条件分岐 if (p) then f else g 「条件 p が成り立つな
ら f ，さもなくば g 」
反復実行 while (p) { f } 「条件 p が成り立つ限り fを繰り返す」

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

計算能力- SK-計算でどの程度の事が計算出来るのか？
実は理論上計算機と同じ計算が出来る！

Theorem 2 (構造化定理)
計算機で計算可能なアルゴリズムを実装するには次の三つの要素があればよい：
逐次実行 f; g 「処理 f の後に g をやる」
条件分岐 if (p) then f else g 「条件 p が成り立つな
ら f ，さもなくば g 」
反復実行 while (p) { f } 「条件 p が成り立つ限り fを繰り返す」
逐次実行は明らかなので，SK-計算で条件分岐と反復操作が出来ることがわかればよい！
石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

条件分岐と反復操作? 条件分岐石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

条件分岐と反復操作? 条件分岐◎ 基本戦略：if p then t else f と書く代わりに
ptf (= (pt )f ) と書こう．

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

条件分岐と反復操作? 条件分岐◎ 基本戦略：if p then t else f と書く代わりに
ptf (= (pt )f ) と書こう．
true :≡ λ t f . t ≡ K, false ≡ λ t f . f ≡ KI とすれば良い．

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

参考文献

条件分岐と反復操作? 条件分岐◎ 基本戦略：if p then t else f と書く代わりに
ptf (= (pt )f ) と書こう．
true :≡ λ t f . t ≡ K, false ≡ λ t f . f ≡ KI とすれば良い．
? 反復操作……while p f x が「px が偽になるまで f を x に繰り返し適用」になるような while を得ればよい．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

条件分岐と反復操作? 条件分岐◎ 基本戦略：if p then t else f と書く代わりに
ptf (= (pt )f ) と書こう．
true :≡ λ t f . t ≡ K, false ≡ λ t f . f ≡ KI とすれば良い．
? 反復操作……while p f x が「px が偽になるまで f を x に繰り返し適用」になるような while を得ればよい．
◎ 観察：while p f x = if (p x ) then x else f (while p f x )石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

条件分岐と反復操作? 条件分岐◎ 基本戦略：if p then t else f と書く代わりに
ptf (= (pt )f ) と書こう．
true :≡ λ t f . t ≡ K, false ≡ λ t f . f ≡ KI とすれば良い．
? 反復操作……while p f x が「px が偽になるまで f を x に繰り返し適用」になるような while を得ればよい．
◎ 観察：while p f x = if (p x ) then x else f (while p f x )λ z. if (p x) then x else f z の不動点があればよい．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

条件分岐と反復操作? 条件分岐◎ 基本戦略：if p then t else f と書く代わりに
ptf (= (pt )f ) と書こう．
true :≡ λ t f . t ≡ K, false ≡ λ t f . f ≡ KI とすれば良い．
? 反復操作……while p f x が「px が偽になるまで f を x に繰り返し適用」になるような while を得ればよい．
◎ 観察：while p f x = if (p x ) then x else f (while p f x )λ z. if (p x) then x else f z の不動点があればよい．
B, M は S, K で書ける．すると，最初の問題から，SK-計算でも任意の項に対して不動点が存在する！

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

条件分岐と反復操作? 条件分岐◎ 基本戦略：if p then t else f と書く代わりに
ptf (= (pt )f ) と書こう．
true :≡ λ t f . t ≡ K, false ≡ λ t f . f ≡ KI とすれば良い．
? 反復操作……while p f x が「px が偽になるまで f を x に繰り返し適用」になるような while を得ればよい．
◎ 観察：while p f x = if (p x ) then x else f (while p f x )λ z. if (p x) then x else f z の不動点があればよい．
B, M は S, K で書ける．すると，最初の問題から，SK-計算でも任意の項に対して不動点が存在する！
◎ よって反復操作も実現可能！

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

条件分岐と反復操作? 条件分岐◎ 基本戦略：if p then t else f と書く代わりに
ptf (= (pt )f ) と書こう．
true :≡ λ t f . t ≡ K, false ≡ λ t f . f ≡ KI とすれば良い．
? 反復操作……while p f x が「px が偽になるまで f を x に繰り返し適用」になるような while を得ればよい．
◎ 観察：while p f x = if (p x ) then x else f (while p f x )λ z. if (p x) then x else f z の不動点があればよい．
B, M は S, K で書ける．すると，最初の問題から，SK-計算でも任意の項に対して不動点が存在する！
◎ よって反復操作も実現可能！

? 構造化定理より SK-計算の能力は計算機と「等価」．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

Table Of Contents

1

本編

2

まとめとその他の話題

石井大海

ものまね鳥を愛でる

参考文献

本編

まとめとその他の話題

参考文献

ま とめとその他の話題計算が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

ま とめとその他の話題計算が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．
◎ こういうのを結合子計算とか結合子論理という．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

ま とめとその他の話題計算が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．
◎ こういうのを結合子計算とか結合子論理という．

? SK は計算機と同等の計算能力を持つ．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

ま とめとその他の話題計算が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．
◎ こういうのを結合子計算とか結合子論理という．

? SK は計算機と同等の計算能力を持つ．
- 発展的話題石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

ま とめとその他の話題
算数が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．
◎ こういうのを結合子計算とか結合子論理という．

? SK は計算機と同等の計算能力を持つ．
n- 発展的話題z }| {◎ 自然数 n ∈ N と「n 回反復」関数 λfx.f (f (f . . . (f x ))) と n を同一視して，自然数の算数を実現出来る（Church 符号化）

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

ま とめとその他の話題論理が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．
◎ こういうのを結合子計算とか結合子論理という．

? SK は計算機と同等の計算能力を持つ．
n- 発展的話題z }| {◎ 自然数 n ∈ N と「n 回反復」関数 λfx.f (f (f . . . (f x ))) と n を同一視して，自然数の算数を実現出来る（Church 符号化）
◎ S, K を関数だと思って「型」をつけてみると，
S : (α → β → γ) → (α → β) → α → γ, K : α → β → α.

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

ま とめとその他の話題論理が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．
◎ こういうのを結合子計算とか結合子論理という．

? SK は計算機と同等の計算能力を持つ．
n- 発展的話題z }| {◎ 自然数 n ∈ N と「n 回反復」関数 λfx.f (f (f . . . (f x ))) と n を同一視して，自然数の算数を実現出来る（Church 符号化）
◎ S, K を関数だと思って「型」をつけてみると，
S : (α → β → γ) → (α → β) → α → γ, K : α → β → α.

これは通常の命題論理の公理から排中律を除いた公理と同じ！

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

ま とめとその他の話題論理が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．
◎ こういうのを結合子計算とか結合子論理という．

? SK は計算機と同等の計算能力を持つ．
n- 発展的話題z }| {◎ 自然数 n ∈ N と「n 回反復」関数 λfx.f (f (f . . . (f x ))) と n を同一視して，自然数の算数を実現出来る（Church 符号化）
◎ S, K を関数だと思って「型」をつけてみると，
S : (α → β → γ) → (α → β) → α → γ, K : α → β → α.

これは通常の命題論理の公理から排中律を除いた公理と同じ！
● これに「例外処理」「短絡評価」を入れると普通の論理になる．

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

ま とめとその他の話題論理が出来るフレンズ- SK-計算：Sxyz B xz (yz ), Kxy B x なる二つの書き換え規則に従って式変形をする操作．
◎ こういうのを結合子計算とか結合子論理という．

? SK は計算機と同等の計算能力を持つ．
n- 発展的話題z }| {◎ 自然数 n ∈ N と「n 回反復」関数 λfx.f (f (f . . . (f x ))) と n を同一視して，自然数の算数を実現出来る（Church 符号化）
◎ S, K を関数だと思って「型」をつけてみると，
S : (α → β → γ) → (α → β) → α → γ, K : α → β → α.

これは通常の命題論理の公理から排中律を除いた公理と同じ！
● これに「例外処理」「短絡評価」を入れると普通の論理になる．
! 論理と計算の深い関係を示唆している（Curry-Howard 対応）

石井大海

ものまね鳥を愛でる本編

まとめとその他の話題

参考文献

参考文献 I[1]

J. Roger Hindley and J. P Seldin, Lambda-calculus and combinators, anintroduction, Cambridge, UK: Cambridge University Press, 2008, isbn:9780521898850, url:
http://www.loc.gov/catdir/toc/ecip0810/2008006276.html.

[2]Jean-Louis Krivine, Realizability algebras: a program to well order R,
version 0, Logical Methods in Computer Science 7 (3:2 Aug. 10, 2011),
doi: 10.2168/LMCS-7(3:2)2011, arXiv: 1005.2395 [cs.LO].

[3]

古森雄一, 汎用システムとしての「ラムダ計算 + 論理」, 2006, url:
http://www.math.s.chibau.ac.jp/~komori/symposium/suukaiken/komori8.pdf.

[4]

古森雄一 and 小野寛晰, 現代数理論理学序説, 日本評論社, 2010.

[5]

Ｒ・スマリヤン, ものまね鳥をまねる, trans. by 阿部剛久 et al., 原著：To
Mock a Mockingbird, 森北出版, 1998.

[6]

魔法少女, 命題論理, 2015.

石井大海

ものまね鳥を愛でる