コンビネータ論理
たとえば、λx.λy.(y x)をコンビネータにしてみよう。
T[λx.λy.(y x)] = T[λx.T[λy.(y x)]] (by 5) = T[λx.(S T[λy.y] T[λy.x])] (by 6) = T[λx.(S I T[λy.x])] (by 4) = T[λx.(S I (K x))] (by 3 and 1) = (S T[λx.(S I)] T[λx.(K x)]) (by 6) = (S (K (S I)) T[λx.(K x)]) (by 3) = (S (K (S I)) (S T[λx.K] T[λx.x])) (by 6) = (S (K (S I)) (S (K K) T[λx.x])) (by 3) = (S (K (S I)) (S (K K) I)) (by 4)
任意の二つの項xとyをこのコンビネータに合成すると、以下のように簡約される。
(S (K (S I)) (S (K K) I) x y) = (K (S I) x (S (K K) I x) y) = (S I (S (K K) I x) y) = (I y (S (K K) I x y)) = (y (S (K K) I x y)) = (y (K K x (I x) y)) = (y (K (I x) y)) = (y (I x)) = (y x)
(S (K (S I)) (S (K K) I))という表現は、ラムダ項としての表現λx.λy.(y x)よりもはるかに長い。これは一般的なことである。普通、T[ ]はラムダ項をΘ(n)に展開する。
この論証不明の定理からすぐに、正規形をもつ条件を満たすかどうかを決定することができる完全な述語は存在しないことが導かれる。さらに、
(EQUAL A B) = T if A = B and (EQUAL A B) = F if A ≠ B.
でのEQUALのような完全な述語は存在しないことも言える。 もしもEQUALが存在したならば、全てのAについて λx.(EQUAL x A) は完全で非自明な述語でなければならない。
この結果はコンビネータ論理の決定不能性を意味しないことに注意しなければならない。これらの結果のいうところは、コンビネータそれ自身を引数に取り(ある条件を満たす)性質を判定するコンビネータが存在しないということであり、計算論的な意味の不能性を意味するわけではない。実際、コンビネータの構文的な等価性は上の定理によればコンビネータにより判定することはできない(コンビネータ論理の定義には異なる変数記号を体系内で区別するような規則は何一つとして含まれてはいない)が、明らかに計算可能である。コンビネータ論理の決定不能性を示すには、コンビネータをゲーデル数を用いて自然数にコーディングの上で、ゲーデル数を表すコンビネータを引数に取り(ある条件を満たす)性質を判定するコンビネータが存在しないということを証明すればよい。一般に、非自明かつweak同値性に関して閉じたn-項関係は決定不能である。それゆえ、上述したような述語は、ゲーデル数を用いてもなお表現できない。その証明は最初に述べた証明を多少変更するだけで得られる。一方で、あるゲーデル数に対してコンビネータの構文的な等価性を判定するコンビネータを構成することもできる。
ラムダ計算は、ラムダ項と呼ばれる以下のような形の記号の列に関係している。
v
λv.E1
(E1 E2)
vは予め定義された変数の名前の無限集合から引き出された変数名で、E1とE2はラムダ項である。 λv.E1の形の項は「抽象」と呼ばれる。vはその抽象の仮引数、E1は本体と呼ばれる。λv.E1という項は、引数に適用されるとvをその値に束縛し、E1の結果の値を評価する。つまり、E1の中にあるvをその引数で置き換えたものを返す。 (E1 E2)の形の項は適用と呼ばれる。適用は関数の呼び出しもしくは実行を作る:E1という関数が、E2という引数で呼び出されると、その結果が計算される。もしE1(ときどきapplicandと呼ばれる)がラムダ抽象なら、その項は簡約されるかもしれない: 引数E2は、E1の仮引数の場所に置き換えられ、同値な新しい項が結果になる。もし、ラムダ項が((λv.E1) E2)の形の項を含まないのならば、それは簡約されず、β正規形と呼ばれる。 E[v := a]は、Eのvの自由変数としての出現をすべてaで置き換えた結果を表現する。したがって、
((λv.E)a) => E[v := a]
伝統的に、(a b c d ... z)を(...(((a b) c) d) ... z)の省略として表記する。(i.e. 適用は左結合である) このような定義をするのは、すべての数学的の根本的な振る舞いを捉えているからである。例えば、ある数の平方を求める関数を考えて欲しい。英語ならこのように書くかもしれない。
The square of x is x*x