ML & HOL
河野真治 @ 琉球大学情報工学です。
ML は、コンピュータ理論研究者御用達のプログラミング言語です。
最初に知ったのは、東大の大形計算機センタで入ったのと、それ
をゼミで説明した先輩がいたから。
型宣言をプログラムコードから推論する型推論と言うのが売りで
す。ということは、型がないのと同じ。自分で矛盾しない限りエ
ラーにならない。型推論は実は、Prolog のun ification と同じ
だから、型のないPrologと、型推論のMLとは、実は、ほとんど同
じ。
この言語が(理論研究者の間で)有名なのは、HOL という会話型定
理証明システムが、かなり早いうちから、この上で実装されてい
たから。自己矛盾的なんだけど、MLの自由な型付けが、定理証明
システムの実装を容易にしているわけ。
-1 :: [2,3,4,5];
> val it = [1, 2, 3, 4, 5] : int list
上が自分で入力したもので、ML (ここではMoscow MLという処理系)
が推論した型がint l ist として表示されている。この言語もポ
インタがない言語です。ということは、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使うぐらいなら、僕は、P rolog 使うだろう
な。上の例だと、こんな感じ。
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_a lloc がないとか言っ
てくる。install 時に mosml のbinaryからsymbolを落してしまっ
ているらしいが... 一応、動いているみたいな気もするが、もう
少し調べないとだめだな。
http://www.dina.kvl.dk/~sestoft/mosml.html
http://sourceforge.net/projects/hol/
---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科
Fnews-brouse 1.9(20180406) -- by Mizuno, MWE <mwe@ccsf.jp>
GnuPG Key ID = ECC8A735
GnuPG Key fingerprint = 9BE6 B9E9 55A5 A499 CD51 946E 9BDC 7870 ECC8 A735