論理プログラミングとシークエント計算の関係について以前書いていましたが、まとめてみます。
論理プログラミングで述語式の列(ゴール節) を実行するには、
、
、…、
をすべて(Prologの場合は順に)実行することになります。これは証明図で書くと以下のようになります。
これは以下の証明図のパターンの項を論理式で置き換えたものを複数組み合わせたものをまとめたものとなります。
論理プログラミングで述語式 を一つのホーン節
に対して実行することは、
が
が一致するかどうかを調べて、ゴール節
を実行することになります。これは証明図で書くと以下のようになります。
これは以下の証明図のパターンの項を論理式で置き換えたものとなります。
論理プログラミングで述語式 を実行するには、ホーン節の集合
の中の
が
と一致する一つのホーン節
を選択することになります(Prologの場合はホーン節の選択を順に実行していって失敗した場合は次のホーン節をやり直すという手順になります)。
これは証明図で書くと以下のようになります。
これは以下の証明図のパターンの項を論理式で置き換えたものとなります。
ここまでが1回分の証明図となります。論理プログラミングの動作としてはここまでですが、さらに証明を続けると以下のようになります。
これは以下の証明図のパターンの項を論理式で置き換えたものとなります。
( は
内の変項
の全ての自由出現を項
で置換した論理式を表します)
1回分の証明図をまとめて書くことを考えます。「」という形のものと論理積(ここでは
と書きます)と論理和(ここでは
と書きます)の組み合わせで書けるもの(自由分配束)を「シークエント式」と呼ぶことにします。「シークエント式」の全体を
と書きます。1回分の証明図をまとめると以下のようになります。
この推論規則を とします。
は
から
への部分写像
と考えることができます。
この逆写像を とすると論理プログラミングのプログラム
は
を満たす
が存在するとき成功となります(
は
の中の
を表すものとします)。
の元がすべて
となる
が存在するとき失敗となります(
は
の中の
を表すものとします)。
それ以外の場合は無限の回数実行されます。
をプログラム の極限と呼ぶことにします。
これで無限の回数実行されるプログラムに対する入出力は の順に記述すれば良いということがわかります(入出力の系統が一つだけの場合)。サーバー側で無限に実行されるプログラムに対する入出力をクライアント側で行う場合などの記述をすることができます。
関数プログラミングの場合も論理プログラミングに対応付けることができればこの考え方で記述することができます。これはなんとかできたと思われるのですが、もう少しちゃんとした理論にできないかと考えています。
この記事の目的はこれを半環と極限の理論で記述することで、それによって環の理論を使うことができるかもしれないので見通しが良くなると思われます。無限に動作するプログラムに入出力を組み込むデザインパターンのようなものが記述できる可能性があると思われます。