この怪文書はクリエイティブ・コモンズ・ライセンスの元でライセンスされています。引用した文章など Kuwata Chikara に著作権のないものについては、それらの著作権保持者に帰属します。
檜山さんのセミナー（第三回）に行ってきた。今回は内容的に俺がまとめを書けるレベルじゃねえと思っていたら、他の参加者から「また徹夜してまとめ書くんでしょ」と言われてもう後に引けない状況。
というわけで風呂入って一休みしたら執筆開始。
追記：檜山さんによる添削・補足・解説記事が公開されているので、そちらも参照してください。
さっき檜山さんから参加者に送られたメールに「論理学の教科書を見たらカリー/ハワード対応に到達するまで普通は半年から一年かかるらしい」とか書いてあって、それを150分のセミナーでやるとかどんだけロックなんだよと思った。こんな時間からまとめを書こうとする俺も大概だが、まあいいや。執筆開始。内容がかなりの圧縮版だった事もあったので、俺の方で端折ったり調べたことを追加したり説明の順序を入れ替えたりしているので、そこら辺は注意。
今回のセミナーはまず算術回路・算術計算図という代物を使った計算過程の視覚化のトレーニングを行い、それを踏まえた命題論理の推論ステップの可視化と、そこから型付きラムダ計算と命題論理の対応関係、つまり今回の本題であるカリー/ハワード対応を導き出した。
まずは算術回路・算術計算図からなのだけど、細かく解説しているとキリがないので、算術回路については思い切って端折って、算術計算図を重点的に使う。理由は算術計算図はテキストエディタだけでも気合で書けるからだ。それでは本題の算術計算図に入る。算術計算図は以下のような定義が使われた。
任意の二引数の関数 f に対して x y --------- [f] f(x, y) 一引数の関数 g に対して x ------ [g] g(x) 定数 a に対して ---- [Const] a 複製 x -------- [Dup] x x 入れ替え x y -------- [Exch] y x
ここに「(+), (*), 5」だけが定義済みの関数・定数であるような系を当てはめて計算を行ってみる。例えばその系に引数として 2 を渡した時の計算例が以下のものになる。
---- [Const]
2 5
---------- [+] ---- [Const]
7 5
------------------------- [*]
35
また、算術計算図では計算マクロと計算済み定数が使える。以下は二つの引数をそれぞれ自乗して加算する SQSUM マクロの例である。
以下の計算過程を SQSUM と定義するものとする。 x y ------- [Dup] -------- [Dup] x x y y ------- [*] -------- [*] x * x y * y -------------------------- [+] x * x + y * y 3 4 ----- [SQSUM] 25
計算済み定数については割愛。大体一緒のノリだ。というかこの時点ですでに1時間使っていて消耗気味なんだよ! こっから先は適宜割愛しまくるし、これで大体雰囲気は掴めたものとして話を続ける。
まず最初の前提として、論理と算術の間には以下のような対応関係がある。
| 論理 | 算術 |
|---|---|
| 演繹系 | 算術回路キット |
| 推論 | 基本演算 |
| 証明図 | 計算図 |
| 演繹系の証明図 | 算術回路キットの計算図 |
| 証明可能 | 計算可能 |
| derived rule | 計算のマクロ |
| 公理 | 最初から使える定数 |
| 定理 | 計算済み定数 |
なので論理の方でも証明図を算術計算図のように使えるものとし、その使い方は以下のようになる。
仮定1 仮定2 ----------- [推論] 結論 ------ [公理の使用] 公理
また、 And 記号として∧を使うものとし、以下の推論規則が成り立つ。
連言の片側を取り出す： A∧B ---- [Sel-1] A A∧B ---- [Sel-2] B 二つの流れを合流させ、連言を作り出す： A B -------- [And] A∧B
推論規則とは別に構造規則というものもある。
A -------- [Dup] A A A B ------- [Exch] B A A --- [Id] A
これらを利用すると、以下の交換法則が成り立つ。
A∧B
-------------------- [Dup]
A∧B A∧B
---- [Sel-2] ---- [Sel-1]
B A
---------------------- [And]
B∧A
これらを使ってセミナーでは連立方程式を解いてみたりしていて、正直これを書くのはかなりしんどいのだけど、まあ頑張ってみるか。まずは以下の連立方程式を考えてみる。
2x + y = 5 3x - 2y = 4
代入法を使えば y = 5 -2x から x = 2, y = 1 というのが簡単に導けるが、ここでは証明図を使った推論ステップで「2x + y = 5 かつ 3x - 2y = 4 ならば x = 2 かつ y = 1」という結論を導いてみる。
2x + y = 5 ∧ 3x - 2y = 4
------------------------------------------------------[ Dup]
2x + y = 5 ∧ 3x - 2y = 4 2x + y = 5 ∧ 3x - 2y = 4
-------------------------- [Sel-1] --------------------------- [Sel-2]
2x + y = 5 3x - 2y = 4
------------ :
y = 5 - 2x :
--------------------- [Dup] :
y = 5 - 2x y = 5 - 2x 3x - 2y = 4
: ---------------------------------------
: 3x - 2(5 - 2x) = 4
: -------------------------------
: x = 2
: ---------------------- [Dup]
y = 5 - 2x x = 2 x = 2
------------------------- :
y = 1 x = 2
---------------------------------- [And]
x = 2 ∧ y = 1
この図を見てドン引きしてる人もいるかもしれないけど、セミナーではマジでこういう図を手書きしてたんだよ!
ところでこの図では「2x + y = 5 かつ 3x - 2y = 4 ならば x = 2 かつ y = 1」の推論ステップを記述しているわけだが、ここで「ならば」に相当する記号「⇒」を導入する。セミナーでは別の記号が使われていたけど、俺の使ってるフォントにはその記号が無いのでご勘弁。
この場合、前述の命題は「2x + y = 5 ∧ 3x - 2y = 4 ⇒ x = 2 ∧ y = 1」と記述でき、この⇒は含意と呼ばれるものだという。この含意を導入できる状態にある場合、先の命題の仮定部分（2x + y = 5 ∧ 3x - 2y = 4）は既に仮定ではないので消し去ってしまい、論理式の中に埋め込んでしまえる。この推論規則を演繹定理（DT）とする。証明図での現れ方は以下のようになる。
A ------ [何らかの推論] B 上記が成り立つ場合： #1 ---- A ---- [何らかの推論] B ---- [DT #1] A ⇒ B
ところで連言（∧）には連言から一方の要素を抜き出して連言を消去する推論規則があったが、含意にも消去を行う推論規則がある。これはモダスポネンス（MP）と呼ばれるもので、「P ならば Q である。 P である。よって Q」という推論規則。所謂「ソクラテスは人間だから死ぬ」とかの三段論法の事らしい。
A ⇒ B A
------------ [MP]
B
ここまでに出てきた推論規則は「Sel-1」「Sel-2」「And」「DT」「MP」の5つなのだが、これらはそれぞれ以下のように論理記号の導入・消去を行う。
| 推論規則 | 役割 | ノート |
|---|---|---|
| Sel-1 | ∧-消去1 | 1番目の選択 |
| Sel-2 | ∧-消去2 | 2番目の選択 |
| And | ∧-導入 | 二つの流れの合流 |
| DT | ⇒-導入 | 演繹定理 |
| MP | ⇒-消去 | モダントポネス |
論理記号には当然他にも様々な種類があり、それらに導入・消去を行う推論規則がある。例えば「または（∨）」に対しては多分以下のような推論規則が成り立つはず。
導入：
A B
------ [Or]
A ∨ B
消去：
A ∨ B A ⇒ C B ⇒ C
---------------------------
C
ところでまとめの冒頭で「命題論理」という言葉を使ったけど、命題論理では命題の詳細な中身には関わらずに証明可能性だけを扱う。また、今回のセミナーでは∧と⇒（及びそれ関連の推論規則）に構造規則だけで構成された自然演繹のサブセットを用いた。
……というところが大体前半戦の内容。ここから後半戦だけど体力が無くなってきた。
まずはいくつかの論理式の証明図を書いてみる。いちいちかったるいかもしれないけど、この後で使うんだよな、証明図を。
まずは「A ⇒ A」の証明図。
A ------- [Id] A DT を用いて仮定の部分を論理式に埋め込む： #1 ------- A ------- [Id] A ------- [DT #1] A ⇒ A
続いて (A ∧ B) ⇒ A。
まずは以下の形にする： A ∧ B ------- [Sel-1] A DT を用いて仮定の部分を論理式に埋め込む： #1 ------ A ∧ B ------- [Sel-1] A ------- [DT #1] (A ∧ B) ⇒ A
最後に A ⇒ (B ⇒ (A ∧ B))
∧-導入を行う：
A B
------- [And]
A ∧ B
DT で二つの仮定のうち B を埋め込む：
#1
---
A B
------- [And]
A ∧ B
------- [DT #1]
B ⇒ (A ∧ B)
もう一度 DT：
#2 #1
--- ---
A B
------- [And]
A ∧ B
------- [DT #1]
B ⇒ (A ∧ B)
------- [DT #2]
A ⇒ (B ⇒ (A ∧ B))
さて、上の証明図で DT を行っていく過程を「ラムダ抽象っぽい」と思った人はビンゴ。何がどうビンゴなのかの話のために、今からラムダ計算の話に移る。
これまでのセミナーでは型無しラムダ計算だけをターゲットにしてきたが、今回は型を導入し、またタプルの概念も導入する。タプルについては「任意の二つの型の順序対」というのが普通の定義……かな。とりあえずタプルについての操作を以下に示す。
タプルは (x, y) で表す (x, y).1 = x (x, y).2 = y
それじゃあ、先に出した算術計算図でタプルを操作してみようか。ここではタプルを生成する二引数の関数 t だけを定義してある。
x y
------ [t]
(x, y)
---------------- [Dup]
(x, y).1 (x, y).2
------------------ [t]
(x, y)
「おいこれさっきの命題論理で見たぞ」という人はまたしてもビンゴ。ここでのタプルの操作は以下のような推論規則の適用そのものだ。
A B
-------- [And]
A ∧ B
--------------------- [Dup]
A ∧ B A ∧ B
------ [Sel-1] ---------- [Sel-2]
A B
------------------------ [And]
A ∧ B
続いて型付きラムダ計算。セミナーでは例の絵算に型情報を付与したものを扱っていたけど、まあとりあえずフォーマルなラムダ式でやってみようか。型は(A, B) -> C という事にしておく。
λy:B. λx:A. (f(x, y):C)
もういい加減疲れてきたので一気に核心の所から書くと、命題論理における DT はまさにラムダ抽象の事であり、その一方で MP は関数適用である。個々の命題記号は基本的な型（A とか B な）であり、論理式は型の表現であると言う事。他の部分についても命題論理と計算の世界で対応が見られ、その対応をカリー/ハワード対応という……らしい。
だから例えば (A, B) -> C というプログラムがあった場合、それは即ち A ∧ B ⇒ C の証明に他ならないというのがカリー/ハワード対応の言っていることで、どういうわけかはわからないけど直観的には納得できるように思える。例えば次の証明図を考えてみる。
A B
-------- [And]
A ∧ B ⇒ C A ∧ B
-------------------- [MP]
C
こいつをちょっとばっかり弄くったとして
A B
------ [t]
(A, B) -> C (A, B)
--------------------- [関数適用]
C
対応しているように見えない? 演繹定理の方も似たような感じで、どんどん⇒を導出していく過程ってラムダ抽象を進めていくように見える。それで何でそんな対応が存在するのかはさっぱりわからんのだけど、ここでキーワードとして出てきたのがデカルト閉圏。ただしこれは名前が出ただけで終わってしまったようなものなので、今のところ詳細は不明。
俺が端折ってしまった部分や懇親会で出た話題にもいろいろと面白いものがあったんだけど、もう空が明るくなってきてしまったので一旦寝る事にする。気力が残っていれば他の部分についても書くかもしれんが、多分無理だろ。さすがに仕事帰りにセミナー寄って、そっから4時間半ぶっ続けで執筆というのは無謀過ぎた。
流石に一気に書き上げただけあっていろいろおかしな記述とかがあるなー。ちょくちょく直していくんで、まあその辺もご了承願いたい。
この怪文書はクリエイティブ・コモンズ・ライセンスの元でライセンスされています。引用した文章など Kuwata Chikara に著作権のないものについては、それらの著作権保持者に帰属します。