Haskell/カリー=ハワード同型

カリー=ハワード同型(Curry-Howard isomorphism)は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。

導入

これよりカリー=ハワード同型は単に C-H と表記する。C-H が示しているのは、定理の本質を反映するような型を構築し、それからその型を持つ値を見つけさえすれば、どんな数学的定理をも証明することができる、ということだ。これは最初は極めて不思議に思える。型と定理にどんな関係があるというのだろうか？しかしながら、以下に述べるように、このふたつは非常に近しい関係にあるのである。はじめる前に簡単に注意しておくが、導入の章では error や undefinedのような 表示的意味論 が ⊥ である式の存在は無視する。これらはとても重要な役割を果たすのだが、これらについては後ほど別に考えることにする。また、unsafeCoerce#のような型システムを迂回する関数についても無視することにする。

Haskellの高階関数の機能を使えばとても複雑な型を構築することができる。次のような質問をしてみるといい。すべての型は少なくともひとつは値が存在する(このような型を空でない集合(inhabited)という)だろうか？最初は「どんな型でもそうだ」と思うかもしれないが、次の例はあっさりとその直感を打ち砕く。たとえば、なんらかの型aの値をまったく別の型 b の値に変換する方法は存在しないので(あらかじめ a や bを知っており ord :: Char -> Intのような単相関数について述べているのでない限り)、型a -> bをもつ関数は存在しない。

信じられないことに、型が数学の論理における真である定理と対応するときだけ、型は空でないことがわかるのである。しかし、この対応はなぜなのだろうか？a -> bのような型は論理の文脈においては何を意味しているのだろうか？

形式論理最速入門

型理論の探求を始める前に、ある程度の形式論理の素養が必要だ。これはとても簡単な入門である。より詳しい背景を知るためには、形式理論についての入門書を参照することをお勧めする。

我々は毎日のように「もし～ならば～」という表現を使っている。たとえば、「もし天気が良かったら、街まで歩いていく」などだ。この種の表現は数学にも登場する。「もしxが正なら、xは(実数の)平方根を持つ」のように言うことがあるだろう。形式論理は曖昧でぼんやりとした自然言語を正確な記号へとこのような主張を翻訳する手段なのである。もし何かが真なら真であるということを、 → 記号(「ならば」と読む)を使って表す。例えば、もし天気が良いということが真なら、街まで歩いて行くというのが真である、という先程使った「もし～ならば～」による文章とまったくおなじ意味で、先ほどの文章は「天気が良い→街まで歩いて行く」と書き換えることができる。また、文章全体を表すために文字を使うことがある。たとえば、もし W が先程の「天気がいい」という文章で、Tが「街まで歩いて行く」という文章なら、先程の例は単に W →T と書ける。

先程述べた → の定義のずるい方法に注意されたい。P → Q は、もし P が真なら、 Qは真である、という意味だった。でも、もし Qが「太陽は熱い」のような常に真であるような文章だったら、Pが何であっても問題はない。Pが偽である文章だとしても同様で、もしPが真であったとしても Qは真であるということになる。したがって、P → Qはやはり成り立つ。Pが真でなくとも Q が真になるということは、まったく別のことなのだ。P → Qといった時にこの疑問を尋ねることはない。よって、「空が赤い→太陽は熱い」がやはり正当な文章であるように、→は実はなんらかの因果関係の一種を表しているわけではない。

論理積と論理和と呼ばれるものも日常の言語と数学の両方で登場する事柄である。前者は「かつ」、後者は「または」を意味する形式表現である。「もし在庫がありお金が足りれば、この雑誌を買うだろう」という文章は形式的に$(M\wedge S)\to B$と表現される。ここで、M = 'お金が足りる'、S = '雑誌の在庫がある'、B = '雑誌を買うだろう'である。実際、$\wedge$単には「かつ」と読むことができる。同様に、$\vee$ は「または」と読むことができ、「徒歩か電車で仕事に行くだろう」は$W\vee T$と表される。ここで、W = '徒歩で仕事に行く', and T = '電車で仕事に行く'である。

