2 OCaml toplevel basics - ATPとCASのこと

　今回からしばらく
『HOL Light Tutorial (for version 2.20)』
http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf
に従って話を進めます．なお，リファレンスはこちら
『The HOL Light System REFERENCE』
(For HOL Light 2.20++ November 2, 2011)
http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf
です．
　まずは，HOL Lightが乗っているOCamlのtoplevel loopについてです．
　toplevel loopとは，ユーザーの入力をOCamlに送り，その結果をユーザーに返す作業を繰り返す，Mathematicaで言えばフロントエンドに相当するものです．
　toplevel loopで行えることは，大まかに言って次の３つです．以下は，OCamlのtoplevel loopをocamlとして起動後，#use "hol.ml";;と入力，ロードが完了

Camlp4 Parsing version 3.09.0

と表示された状態からの例です．
（１）issue directives
　例えば，Libraryディレクトリにあるanalysis.mlというファイルをロードするには

#use "Library/analysis.ml" ;;

システムのコマンドを実行するには

Sys.command("システムのコマンド") ;;

loopを終了するには

#quit ;;

とします．
（２）evaluate expressions
　例えば

2 + 2;;
val it : int = 4

と評価されて，直前の結果は，itとして参照でき，今の場合

it * it;;
val it : int = 16

となります．このit:intというのはitつまり16のtypeがintであるということで

16.;;
val it : float = 16.
"16";;
val it : string = "16"

といった違いがあり，例えば，floatの割り算は

16. /. 2. ;;
val it : float = 8.

stringの結合は

"ABC" ^ " to " ^ "XYZ" ;;
val it : string = "ABC to XYZ"

といった具合です．また

2=1;;
val it : bool = false
2=1+1;;
val it : bool = true
2>1;;
val it : bool = true

のような評価もできます．
（３）make definitions
　ある本体に名前を付けて，参照できるようにするには

let 名前 = 本体

とします．例えば，

let x = 1 and y = 2;;
val x : int = 1
val y : int = 2
x+y;;
val it : int = 3
let x = x+y;;
val x : int = 3

となり，inを用いて

let x = 0 in x+y;;
val it : int = 2
x;;
val it : int = 3

のようにローカルな処理もできます．
　引数に値を対応させる関数に名前を名付けるには

let 名前引数 = 値 ;;

あるいは

let 名前 = fun 引数 -> 値 ;;

と入力します．例えば，f1(x)=x*xと定義するには

let f1 x = x * x;;
val f1 : int -> int =

とすればよく，この

f1 : int -> int =

とは，f1のtypeは，intにintを対応させる関数ということです．使い方は，括弧なしで

f1 5;;
val it : int = 25

とすればよく，結合の強さは

f1 5 + 5;;
val it : int = 30

のように，f1(5)+5となります．２変数関数は，例えば

let f2 x y = x * y;;
val f2 : int -> int -> int =

となり，f2のtypeは，intとintにintを対応させる関数ということです．使い方は，同じく

f2 5 7;;
val it : int = 35

ですが，例えば，上で定義した１変数関数f1の合成による5の像f1(f1(5))を括弧なしで書くと

f1 f1 5;;
Characters 0-2:
f1 f1 5;;
^^
This function is applied to too many arguments,
maybe you forgot a `;'

のようにf1 5が左側のf1の引数と見なされてしまいますので，ここは

f1 (f1 5);;
val it : int = 625

あるいは，合成の記号として o（小文字のオー）を用いて

# let f x = x+1 and g x = 2 * x ;;
val f : int -> int =
val g : int -> int =
# f o g 3;;
Characters 4-7:
f o g 3;;
^^^
This expression has type int but is here used with type 'a -> int
# (f o g) 3 = f ( g 3 );;
val it : bool = true

とすることになります．

　なお，OCamlについての詳しくは
http://ocaml.jp/FrontPage
あるいは
http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/class/isle4/mltext/ocaml.html
などが参考になります．