人工知能的論理プログラミング(7) - エレファント・ビジュアライザー調査記録

並行論理プログラミングと半環

「論理プログラミング」では PLP と PLP+ というプログラミング言語を考えています。PLP は「Prolog について」のところで書いたような理想的な並行 Prolog です。PLP+ はこれの無限に実行できるバージョンなのですが、PLP が定義されていないので PLP+ も定義されていません。PLP+ はいったい何なのかというと、「素数を登録するプログラム」のようなものが書けるように Prolog を拡張したプログラミング言語を目指したものです。

以下のような問題を考えます。

PLP は定義できるか
PLP で論理式が証明できるかどうかを調べることができるか

2は「不完全性定理」で調べた「チューリング機械の停止問題」の問題があるので、(まだ PLP を定義していないのですが)できないと考えられます。その代わりに

PLP が有限回で終了して結果が真 $\iff$ 論理式が証明できる

という問題を考えることができます。

まず、PLP のプログラムを単純化して考えます。

Prolog のプログラムを単純化して
$\begin{matrix} h_1 & :- & t_{11}, & \cdots, & t_{1n}. \\ \vdots & & \vdots & & \vdots \\ h_m & :- & t_{m1}, & \cdots, & t_{mn}. \\ \end{matrix}$
とします。これを項 $x$ に論理式
$\begin{matrix} h_1=x & \land & t_{11} & \land & \cdots & \land & t_{1n} & \lor \\ \vdots & & \vdots & & & & \vdots & \\ h_m=x & \land & t_{m1} & \land & \cdots & \land & t_{mn} \\ \end{matrix}$
を対応させる写像
$\begin{matrix} x & \mapsto & h_1=x & \land & t_{11} & \land & \cdots & \land & t_{1n} & \lor \\ & & \vdots & & \vdots & & & & \vdots & \\ & & h_m=x & \land & t_{m1} & \land & \cdots & \land & t_{mn} \\ \end{matrix}$
とみなします。これを
$\begin{pmatrix} h_1 & t_{11} & \cdots & t_{1n} \\ \vdots & \vdots & \ddots & \vdots \\ h_m & t_{m1} & \cdots & t_{mn} \\ \end{pmatrix}$
と書くことにします。項 $u$ が写る先
$\begin{matrix} h_1=u & \land & t_{11} & \land & \cdots & \land & t_{1n} & \lor \\ \vdots & & \vdots & & & & \vdots & \\ h_m=u & \land & t_{m1} & \land & \cdots & \land & t_{mn} \\ \end{matrix}$
を
$u * \begin{pmatrix} h_1 & t_{11} & \cdots & t_{1n} \\ \vdots & \vdots & \ddots & \vdots \\ h_m & t_{m1} & \cdots & t_{mn} \\ \end{pmatrix}$
と書くことにします。
$P' = \begin{pmatrix} h'_1 & t'_{11} & \cdots & t'_{1n} \\ \vdots & \vdots & \ddots & \vdots \\ h'_m & t'_{m1} & \cdots & t'_{mn} \\ \end{pmatrix}$ と $P = \begin{pmatrix} h_1 & t_{11} & \cdots & t_{1n} \\ \vdots & \vdots & \ddots & \vdots \\ h_m & t_{m1} & \cdots & t_{mn} \\ \end{pmatrix}$
に対して $P' * P$ を項 $x$ に論理式
$\begin{matrix} h'_1=x & \land & t'_{11} * P & \land & \cdots & \land & t'_{1n} * P & \lor \\ \vdots & & \vdots & & & & \vdots & \\ h'_m=x & \land & t'_{m1} * P & \land & \cdots & \land & t'_{mn} * P \\ \end{matrix}$
を展開して選言標準形にしたものを対応させる写像とします。これを展開と呼ぶことにします。展開をChatGPTでやってもらおうとしましたが、うまくできませんでした。展開を有限回繰り返したものの各「連言」を順に実行する(「選言」については並行に実行)とどうなるのか、ということを考えます。これで論理式の証明ができるのかということをChatGPTで聞いてみましたが、あまり良い答えは返ってきませんでした。これは無限ループになる可能性があると考えられますが、よくわかりません。今後考えていきます。