これらの記号とこれから紹介する幾つかのものを使い、任意の複雑な記号列を生成することができる。これらの記号列は、定理(theorems)と呼ばれることもある真の主張と、非定理(nontheorems)と呼ばれることがある偽の主張の二種類に分類できる。あらゆる記号列はその文字が表しているものに従って定理か非定理のどちらかになることに注意すると、例えば、もし P が「昼間である」という文章を表し、Qが「夜である」という文章を表すなら、(夕方のような例外を除けば)$P\vee Q$ は定理であるが、もしPが「木は青い」でQは「すべての鳥は飛ぶことができる」ならこれは非定理となる。定理かどうかわからない記号列は、命題と呼ぶこともある。

(「もしあなたが夕食を食べるのなら、その時に限りデザートを食べるだろう」という意味で「もしあなたが夕食を食べるならデザートも食べるだろう」というときのように)論理にはもっと多くの微妙な話題が存在する。もしこれらの話題に興味があるなら、これらの話題を包括的にあつかう多くの教科書がある。

定理と型

それでは、形式論理においては型 a -> b は何を意味するのだろうか？簡単なことに、単にa → bを意味しているのだ。もちろん、これはa と bが形式理論において解釈可能な型であるときだけ成り立っている。これは C-H の本質である。また、先程述べたように、a -> b が空でない型であるとき、その時に限り a → bは定理となる。

もっとも単純な Haskell 関数のひとつを使ってみていこう。const は a -> b -> a　という型を持つ。形式論理ではa → b → aとなる。値constがあるので、これは型 a -> b -> a が空ではなく、定理であることは間違いない。いま、a → bは「もしa が真だとすれば、b は真である」の別の表現なのである。したがって、a → b → a は「もしaが真であり、もしbが真であるなら、aは真であると結論できることを意味する。aが真であると仮定するなら、仮定によりaが真であるから、これはもちろん定理である。

⊥にまつわる問題

型が空でないならば、その型は定理と一致することを述べてきた。しかしながら、Haskell においては、値undefinedが存在することにより、どんな型も空ではない。実際に、より一般的には、⊥の表示的意味論を持つ値は、すべては型forall a. aという型であるのが問題なのである。型理論における⊥は、論理における矛盾と一致する。すべての型は空でないので、Haskell の型を使ってどんな定理も証明することができる。それゆえ、Haskell の型システムは実際には矛盾した論理システムと一致する。しかしながら、もしHaskellの型システムの制限されたサブセットを使うなら、特に多相型を禁止すれば、ちゃんと面白いことができる一貫性のある論理体系を得ることができる。これからは、そのような型システム内で話を進めていく。

これで C-H の基礎を身に着けたので、型と命題の関係をさらに解き明かすのを始めることができるようになった。

論理演算と等価なもの

記号論理の本質は、P や Q のような命題の集合と、Q → P や $P\vee Q$ のようなこれらの命題を組み合わせるさまざまな方法である。命題を組み合わせるこれらの方法は命題の演算と考えることができる。C-H により命題は型と対応し、ゆえに普通は型構築子として知られるその論理演算と C-H の等価なものを得るのである。すでにこの一例を見てきた。論理における論理包含演算子 → は型構築子 (->) と対応する。この章の残りの部分は残りの命題演算を探求し、対応関係の説明を進めていく。

論理積と論理和

$A\wedge B$ が定理となるためには、A と B の両方は定理でなければならない。よって、$A\wedge B$ の証明は A と B の両方を証明することに等しい。型 A の値を見つけることが 命題 A の証明であることを思い出そう。ここで A と A は C-H 対応している。ゆえに、この場合、最初の A と一致する型と２つ目の B と一致する型の、従属する２つの値含む値を見つけたいということになる。これは実にペアに似ているように思える。実際に、記号列 $A\wedge B$ は (a, b) と表現する。ここで a は A に、b は B に相当する。

