Prologとつき合う - Yet Another Ranha

C81 3日目東ペ06a - COMFRK VOL. 3 ( http://comfrk.info/ )の宣伝のつもりで書き始めてます。

えーと記事のタイトルは「年末年始Prolog入門モドキ by ranha」ということになっていますが、嘘ですんで…。

ネムインダ

最近、SWI-Prologでは次のようなプログラム片がtrueを返すようになりました。

p :- p.

?- p.
true ;
true ;
true ;
...

ウウーン良いですね。いや…ダメだよコレは。
ということを、ぼくの担当分で紹介しています。といっても入門記事なので全く新規性のある話をしているわけではないのですが。

ここまでが記事の紹介です。
C81 3日目東ペ06aに来てくださいね！！

この後は記事の目論みといいますかなんというか…。

所謂Prologのプログラムのセマンティクス(意味)というのをどのようにして与えるかと言われると、
「普通は」プログラムのあーだこーだを取った時の最小不動点がマサにソレだ(否定を入れると話は危険な領域に突入するのですが)という事に成ります。

ちなみに、上のプログラムの最小不動点は「何も無い。空集合」です。
ですから、そのような「何も分からない」ところから「pが成り立つ」ということが分かるのは非常に悪いわけですね。

ところが上をご覧の通り成り立っていまして…ていうのはこれもまた嘘で。
実はプログラム全体は次のようになっております。

:- use_module(library(coinduction)).
:- coinductive p/0.

p :- p.

刮目せよ！！！！
SWI-Prologのバージョンなんたら(少なくとも5.10.4)からは、なんとcoinductionが使えるようになっています。
結構お粗末な感じではありますが…。

でこのcoinductionが使えると何が嬉しくなるのかというと、今迄皆さんが生死を共にして来た"occur check無しのunification"が水を得た魚に成ると。

例えば、またしても次のプログラム。

num(z).
num(s(X)) :- nat(X).

まぁ自然数かどうかをチェックする代物なのですが、ここでX = s(X)の等式を満たす悪魔じみた数X(ωと呼ぶと見栄えが良いですが)を渡すと

?- X = s(X) , num(X).

絶対に返ってきません。
まぁそもそもこれで返ってくるとエラいこっちゃという話なのですが。(元のプログラムの意味を最小不動点に依るものとすると、自然数しか含まないので化け物は含まれない為)

ここでお呪いを唱えます！！

:- use_module(library(coinduction)).
:- coinductive num/1.

num(z).
num(s(X)) :- num(X).

?- X = s(X) , num(X).
X = s(X) ;
X = s(X) ;
X = s(X) ;
X = s(X) .

ヤッタゼ！！！

ということで、こういう「無限サイズの項」が扱えるようになります。ωは無限サイズですけど、任意の自然数は高々有限サイズですよね。

こういうのは一体何の役に立つのかというと、まぁ非常に自明ですが有名な例として、「ストリーム」があるでしょう。

bit(0).
bit(1).
stream([H|T]) :- bit(H) , stream(T).

まぁリアルなプログラムを書いてるとこういう「無限サイズのデータ」が扱いたくなるようです。
例えば、0が無限に続いてるとストリームですか? とPrologにおたずねすると

?- X = [0 | X] , stream(X).

話に成りません。いや、ならないで然るべきなのですが。しかしここで、またしてもお呪いです。

?- X = [0 | X] , stream(X).
X = [0|X] ;
X = [0|X] ;
X = [0|X] .

やりました！！

こういうCo-Logicなアプローチというのは最近ぼくの中では非常に流行っていまして、
例えば"Coinductive Logic Programming for Type Inference"(http://www.computing.dundee.ac.uk/staff/katya/TYPES11.pdf)、
これを紹介するのは反則な気もするのですが、兎に角色々面白いところです。

かようなプログラムに関するお話を読む時の基本は、coinduction云々は勿論ありますが、まずは何より普通のエルブランモデルですとか、最小不動点意味論に馴染みがあるかどうかという所が大きい話だと思いますので、最も基本的なエルブランの定理(モデルの方の。スコーレムの基本定理と書いた方が宜しいでしょうか)の証明を書散らしたみたいな感じになっています。