Tuesday, 15 May 2007

ML & HOL



ML は、コンピュータ理論研究者御用達のプログラミング言語です。最初に知ったのは、東大の大形計算機センタで入ったのと、それをゼミで説明した先輩がいたから。

型宣言をプログラムコードから推論する型推論と言うのが売りです。ということは、型がないのと同じ。自分で矛盾しない限りエラーにならない。型推論は実は、Prolog のunification と同じだから、型のないPrologと、型推論のMLとは、実は、ほとんど同じ。

この言語が(理論研究者の間で)有名なのは、HOL という会話型定理証明システムが、かなり早いうちから、この上で実装されていたから。自己矛盾的なんだけど、MLの自由な型付けが、定理証明システムの実装を容易にしているわけ。

-1 :: [2,3,4,5];
> val it = [1, 2, 3, 4, 5] : int list

上が自分で入力したもので、ML (ここではMoscow MLという処理系)が推論した型がint list として表示されている。この言語もポインタがない言語です。ということは、GCがある言語ってことだな。

- fun zip(l1,l2) =
if null l1 orelse null l2 then []
else (hd l1,hd l2) :: zip(tl l1,tl l2);
> val zip = fn : 'a list * 'b list -> ('a * 'b) list

- zip([1,2,3],["a","b","c"]);
> val it = [(1, "a"), (2, "b"), (3, "c")] : (int * string) list

とかになると、ほとんど意味不明だけど、orelse みたな便利な構文が多いのも特徴です。hd が carで、tl が cdr 。:: が cons というと、LISPを知っている人はわかるはず。

ちょっと面白いのは、curry 化が入っている。f(a,b) という複数の引数の関数を、g = f'(a) という関数が返す関数g を使って、(f'(a)) (g) みたいに書ける。つまり、特殊化した関数を返すことが出来ます。どんな風に実装しているかは、あまり考えたくないが...

- fun curried_zip l1 l2 = zip(l1,l2);
> val curried_zip = fn : 'a list -> 'b list -> ('a * 'b) list

- fun zip_num l2 = curried_zip [0,1,2] l2;
> val zip_num = fn : 'a list -> (int * 'a) list

- zip_num ["a","b","c"];
> val it = [(0, "a"), (1, "b"), (2, "c")] : (int * string) list

ってな感じ。

個人的には、あまり好きな言語ではないです。HOLも難しすぎるというのが印象。でも、論理を勉強するなら、やっておけば? ってなところですね。ML使うぐらいなら、僕は、Prolog 使うだろうな。上の例だと、こんな感じ。

SICStus 4.0.0 (i386-darwin-8.8.1): Thu Mar 1 22:07:26 CET 2007
Licensed to SP4ie.u-ryukyu.ac.jp temp
| ?- [user].
% compiling user...
| zip([],_,[]).
| zip(_,[],[]).
| zip([H1|T1],[H2|T2],[(H1,H2)|T3]) :- zip(T1,T2,T3).
|
| zip_num(I,O) :- zip([0,1,2],I,O).
| ^D
% compiled user in module user, 0 msec 632 bytes
yes
| ?- zip([1,2,3],[a,b,c],X).
X = [(1,a),(2,b),(3,c)] ?
yes
| ?- zip_num([a,b,c],X).
X = [(0,a),(1,b),(2,c)] ?
yes
| ?- zip(X,Y,[(1,a),(2,b),(3,c)]).
X = [1,2,3],
Y = [a,b,c|_A] ? ;
X = [1,2,3|_A],
Y = [a,b,c] ? ;
no
| ?-

ソフトウェア工学では、(他で教えないから仕方なく) 論理も教えているんだけど、その一環で使う気だったんだが、install めんどくさすぎ〜 epkg にいれるか。

MLの処理系は、Standard ML, ocaml, NewJersey ML とかあるが、HOLは、Moscow MLがお勧めらしい。OS X でも動くようですが、HOLの muddy.o のDynamic loading で、stat_alloc がないとか言ってくる。install 時に mosml のbinaryからsymbolを落してしまっているらしいが... 一応、動いているみたいな気もするが、もう少し調べないとだめだな。

http://www.dina.kvl.dk/~sestoft/mosml.html

http://sourceforge.net/projects/hol/

No comments: