この記事の問いと内容
論理と計算との間には深い関係がある。現在のコンピュータサイエンスでは、その応用範囲は広い。
・計算可能であるとはどういうことか？
→理念
・具体的には、どのようにして計算は行われるのか？
→計算モデル論
・計算手順をうまく記述するにはどのような言語が必要か？
→プログラミング言語論
・課題を効率的に解くにはどうすればいいか？時間やメモリはどうすべきか？
→アルゴリズム、計算の複雑さの理論
・計算の正しさを保証するにはどうしたらよいか？
→検証論
などの問いが浮かび上がってくる。その中でも、今回の記事では、カリーハワード同型対応と呼ばれる、論理とプログラムの関係に迫りたい。
証明＝プログラムとはどういうことだろうか？
ぜひ目次を見てみてほしい。
論理の哲学 知の教科書
「論理」というものについて、幅広い話題が楽しめるとても貴重な一冊だと思う。悲しいことに現在は絶版のよう。この本の一部については、次の記事でまとめている。
こちらの本の「計算と論理」の章からまとめさせてもらう。「コンピュータは数学者になれるのか？」と同じ、照井一成氏が執筆している。
証明を形式化した「自然演繹」、関数型言語のもとになっているラムダ計算について知っている人は、イメージしやすい話だと思う。
それでは、論理と計算の間にある不思議な対応関係についてみていこう。
プログラムと論理の関係
プログラムの正しさを保証するには、エラーを絶対に出したくない。
「型」のエラーが起こりがち。整数型と文字列型を足し合わせたりはできない。
関数にも型をつけて、型が合っている時だけ演算できるようにする。そのために、関数適用規則を定義する。
この規則は、型に注目してみると、「論理法則」とも捉えられる。
つまり、型＝論理式と解釈できる！！
さらに、関数型プログラミングでは、関数を構成する際に、型をチェックする。そうして、プログラムは、構成規則を繰り返し適用して得られる。これは、「証明」で言うところの、推論規則の適用に対応する。
つまり、プログラム＝証明となる。
関数型プログラミングの本体とは、ラムダ計算を実行することである。その計算を一歩進めることを、ラムダ計算では簡約という。
関数 λx. ( ( × x)( ( + x) 5)) に9を適用してみる。
(λx. ( ( × x)( ( + x) 5) ) 9)
( ( × 9)( ( + 9) 5) )
(( × 9) 14)
126
簡約のイメージがつかめるだろうか？
この簡約を、論理の言葉で言い換えることはできるか？？
証明の簡略化である。
プログラムの実行=証明の簡略化となる。
カリーハワード同型対応
カリーハワード同型対応
自然演繹 型付ラムダ計算
論理式 ＝ 型
証明 ＝ ラムダ項(プログラム)
証明の簡略化 ＝ ラムダ項の簡約(プログラムの実行)
型付ラムダ計算と自然演繹は、記法が異なるだけで、実際には同じもの！！
「プログラムを書く」ことと、「証明をする」ことは同じになる！
対応関係の不思議
真理性を保証する静的な証明と、アルゴリズムを実行する動的なプログラム。形式化すれば、それらは同型になる。
なぜこのような同型性が成り立つのだろうか？
・自然演繹
論証において使われるテクニックを自然に表現するために作られた体系
・ラムダ計算
関数を定義したり値を求めたりといった数学者の関数使用の営みを理想化したもの
自然演繹とラムダ計算の対応には、深い事情がありそう。
数学の証明の中には、プログラムと見ることのできるものがある。「素数は無限に存在する」の証明などもそう。次々により大きい素数を構成していくことで、証明する。まるで、プログラムを書くイメージに近い。
カリーハワード同型対応とは、証明とプログラムの間に見られるこの緩やかな対応関係を、形式化を通じて純度の高い形で抽出したものに他ならない。
さらに、カリーハワード同型対応のおもしろいところは、証明とプログラムの間の対象レベルの対応関係であるにとどまらず、証明についての理論とプログラムについての理論の間のメタレベルの対応関係としてもあらわれるところだ、と著者は指摘している。
最後に著者の印象的な指摘を引用させてもらう。計算と論理の深い関係が示唆されていておもしろい。
「論理には興味あるけれども計算には興味ないからそんなことはどうでもいい」という人もいるかもしれない。しかし証明とプログラムの同型性を通じて、計算はあらかじめすでに論理の一部なのである。そして、しばしば永遠普遍の必然性を持つものとして崇められている「正しい推論」ですら、計算的要素を含むダイナミックな証明によって支えられているのである。このことの発見は、それ自体驚くべきことなのではないだろうか。
おすすめ記事
さらに、論理と計算の関係について深掘りしたい人は、次の記事がおすすめ。
数理論理学の「自然演繹」の考え方に触れたいかたには、次の記事をすすめたい。
幅広く、計算機科学について知りたい方には、次の記事でおすすめな本を紹介している。
ラムダ計算については、次の本がとてもくわしい。
