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

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

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

ここでは  unify(x, y) は単に項  x y が一致するとき true 、そうではないとき false となるものとします。 unify(x, y) を述語式で表す方法については後で述べる予定です。Prolog の単一化についても後で述べる予定です。

プログラムが成功するときは、論理式として見ると証明図を書くことができて、逆に証明図を書くことができれば、プログラムとして見ると成功するということを見ていきます。

PLP では終了しないプログラムも許すとしているのでこれ以上のことは言えないのですが、もしすべてのプログラムが終了するとすればプログラムが失敗するならば論理式として証明図を書くことができず、逆に論理式として証明図を書くことができないならばプログラムとして失敗するということが言えます。