コンビネータ論理
コンビネータの項からラムダ項への変換L[ ]は自明である。
これは、前述のT[ ]の逆変換ではないことに注意。
一般的なコンビネータ項が正規形を持つかどうか、二つのコンビネータ項が同じかどうかは判定できない。これは、対応するラムダ項における非決定性と同じである。直接的な証明は以下のようになる。 まず、以下の項を見てみよう。
この項は正規形を持たない。なぜなら、以下に示すようにこれは自分自身に簡約するからである。
そして、明らかにこれ以上短い式を作る簡約はない。 正規形を検出するコンビネータNを考えてみよう。
(TとFはチャーチエンコーディングにおける真理値を表現する。λx.λy.xとλx.λy.yで、コンビネータの形ではT = K and F = (K I)である。) そして、
(S I I Z)という項を考えてみよう。(S I I Z)は正規形を持つだろうか?それはもしこのようにしたとき、こうなる。
今、Nを(S I I Z)に適用する必要がある。 (S I I Z)が正規形を持つか、そうでないか。もしそれが正規形を持つならば、以下のように簡約される。
しかし、Ωは正規形を持たないため、矛盾している。もし、(S I I Z)が正規形を持たないならば、このように簡約する。
(S I I Z)の正規形は単にIであり、また矛盾を生む。したがって、仮定した正規形コンビネータNは存在できない。
ライスの定理におけるコンビネータ論理の例(原文:The combinatory logic analogue)が言うのは、完全で非自明な述語は存在しないという事である。ある述語がコンビネータであるということは、適用の際にTrueかFalseのどちらかを返すということである。