研究(1)コンビネータの型と論理学の関係

コンビネータの型について

特殊なものを除いて、コンビネータには型をつけることができます。
そして、型付けられたコンビネータは論理学と深い関係があるのです。
型をつけられないコンビネータは、自己適用をするmockingbirdやLarkなどがそうです。
今回はこれらについては触れません。
ここでは、haskellというプログラミング言語を用いて調査します。
ただし、haskellについての知識はあまり必要ではありません。
以下がプログラムです。

s :: (x -> y -> z) -> (x -> y) -> x -> z
s x y z = x z (y z)

k :: x -> y -> x
k x y = x

i :: p -> p
i x = x

b :: (x -> y) -> (z ->x) -> z -> y
b x y z = x (y z)

w :: (x -> x -> y) -> x -> y
w x y = x y y

c :: (x -> y -> z) -> y -> x -> z
c x y z = x z y

簡単に解説すると、2行ごとに1つのコンビネータを定義しています。
1行めの::以降が型情報で、2行目がコンビネータの定義になっています。

コンビネータ論理では、sとkだけでチューリング完全なことが知られていますが
bcwkの組み合わせでもチューリング完全になります。
むしろこちらの方が次の意味でわかりやすいと思います。
kは削除
wは複製
bは関数合成
cは引数のスワップ
を担当します。
sコンビネータはこれらのうち、複製、関数合成、引数のスワップを一緒くたにしたものと考えることができます。

コンビネータの型と論理学の公理との関係

上に載せたhaskellのコンビネータの定義に出てくる型は
そのまま命題論理の公理と対応しています。
AB: (B → C) → ((A → B) → (A → C)),
AC: (A → (B → C)) → (B → (A → C)),
AK: A → (B → A),
AW: (A → (A → B)) → (A → B).

また、sとkの組み合わせの場合は
AK: A → (B → A),
AS: (P→(Q→R))→( (P→Q)→(P→R) )
という公理と対応しています。
そして関数適用がモーダス・ポネンス(PとP->QからQを導く)に対応します。

haskellのソースコードのほうではカッコが少し省略されていますが
自動的に推論された型がそのまま公理と対応しているのがわかります。

さらにこれらからいくつかの公理を除去した論理学も研究されています。
例えばBCK論理では、上の公理から複製wを取り除いた論理の体系です。
こうした通常の命題論理より弱い論理体系群は部分構造論理と呼ばれています。

haskellのプログラムは型が命題、プログラムが証明に対応しています。
これをカリー・ハワード同型対応と呼びます。