エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

論理プログラミング(7)

PLP のデータとなる項を定義します。

記号の有限集合  C があってその元を定数と呼びます。定数は項となります。

記号の可算集合  V があってその元を変数と呼びます。変数は項となります。

記号の有限集合  F があってその元を関数と呼びます。関数  f に対して  f(t_1, t_2, \cdots , t_n) という形の記号の列は項となります。ここで  t_1, t_2, \cdots , t_n は項です。

以上で定義された最小のものが項となります。項全体の集合を  T とおきます。

 

関数は変数に依存した項を表すためのもので、「シークエント計算」のところでは説明していなかったのでこの後説明していくことにします。

 

次に PLP のプログラムを定義します。

記号の有限集合  P があってその元を述語と呼びます。述語  p に対して  p(t_1, t_2, \cdots , t_n) という形の記号の列はを述語式と呼ぶことにします。ここで  t_1, t_2, \cdots , t_n は項です。述語式全体の集合を  Q とおきます。

 \displaystyle h :- q_1, q_2, \cdots , q_n .

の形の列をホーン節と呼びます。ここで  h, q_1, q_2, \cdots , q_n は述語式です。これは

 \displaystyle q_1 \land q_2 \land \cdots \land q_n  \rightarrow h

という論理式を表しています。以下では論理式の意味で使うこともあります。 n=0 の場合もあり、これは

 \displaystyle h .

と書きます。

ホーン節の  h がない場合は  h が「偽」の場合を表し

 \displaystyle \lnot ( q_1 \land q_2 \land \cdots \land q_n  )

という論理式を表します。これをゴール節と呼び Prolog では

 \displaystyle ?- q_1, q_2, \cdots , q_n .

と書きます。これはホーン節には含めないことにします(通常は含めるようですが)。

PLP のプログラムは有限個のホーン節と1個のゴール節からなります。ゴール節は1個の述語式からなるものを考えます。複数の場合

 \displaystyle r :- q_1, q_2, \cdots , q_n .

をゴール節に追加してゴール節は  r だけにすることができます。

 

次に PLP で使う論理式を定義します。

述語式全体の集合  Q によって自由生成される半環を  E とおきます。これは Q を含む最小の半環で  Q の元と2項演算子  \land \lor で書くことができるものの全体になります。 E は分配法則が成り立つので  E の元は

 \displaystyle (q_{11} \land q_{12} \land \cdots \land q_{1m_1})

 \displaystyle \lor

 \displaystyle (q_{21} \land q_{22} \land \cdots \land q_{2m_2})

 \displaystyle \lor \cdots \lor

 \displaystyle (q_{2n} \land q_{n2} \land \cdots \land q_{nm_n})

という形に書くことができます。この形を選言標準形と呼びます。

 \displaystyle (q_{i1} \land q_{i2} \land \cdots \land q_{im_i})

を連言節と呼ぶことにします。 E の元は選言標準形で書かれていると考えることにして、 E の元を正規化された論理式と呼ぶことにします。

 

次にシークエント計算のところで見た  d' \vdash r'から d' \vdash p''_{ij}までの議論について見てみると、PLP のプログラムはある述語式に正規化された論理式と対応させる写像

 \displaystyle d: Q \rightarrow E

と考えることができます。この写像を拡張して

 \displaystyle d: E \rightarrow E

と考えます。この写像微分と呼ぶことにします。微分  d と述語式  r に対して可算個の列

 \displaystyle (r, d(r), d^2(r), \cdots)

を考えて、これを  r d による極限と呼び、 exp(d, r) と書くことにします。

 

この極限を使って関数プログラミングオブジェクト指向プログラミングを表すとどうなるかというのがここでの議論の目的となるので、後で考えていくことにします。

 

次に PLP のプログラムと証明の関係について考えていきます。

項の定義で変数を含まないように定義したものを変数を含まない項と呼びその全体の集合を  T' とおきます。 V から  T' への写像 E から  E への写像に拡張したものを代入と呼びます。 S を代入全体の集合とし、 P(S) をその冪集合とします。

 

正規化された論理式  e に対して

 e unify(x, y) という形の述語式以外の述語式を true で置き換えたものを  e \uparrow

 e unify(x, y) という形の述語式以外の述語式を false で置き換えたものを  e \downarrow

と書きます。 \mu : E \rightarrow P(S) e \in E \sigma(e) が true となる代入  \sigma 全体の集合に写す写像とします。

 \mu(d^n(r) \uparrow) = \phi となる  n が存在するときこのプログラムは失敗(証明できない)、 

 \mu(d^n(r) \downarrow) \ne \phi となる  n が存在するときこのプログラムは成功(証明可能)、

任意の  n に対して  \mu(d^n(r) \uparrow) \ne \phi かつ  \mu(d^n(r) \downarrow) = \phi のときこのプログラムは無限に実行されます(終了しない)。