人気ブログランキング | 話題のタグを見る

カリー・ハワード同型対応

カリー・ハワード同型対応とは、

プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。

要するに、型付きラムダ計算のプログラムを作ると、プログラムは命題論理学の証明に対応し、プログラムの型は命題に対応しているということだ。どうやら、型付きラムダ計算でプログラムを作って、そのうちの型シグネチャーを取り出すと、論理学の証明になってしまうらしい。

例えばデータ型が B 型のラムダ項 M があって、それをデータ型 A の変数で関数抽象すると次のようになるが、

[x : A]
...
M : B
-------------
λx.M: A -> B

という型付きラムダ計算のプログラムは、論理学の推論の

[A]
...
B
-------------
A -> B

と対応している。また、関数適用もつぎのように modus ponens と対応している。

M : A -> B, N : A
----------------------
M N : B

A -> B, A
-----------------
B

データ型と命題が対応していると言われても、何それ?という感じがするが、データ型 A のことを考えるとこれは {x | x ∊ A} という集合だ。x ∊ A という命題は、x が A に属していれば x ∊ A は真になる。

ラムダ項 N の型が A であるということは、ラムダ項 N について N ∊ A は真であるということを意味する。またラムダ項 M が A -> B 型の関数であるということは、M を 任意の N ∊ A に関数適用したときその値は全て型 B であるということを意味している。すなわち N ∊ A であれば、M N ∊ B である。

そこで命題 A を x ∊ A とおき、命題 B を y ∊ B と置くと、関数型 A -> B は x ∊ A ならば Mx ∊ B という命題であり、任意の x ∊ A について、Mx ∊ B であるということになり、命題 A が真であれば命題 B が真であることが分かる。すなわち A -> B, A => B である。

また、x ∉ A であれば、A -> B は型エラーとなるので A -> B が真であるという仮定は失われる。modus ponens は A -> B と A が同時に真であるときにのみ B が真であるという推論は正しい。

型 A や 型 B には任意の集合を取ることができるから、これらは x ∊ A や y ∊ B によって任意の命題に変えることができる。M N という関数適用は x と y の間に y = M x という関係を定義するが、これは A -> B という関数型によって抽象化される。このことは、逆に A -> B によって示される命題の含意について、集合 A と 集合 B の内的な関連性を示唆する。

関数型プログラミングと論理学の間には、単なる同型対応だけではなく、意味論的にも関連があるような気がする。


by tnomura9 | 2019-11-01 18:52 | ラッセルのパラドックス | Comments(0)
<< 含意と関数 集合と要素の所属関係のみですべ... >>