Prolog とシーケント代数

去年も今頃授業でやっていたみたいです。関数型言語と同じで、

＊　　プログラム中での変数の論理的関係が理解しやすいように記述する

ための指針みたいなものだと思うと良いと思う。Prolog 使うとバグがなくなるとか、そんなことではなくてさ。

Prolog のbaseになっているシーケント代数の方もやるんですが、自然演繹と両方やるのはちょっとなぁ。まぁ、たいした量じゃないから両方かな。

でも別にシーケント代数やっていたら、Prolog 理解しやすくなるというわけでもなく。でも、Prolog で使う範囲だと推論規則が少なくて良いってのはあるかな。


Σ |- Q, Γ Σ' , Q |- Γ'
---------------------------------------------------------- (cut rule)
Σ , Σ ' |- Γ , Γ'

これだけだものな。

実際のProlog programmingだと多用(つうか濫用)するのは単一化の方なので、単一化を詳細にやらないのはどうなのとも思うのですが、やろうと思うと結構煩雑。

Clausal form への変換のプログラムも少し探してみたんですが、結構、複雑で、授業で紹介するにはどうなのかな。確か、Clockskin and Merish の教科書にも変換プログラム載っていたと思うんだけど、割と大変だった。

アセンブラのマニュアルとかは「ちょっと論理式かプログラムで書いてくれ」と思うことはあります。