論理和は論理積とは逆である。$A\vee B$ が定理であるためには、A か B のどちらかが定理でなければならない。先程と同様に、型 A の値か型 B の値のどちらかを含むような値を探す。これは Either だ。Either A B は命題 $A\vee B$ と一致する型なのである。

偽

我々の論理体系では、偽の主張を表すことは役に立つことがある。定義により、偽の主張は証明することができないものである。ゆえに、空であるような型を探すことになる。デフォルトのライブラリにはこのような型は存在しないが( () 型で混乱しないように。これは明らかにひとつ値がある)、GHC の -XEmptyDataDecls フラグをオンにすれば自分で定義することができる。

data Void

構築子を省くことにより、Void は空である型を意味することになる。それゆえ、Void 型は論理の非定理と一致する。役に立つ当然の帰結を幾つか挙げる。

1. どんな型Aについても、(Void, A) と (A, Void) はどちらも空である型であり、もしFが非定理なら $F\wedge A$ と $A\wedge F$ はどちらも非定理であるという事実と対応する。
2. どんな型 A についても、Either Void A と Either A Void は本質的に A と同じであり、 Fが非定理で A が定理であるとき、$F\vee A$ と $A\vee F$ が真であるという事実と対応する。
3. 非定理と対応するどんな型も Void に置き換えることができる。これはどんな非定理型も空であるからで、ゆえになにも変更せずとも Void に置き換えることができるのである。Void は実際にどんな非定理型とも等価である.

4. 最初の章で発見したように、P の値が真であるかどうかにかかわらず、もし Q が真であれば論理包含 P → Q は真である。したがって、型 Void -> a の項を見つけ出すことができるはずである。実際に存在するのだが、これはすこし説明が複雑になる。答えは 空( empty )関数である。関数 f :: A -> B を 最初の要素が A の要素であるような(おそらく無限の) 集合の組 (定義域) と ２つ目の要素がB (値域)の要素であるようなこの項における f の出力と定義することができる。たとえば、自然数においてある自然数のすぐ次の自然数を得る関数は {(0,1), (1,2), (2,3), ...} と表すことができる。(total かつ well-defined な) 関数とするために、項 aが型 A である組 (a, f a) ひとつをちょうど得ることに注意されたい。

   
   

   この空関数を empty と呼ぶことにしよう。このように empty は空集合で表すことができる。 しかし、それぞれ定義域の要素である組がなければならないが、この表現に組は存在せず、定義域は空、すなわち Void でなければならない。値域の型についてはどうだろうか。 empty はどんな出力もしないので、値域に課された制限はない。それゆえ、値域の型はどんな型と仮定しても正当であり、empty :: forall a. Void -> a ということになる。残念ながら Haskell ではこのような関数を書くことはできないが、理想的には次のように書ければよい。

   
   

   empty :: Void -> a
   

   これは Haskell では禁じられている。なんとか可能そうなもっとも近いものは次のようなものだ。

   empty :: Void -> a
   empty _ = undefined
   

   もしくは、

   empty :: Void -> a
   empty = empty
   

   
   

   (やはりHaskellでは許されないのだが)ほかの理にかなった方法としては次のように書くことが考えられる。

   empty x = case x of { }
   

   
   

   これはどんなxの値も扱うことができるので、このcase 文は完全に適切な形式(well formed)である。

   
   

   関数の右辺には決して届かない(ゆえに何も渡してはいない)ので、これはまったく安全であることに注意しよう。全体の結論としては、Void -> a は空でない型であり、P が偽であるならば P → Q は真である、ということになる。

否定

