コンビネータ論理 コンビネータ計算の非決定性

ウィキペディア

コンビネータ論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/10 14:50 UTC 版)

コンビネータ計算の非決定性

一般的なコンビネータ項が正規形を持つかどうか、二つのコンビネータ項が同じかどうかは判定できない。これは、対応するラムダ項における非決定性と同じである。直接的な証明は以下のようになる。 まず、以下の項を見てみよう。

       Ω = (S I I (S I I))

この項は正規形を持たない。なぜなら、以下に示すようにこれは自分自身に簡約するからである。

         (S I I (S I I))
       = (I (S I I) (I (S I I)))
       = (S I I (I (S I I)))
       = (S I I (S I I))

そして、明らかにこれ以上短い式を作る簡約はない。 正規形を検出するコンビネータNを考えてみよう。

       (N x) => T, if x has a normal form
                F, otherwise.

(TとFはチャーチエンコーディングにおける真理値を表現する。λx.λy.xとλx.λy.yで、コンビネータの形ではT = K and F = (K I)である。) そして、

       Z = (C (C (B N (S I I)) Ω) I)

(S I I Z)という項を考えてみよう。(S I I Z)は正規形を持つだろうか？それはもしこのようにしたとき、こうなる。

         (S I I Z)
       = (I Z (I Z))
       = (Z (I Z))
       = (Z Z)
       = (C (C (B N (S I I)) Ω) I Z)           (definition of Z)
       = (C (B N (S I I)) Ω Z I)
       = (B N (S I I) Z Ω I)
       = (N (S I I Z) Ω I)

今、Nを(S I I Z)に適用する必要がある。 (S I I Z)が正規形を持つか、そうでないか。もしそれが正規形を持つならば、以下のように簡約される。

         (N (S I I Z) Ω I)
       = (K Ω I)                               (definition of N)
       = Ω

しかし、Ωは正規形を持たないため、矛盾している。もし、(S I I Z)が正規形を持たないならば、このように簡約する。

         (N (S I I Z) Ω I)
       = (K I Ω I)                             (definition of N)
       = (I I)
         I

(S I I Z)の正規形は単にIであり、また矛盾を生む。したがって、仮定した正規形コンビネータNは存在できない。

ライスの定理におけるコンビネータ論理の例(原文：The combinatory logic analogue)が言うのは、完全で非自明な述語は存在しないという事である。ある述語がコンビネータであるということは、適用の際にTrueかFalseのどちらかを返すということである。もし2つのNA=TとNB=Fを満たすような2つの引数A,Bが存在するとき、その述語Nは非自明であるという。また、NMがいかなる引数Mについても正規形をしているとき、そしてその時に限り述語Nが完全であるという。ライスの定理の例は、全ての完全な述語は自明であると述べている。この定理の証明はかなり単純である。

証明:背理法による。完全で非自明な述語の存在を仮定し、N と呼ぶことにする。

Nは非自明であるから以下を満たすコンビネータA,Bが存在する。

(N A) = T
(N B) = F

Define NEGATION ≡ λx.(if (N x) then B else A) ≡ λx.((N x) B A)
Define ABSURDUM ≡ (Y NEGATION)

不動点定理により、 ABSURDUM ≡ (Y NEGATION) = (NEGATION (Y NEGATION)) ≡ (NEGATION ABSURDUM) を満たすABSURDUM = (NEGATION ABSURDUM)が与えられる。

Nは完全であるから以下の2つのうちどちらかを満たす。

1. (N ABSURDUM) = F
2. (N ABSURDUM) = T

場合1: F = F = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N A) = T これは矛盾である。

場合2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N B) = F これもまた矛盾である。

故に、 (N ABSURDUM) は真であっても偽であってもNが完全で非自明な述語であることに反する。QED。

この論証不明の定理からすぐに、正規形をもつ条件を満たすかどうかを決定することができる完全な述語は存在しないことが導かれる。さらに、

(EQUAL A B) = T if A = B and
(EQUAL A B) = F if A ≠ B.

でのEQUALのような完全な述語は存在しないことも言える。 もしもEQUALが存在したならば、全てのAについて λx.(EQUAL x A) は完全で非自明な述語でなければならない。

この結果はコンビネータ論理の決定不能性を意味しないことに注意しなければならない。これらの結果のいうところは、コンビネータそれ自身を引数に取り（ある条件を満たす）性質を判定するコンビネータが存在しないということであり、計算論的な意味の不能性を意味するわけではない。実際、コンビネータの構文的な等価性は上の定理によればコンビネータにより判定することはできない（コンビネータ論理の定義には異なる変数記号を体系内で区別するような規則は何一つとして含まれてはいない）が、明らかに計算可能である。コンビネータ論理の決定不能性を示すには、コンビネータをゲーデル数を用いて自然数にコーディングの上で、ゲーデル数を表すコンビネータを引数に取り（ある条件を満たす）性質を判定するコンビネータが存在しないということを証明すればよい。一般に、非自明かつweak同値性に関して閉じたn-項関係は決定不能である。それゆえ、上述したような述語は、ゲーデル数を用いてもなお表現できない。その証明は最初に述べた証明を多少変更するだけで得られる。一方で、あるゲーデル数に対してコンビネータの構文的な等価性を判定するコンビネータを構成することもできる。