演繹定理とコンビネータ

演繹定理（英: Deduction theorem）とは、数理論理学において、論理式 E から 論理式 F が演繹可能ならば、含意 E → F が証明可能である（すなわち、空集合から演繹可能）、というもの。
公理的命題論理では、公理図式として次のものを使うのが一般的である（ここで、P、Q、R は任意の命題）。
* 公理 1 : P→(Q→P)
* 公理 2 : (P→(Q→R))→( (P→Q)→(P→R) )
* モーダスポネンス : P と P→Q から Q を推論する。
これらから明らかに公理図式 P→P が得られる（命題論理参照）。
カリー・ハワード対応では、上述の演繹メタ定理についての変換過程は、ラムダ計算の項から組合せ論理の項への変換に類似している。ここで、公理1がKコンビネータに対応し、公理2がSコンビネータに対応する。Iコンビネータは公理図式 P→P に対応する。

http://ja.wikipedia.org/wiki/%E6%BC%94%E7%B9%B9%E5%AE%9A%E7%90%86

KコンビネータとSコンビネータの型がそれぞれ公理1,2に対応することをHaskellの型推論で確認する。

Prelude> let k x y = x
Prelude> :t k
k :: t -> t1 -> t
Prelude> let s x y z = x z (y z)
Prelude> :t s
s :: (t1 -> t -> t2) -> (t1 -> t) -> t1 -> t2

->は右結合だから括弧を明示的に書くと・・・

k :: t -> (t1 -> t)
s :: (t1 -> (t -> t2)) -> ((t1 -> t) -> (t1 -> t2))

おお、ほんとだ。