論理のおける ¬ 演算は、定理を非定理に、非定理を定理に変える。もし A が定理なら ¬A は非定理であるし、A が非定理なら ¬A は定理となる。Haskell ではどうやって表現できるだろうか？回答はずるいものだ。型シノニムを定義する。

type Not a = a -> Void

だから、A について、Not A の型は単に A -> Void である。これはどのように働くのだろう？ A が定理型であれば、 A -> Void は空でない集合でなければならない。返り値の型 Void は値を持っていないので、どんな関数もどんな値でも返す方法はない(この関数は A のすべての空でない集合についても値を提供しているはずである)！言い換えれば、先ほどの章で探求したように、A が非定理だったら、A を Void に置き換えることができる。そして、関数　id :: Void -> Void　は Not A の要素であり、ゆえに要求通り Not A は定理となる(その定義域に要素がないので、この関数はどんな値も提供する必要はない。それにもかかわらず、これは空のグラフであり、関数なのだ。)。

公理的論理と組み合わせ計算

これまでのところ、Haskell の型システムからいくつかのごく基本的な機能のみを使ってきた。論理のほとんどの機能はごく基本的な「プログラミング言語」であるコンビネータ計算(combinator calculus)を使えば探求することができる。どうやってC-H がこれらの２つの領域を結びつけているかを十分に理解するためには、形式論理の議論とプログラミング言語についての議論の両方を「公理化」する必要がある。

公理的論理

→操作がどのように振る舞うべきかについてのふたつの公理から始めよう(いまから、これらの → は右結合関数である、すなわち、A → B → C は A → (B → C) を意味するものとする)。

1. A → B → A
2. (A → B → C) → (A → B) → A → C

最初の公理は、どんな２つの命題 A と B についても、もし A と B の両方を仮定するなら、A が真であるということがわかる、ということを言っている。ふたつめの公理は、もし A ならば B ならば C ならば(言い換えれば、もし C が真ならいつも A と B も真であるとすれば)、かつ A ならば B であれば、A が真であることがわかれば C が真であると結論できるということだ。これは複雑に見えるが、少し考えるとこれはごく当たり前のことであるのがわかる。様々な色の箱があり、車輪の付いているものや、蓋の付いているものもあると想像してみよう。すべての赤く車輪のついた箱には蓋があり、赤い箱には車輪がついている。ひとつ箱を選ぶ。A = '検討中の箱は赤', B = '選んだこの箱は車輪が付いている', C = '選んだ箱には蓋が付いている'としよう。ふたつめの法則は、A → B → C (すべての赤く車輪がついた箱は蓋もついている)、かつ A → B (すべての赤い箱は車輪がついている)なら、もし A (箱が赤である)ならば、C (箱には蓋が付いている)が真であるのは間違いない。

モーダス・ポネンスとも呼ばれている推論規則も認めることにする。

1. If A → B, and A, then B.　もし A → B　かつ A　なら、 B　である。　

この法則はもとの定理から新しい定理を作ることを可能にする。これはまったく明白のはずである。→ が何を意味しているかの本質的な定義そのものである。この小さな原理は、ほとんどの我々の議論をカバーする十分な表現力する、単純で十分な論理体系を提供する。このシステムにおける、A → Aの証明例を示す。

最初に、定理としてふたつの公理を知っている。

• A → B → A
• (A → B → C) → (A → B) → A → C

ふたつめの公理の左辺が最初の公理であるように見えるのに気づくだろう。ふたつめの公理は、もしA → B → Cがわかっているなら、(A → B) → A → Cと結論できることを保証する。このとき、もし C を A と同じ命題だとすれば、もし A → B → Aならば (A → B) → A → A を得る。もし B を命題 C → A とすれば、ほかの命題 C について、もし A → C → A ならば A → A を得る。しかし、繰り返すが、A → C → A (これはまた最初の公理だ)であり、ゆえに求めていた A → Aを得る。

