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

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

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

PLP のプログラムは形としてはPrologのプログラムで、実行順序のないものとします(以下で少しずつどういうことか説明していきます)。PLPのプログラムは論理的には

 \displaystyle \exists t_1 \exists t_2 \cdots \exists t_n d \rightarrow r

という論理式と考えることができます。ここで  r

 \displaystyle p(u_1, u_2, \cdots , u_m)

という形の式とします。 p は述語、各  u_i は項または変数です。この形の論理式を述語式と呼ぶことにします。 d

 \displaystyle a_1 \land a_2, \land \cdots \land a_k

という形の論理式で、各  a_i

 \displaystyle \forall v_{i1} \forall v_{i2} \cdots \forall v_{ih_i} (p_{i1} \land p_{i2} \land \cdots \land p_{il_i} \rightarrow q_i)

という形の論理式で、各  p_{ij} と各  q_i は述語式です。

 

PLP のプログラムを論理式と考えて、それを証明することを考えます。証明は「シークエント計算」に基づいて行っていきますが、正確な説明にはなりませんが「シークエント計算」の全体を説明すると長くなるので必要な部分だけを書いていくことにします。

 

まず上記の

 \displaystyle \vdash \exists t_1 \exists t_2 \cdots \exists t_n d \rightarrow r

を証明するには、新しい項  t'_1, t'_2, \cdots t'_n を追加して  d \rightarrow r に現れる  t_1, t_2, \cdots t_n を  t'_1, t'_2, \cdots t'_n にそれぞれ置き換えたものを  d' \rightarrow r' と書くとすると、

 \displaystyle \vdash d' \rightarrow r'

を証明すれば十分となります(「シークエント計算」の「 \exists 右」)。 d が  d(t_1, t_2, \cdots t_n) という述語、 r が  r(t_1, t_2, \cdots t_n) という述語とすると、 d' \rightarrow r' は  d(t'_1, t'_2, \cdots t'_n) \rightarrow r(t'_1, t'_2, \cdots t'_n) となります。

 

次に  \vdash d' \rightarrow r' を証明するには、 d' \vdash r' を証明すれば十分となります(「 \rightarrow 右」)。

 

 d' \vdash r' を証明するには  d', d' \vdash r' を証明すれば十分となります(「簡約左」)。

 

 d', d' \vdash r' を証明するには  d', a'_i \vdash r' をどれかの  i に対して証明すれば十分となります(「 \land左」の繰り返し)。ここで  a'_i は  a_i に同様の変換を行ったものとします。Prolog ではこの  i についての実行順序は固定となりますが、PLP ではプログラムは並行に実行されるとしてすべての  i に対して実行されるものとします。

 

 a'_i

 \displaystyle \forall v_{i1} \forall v_{i2} \cdots \forall v_{ih_i} (p'_{i1} \land p'_{i2} \land \cdots \land p'_{il_i} \rightarrow q'_i)

とおくと、

 \displaystyle d', \forall v_{i1} \forall v_{i2} \cdots \forall v_{ih_i} (p'_{i1} \land p'_{i2} \land \cdots \land p'_{il_i} \rightarrow q'_i) \vdash r'

を証明するには、新しい変数  v'_{i1} , v'_{i2},  \cdots ,  v'_{ih_i} を追加して  v_{i1} , v_{i2},  \cdots ,  v_{ih_i} v'_{i1} , v'_{i2},  \cdots ,  v'_{ih_i} でそれぞれ置き換えた

 \displaystyle d', p''_{i1} \land p''_{i2} \land \cdots \land p''_{il_i} \rightarrow q''_i \vdash r''

を証明すれば十分となります(「 \forall 左」)。

 

 \displaystyle d', p''_{i1} \land p''_{i2} \land \cdots \land p''_{il_i} \rightarrow q''_i \vdash r''

を証明するには

 \displaystyle d' \vdash p''_{i1} \land p''_{i2} \land \cdots \land p''_{il_i}

 \displaystyle q''_i \vdash r''

を証明すれば十分となります(「 \rightarrow左」)。

 

 q''_i \vdash r'' は  q''_i と  r'' が一致するときは公理となるので証明可能で一致しないときは証明できません。

 

 \displaystyle d' \vdash p''_{i1} \land p''_{i2} \land \cdots \land p''_{il_i}

を証明するには  l_i = 0 のときは公理となり証明可能で、 l_i \ne 0 のときは

 \displaystyle d' \vdash p''_{ij}

をすべての  j に対して証明すれば十分となります(「 \land右」の繰り返し)。Prolog ではこの  j についての実行順序は固定となりますが、PLP ではプログラムは並行に実行されるとしてすべての  j に対して実行されるものとします。

 

 \displaystyle d' \vdash p''_{ij}

を証明するには上記の

 d' \vdash r'

以下の議論を繰り返していきます(無限に実行するものを定義することも可能)。