カリー=ハワード同型対応(Curry-Howard correspondence / Curry-Howard isomorphism)とは、プログラムと数学の定理が対応するという理論である。
概要
カリー=ハワード同型対応とは、入力(引数)や出力(戻り値)の「型」が命題に、プログラムが命題の証明に対応するという理論である。定理証明によるプログラム検証の理論的根拠にあたる。
カリーは純粋関数型言語Haskellやカリー化にその名を残すHaskell B. Curry、ハワードはHaskell B. Curryの提唱した理論を発展させて本理論の形にした論理学者William Alvin Howardの名前に由来する。
どういうことなの?
上記理論をそのまま現在流通しているプログラムにあてはめるなら、整数を引数にとって整数を返す関数は、整数型というのが前提と結論の命題、関数が前提から結論すなわち「(整数型)ならば(整数型)である」の証明ということになる。それなんてトートロジー?
実は上記は必要なものがかなりいっぱい省略されている。
型について
まず「型」という言葉だが、ここでいう型というのは通常の静的型付けプログラミングでいう型よりもかなり広い概念である。通常「型」というと整数型・文字列型や、オブジェクトなどのように型を組み合わせたデータ型を考えると思うが、ここでいう型にはもっと細かい条件をつけることができる。
単純な例からいくと、自然数のように「1以上の整数」型のような型を設定することができる。もう少し複雑な例を挙げると「昇順に並べられた整数のリスト」型という型も可能である。さらには出力を意識した型として、「入力の総和に等しい整数」型というものすら許される。
また、その処理系で扱える整数が符号付き32ビットまでなどの制限を受けている場合は「整数型」も「-231 〜 231 - 1 の整数」型のようになる。
主語について
型は命題であると述べたが、上記で(整数型)と書いた部分は主語がないので命題とは言い難い。命題とするには(入力が整数型)とか(出力が整数型)のように主語を補う必要がある。少なくとも出力の型については前述のように型に関する追加条件が付加されて(出力が「特定の条件を満たす」整数型)のようになる。
述語について
(入力が整数型)ならば(出力が「特定の条件を満たす」整数型)ということをもう少し命題らしくしたら、
(入力が整数型)ならば「その全ての」入力について、(出力が「特定の条件を満たす」整数型)となる出力方法が「少なくとも一つ存在する」。
この出力方法が存在することは、(入力が整数型)ならば(出力が「特定の条件を満たす」整数型)であるプログラムを実際に示す(実例を提示する)ことによって証明される。ということで、プログラミングと定理証明がつながるのである。
例
リストをソートする関数だと、「入力がリストならば、出力がソートされたリストになる関数が存在する」ことをソートアルゴリズムの存在を示すことで証明する形になるが、既出
なのでここでは整数の絶対値をとる関数について考えてみることにする。
整数の絶対値については |a|2 = a2 かつ |a| ≥ 0 を定義として利用することにする。
前提となる命題(型)は「入力 x が整数である」、結論となるべき命題(型)は「出力 |a| は |a|2 = a2 かつ |a| ≥ 0 を満たす」となる。証明すべきことは、「入力 x が整数なら、すべての x について、 abs(x)2 = x2 かつ abs(x) ≥ 0 となる関数abs(x)が少なくとも一つ存在する」である(これも一つの命題である点については考察3で触れる)。
証明1
x ≥ 0 のとき abs(x) = x, x < 0 のとき abs(x) = -x と定義すれば、定義した abs(x)はabs(x)2 = x2 かつ abs(x) ≥ 0 を満たす。よって関数abs(x)が少なくとも一つ存在することが証明された。
証明2
abs(x) = √x2 と定義すれば、定義した abs(x)はabs(x)2 = x2 かつ abs(x) ≥ 0 を満たす。よって関数abs(x)が少なくとも一つ存在することが証明された。
考察1
証明1に対応するプログラムはabs(x) = if (x ≥ 0) x else if (x < 0) -x のようなコードになり、証明2に対応するプログラムはabs(x) = sqrt(x^2) のようなコードに対応する。(特定の言語に偏らないために文法はわざといい加減に書いています)
考察2
ところで、abs(x)が整数であることを証明していないことにお気づきだろうか。証明されていない以上、abs(x)の型はあくまでも「整数xの絶対値」型であって整数型ではない。あとでabs(x)が整数であることを利用したプログラムを書こうというのであれば、abs(x)が整数であることも証明に加えなければならない。
逆に考えると、その後のプログラミングで必要にならない性質は(仮に戻り値にその性質が備わっていたとしても)証明する必要はないともいえる。
考察3
「入力 x が整数なら、すべての x について、 abs(x)2 = x2 かつ abs(x) ≥ 0 となる関数abs(x)が少なくとも一つ存在する」も一つの命題である点についてはすでに述べた。命題は対応する型があるということになるが、この型はいわゆる関数型であり、これを引数とすると高階関数によるプログラムが現れる。
考察4
型の条件を考えることが、ユニットテストや契約プログラミングでいう事前条件や事後条件を考えることに対応しているといえなくもない。
考察5
静的型付けによる型安全の理論は、考え方によってはカリー=ハワード同型対応の不完全な実現というように考えることができるのかもしれない。
そういった見地にたてば、いわゆる「内部で変化する「状態」を持つ」ということは、Aという型が存在した場合、カリー=ハワード同型対応では状態BにおけるA(B)型と状態CにおけるA(C)型というものは別の型であるべきなのに、言語仕様上は同じA型となり、型チェックをすり抜けて型安全を破壊してしまうのでよくないというように考えることができるといえる。
限界
命題は真偽を決定できるものであるが、実際には真偽を決定できない命題も存在する。そういった命題は本理論や定理証明の対象外となる。あるいは、新たな公理を持ち込むことで証明可能になるかもしれない。
また、考察1でもすでに述べたが、証明は少なくとも一つ存在していることを示すだけで、それが唯一無二で最適化された方法であることを示しているわけではない。たとえばソートだと、アルゴリズムが変われば証明方法が異なるが、いずれでも定理証明が成立する(ボゴソートは前述の真偽の決定可能性問題に触れそうな気もするが)。「最適の方法であること」を命題に織り込んで証明するという考え方もあると思われるが、まだそのレベルまでは到達していないのが現状であると思われる。
関連項目
- 2
- 0pt