この例の実演はいくつかの単純な公理ともとの定理から新たな定理を創りだす簡単な方法さえあれば、さらに複雑な定理を導出できることを示す。これを得るまでに随分手間がかかるかもしれない。A → A が定理であるという明らかな主張を証明するのにも何行もかかった！しかし、最終的にはたどり着いた。本質的にごく簡単なシステムを定義し、このシステムがどのように働くのかを研究するのは非常に簡単なので、この種の形式化は興味深い。

コンビネータ計算

ラムダ計算はごく簡単な原理から単純なプログラミング言語を定義する方法のひとつである。もしまだラムダ計算の章を読んでいないのであれば、少なくとも型なしバージョンの計算の導入の節だけでも読んでおくことを勧める。忘れかけているかもしれないから、念のため確認しておこう。ラムダ項はつぎの３つのうちのひとつである。

• 値, v
• ラムダ抽象 $\lambda x.t$。ここで t は別のラムダ項である。
• 適用 $(t_{1}t_{2})$。ここで $t_{1}$ と $t_{2}$ はどちらもラムダ項である。

ベータ簡約 と呼ばれる簡約規則がひとつある。

• $((\lambda x.t_{1})t_{2})$ → $t_{1}[x:=t_{2}]$。ここで、$t_{1}[x:=t_{2}]$はすべての x の自由な出現をともなう$t_{1}$は$t_{2}$で置換されることを意味する。

ラムダ計算の項目で言及したように、識別子の自由な出現の記述を束縛するのを試すときには困難が生じる。これらの困難のため、コンビネータ計算はアメリカの数学者ハスケル・カリーによって考案された(のちにプログラミング言語の名前ともなった)。基本的なコンビネータ計算にはいくつかの亜種が存在するが、ここでは最も簡単なものについて考える。ふたつのいわゆる コンビネータ と呼ばれるものから始める。

• 　K はふたつの値をとり、最初のひとつを返す。ラムダ計算においては、$\mathbf {K} =\lambda xy.\ x$　である。
• S は２引数の関数、１引数の関数、値をとり、値を１引数の関数に渡して、２引数の関数に適用する。ラムダ計算では、$\mathbf {S} =\lambda xyz.\ xz(yz)$ である。

最初の関数はconstだと認識したかもしれない。ふたつめはすこし複雑だが、((->) e) モナド(つまりは Reader だ)におけるモナディック関数 ap　である。これらふたつのコンビネータはラムダ計算全体の完全な基礎を形成する。どんなラムダ計算プログラムもこれらふたつの関数だけを使って書くことができる。

直観論理か古典論理か

これまで証明してきたすべての結果は、直観主義論理の定理である。古典論理の基本的な定理、 Not Not A -> A を証明することを試みるどうなるのであろうか。 ((A -> Void) -> Void) -> A と変換されることを思い出そう。すると、型 (A -> Void) -> Void の関数について 型Aを返すような関数が必要だ。いま、もし型 A -> Void が空である、言い換えれば 型 A が空であるなら、型 (A -> Void) -> Void の関数がまさに存在する。必要なのはなんらかの空である型をとりその型の要素を返す関数である。それぞれの型の "最も単純"、言い換えれば "最初" の要素を発見するだけであるので、コンピュータにとってはじゅうぶんに容易い。しかし、通常のラムダ計算やコンビネータの技法を使用してこれを果たす方法はない。ゆえに、これらの２つの技法を使ってこの結果を証明することができず、根本的な論理は古典論理というより直観論理であることがわかる。

代わりに、エラーが発生した時に throwを呼び出しcatchへ計算を移行する、従来のエラー処理関数を考える。 throw関数はもとの関数のどんな返り値も取り消すので、その型は A -> Void である。ここで、A はその関数の引数の型である。catch 関数は throw 関数をその引数としてとり、もし throw が例外を引き起こす(すなわち Void を返す)なら throw 関数の引数を返すだろう。そして catch の型は ((A -> Void) -> Void) -> A となる。

---