fixedpoint.jp - ケーススタディ -- Prolog と型システム




ケーススタディ -- Prolog と型システム

最近 comp.lang.prolog にて多くのメッセージが寄せられたトピックが "This was memory fragmentation" です。このトピックはもともと "Prolog, memory management and memory leaks" の続きとしてポストされたものです。

題名のとおり、Prolog で組まれたサーバプログラムがメモリを消費するという話題から議論が始まったのですが、下の Joachim Schimpf による投稿

http://groups.google.com/group/comp.lang.prolog/msg/9df3c6b6ec3c0d8e
> I consider this a limitation (bug) in current Prolog compilers. Every
> Prolog compiler should compile this code into something like this:

> a(N,_) :- var(X), original_code_for_a(X).
> a(N,_) :- ( N> 0 -> .. ; ... ).

Don't forget that N > 0 and N =< 0 may both fail with ieee floats.
So to be safe you'd need some analysis too. 

の辺りから、型によるデータの整合性をチェックするという話になっています。

上のような問題の対策として、変数の値が整数である述語を利用する方法が提案されます:

http://groups.google.com/group/comp.lang.prolog/msg/5279a5b4c18608db
This is getting interesting.

If we observe that the constant 0 is an integer, then we may avoid the
problem by using:

a(N,_) :- ( integer(N) -> (N> 0 -> ... ;  ... ) ; original_code ).

or, in case we want to accept expressions that evaluate to an integer:

a(N,_) :- ( evaluates_to_integer(N,N1) -> (N1 > 0 -> ... ;  ... ) ;
original_code ).

This would allow to further simplify the code for N1>0, as no type-
checking would now be required.

But I am sure Bart will find something wrong with this :) Or he is
doing this already :)

この述語の役割は型によるチェックであり、こういった型の有用性を生かすために型の宣言を利用するべきだという意見が出ます。

http://groups.google.com/group/comp.lang.prolog/msg/f3efce26ba99e856
Given that experts (Jan, Vitor) make subtle mistakes, and given the
pitfalls of floating point arithmetic (see what Joachim wrote), and
because of the pitfalls of unification (with 0 for instance) is quite
different from arithmetic equality testing (=:= 0) ...

wouldn't the following be a better way to write fac/2:

         :- type facbartpref(nonnegint:in, int:out). % (*)

         facbartpref(0,1).
         facbartpref(N,Res) :-
                 N == 0,
                 M is N - 1,
                 facbartpref(M,Temp),
                 Res is N * Temp.

I have replaced the N > 0 by N == 0. A decent compiler should be able
to avoid choicepoints, and if statically, it cannot prove that
facbartpref is called correctly, it can insert a minimal set of tests
to ensure this.

Why is the Prolog community still so scared of type/mode declarations,
when their advantage is so obvious.
(*) modulo choice of syntax and type system

これに対するさまざまな反応;

この議論の中で最も共感できたのは、SWI-Prolog の開発者 Jan Wielemaker の次の意見です:

http://groups.google.com/group/comp.lang.prolog/msg/5cbd4f1e29d6c7a8
So my first reading was correct after all.  There is 75% characters
(or lines) of the source code that does not add to the logic but is
merely there to validate assumptions?  That is really huge.

Ok, Prolog source is overall so much shorter that the total amount of
code and readability might still not be bad ...

What is interesting now is how much of the 75% could be replaced by a
type system and how much lines are needed for the declarations that
replace these tests.

© 2006-2008 Takeshi Abe