SKIコンビネータ計算
任意のコンビネータ項に対して、それと外延的に等価かつ同じ自由変数を持つラムダ項が存在する。これは、コンビネータ項に現れるすべての定数記号を、
S = λxyz.xz(yz)
K = λxy.x
I = λx.x
と置き換えれば良いから明らかである。一方任意のラムダ項に対して、それと外延的に等価かつ同じ自由変数を持つコンビネータ項が存在する。これは、命題論理におけるヒルベルトスタイルと自然演繹スタイルの証明系が等価であることと対応する(演繹定理)。
コンビネータ K および S は、よく知られた次の命題論理の公理図式と対応する:
AK: A → {\displaystyle \to } (B → {\displaystyle \to } A), AS: (A → {\displaystyle \to } (B → {\displaystyle \to } C)) → {\displaystyle \to } ((A → {\displaystyle \to } B) → {\displaystyle \to } (A → {\displaystyle \to } C)).
関数適用は推論規則モーダスポネンスと対応する:
MP: A → B , A ⊢ B {\displaystyle A\to B,A\vdash B}
公理 AK, AS 及び推論規則 MP は、直観主義命題論理の含意断片に対して健全かつ完全である。この体系に爆発原理 F → A と排中律に類する規則(例:パースの法則)を追加したものは古典命題論理と対応する。
SKIコンビネータ計算ではブール論理の計算が可能である。これは、次を満たす真(T)または偽(F)を表す閉項によって実現される:
Txy = x
Fxy = y
T と F を合せてChurch booleanという。これは具体的に次のように定義できる:
T = K
F = SK
Kxy = x
SKxy = Ky(xy) = y
真と偽を定義すれば、今やブール論理の全ての演算は if-then-else 構造によって実装できる。
入力となるChurch booleanの否定を得るには、入力に F と T を順に適用すればよい。したがって NOT は次のように定義できる:
NOT = S(SI(KF))(KT)
NOTx = S(SI(KF))(KT)x = SI(KF)x(KTx) = Ix(KFx)(KTx) = xFT
入力となる2つのChurch booleanの論理和を得るには、入力1に T と入力2を順に適用すればよい。したがって OR は次のように定義できる:
OR = SI(KT)
ORxy = Ix(KTx)y = xTy
入力となる2つのChurch booleanの論理積を得るには、入力1に入力2と F を順に適用すればよい。したがって AND は次のように定義できる:
AND = SS(K(KF))
ANDxy = Sx(K(KF)x)y = xy(KFy) = xyF