言語ゲーム

とあるエンジニアが嘘ばかり書く日記

Twitter: @propella
トップ > CafeOBJ

CafeOBJ

こないだ C5 の後でちょっと話題になったので、CafeOBJ について調べてみました。

http://www.ldl.jaist.ac.jp/cafeobj/system.html からダウンロードして展開、Mac の場合 lisp/CafeOBJ にバイナリがあるので、それを /usr/local/bin/cafeobj にシンボリックリンクを貼って使う事にしました。

CafeOBJ 入門 http://www.jaist.ac.jp/~t-seino/lectures/cafeobj-intro-j/ を読みながら進めます。

とりあえず最初の例にコメントをつけてみます。コメントは '-- '、'** '、'--> ' または '**> ' の四種類あって、> の付くやつはエコーバックされます。

mod! SIMPLE-NAT {   -- モジュール: 仕様の開始。モジュール宣言。! はキツさをあらわすらしい(?)
  [ Nat ]           -- ソート: 型の宣言 [ 子型 < 親型 ] のように包含関係を書けるらしい。
  -- オペレータ: 文法は "op 名前 : 引数型 -> 戻値型" 
  op 0 : -> Nat     -- 0 という演算子は Nat 型を返すという意味。訳: 0 は自然数を返す関数
  op s : Nat -> Nat -- s という演算子は Nat 型を受取り Nat 型を返す。訳: 1+自然数は自然数
}

mod! NAT+ {                          -- モジュール: このように識別子には + のような記号も使える。
  pr(SIMPLE-NAT)                     -- 輸入: 別のモジュールを読み込む。pr、ex、us の三種類ある。
  -- オペレータ: _ は引数の位置をあらわす。
  op _+_ : Nat Nat -> Nat            -- + は Nat 二つを受け取って Nat 一つを返す。
  -- 等式: 公理をつくる。文法は "eq 左辺 = 右辺 ."。M:Nat は M が Nat に含まれるという意味。
  eq 0 + M:Nat = M .                 -- 自然数 M に 0 を足すと自然数 M
  eq s (N:Nat) + M:Nat = s (N + M) . -- 自然数 N + 1 に 自然数 M を足すと 1 + N + M
}

[] で型を宣言して op で関数の型を宣言する所までは雰囲気で言うと C のヘッダファイルみたい。eq というのは普通の言語には無いですな。さてこれを実行するには、まず simple-nat.mod というファイルに保存。そして cafeobj を立ち上げて in コマンドでファイルを読みます。

$ cafeobj
CafeOBJ> in simple-nat
processing input : ./simple-nat.mod
..._* done.
-- defining module! NAT+.._..* done.

よくわからんが多分うまく行ったみたいです。次にこの定義を元に実験してみます。select で使うモジュールを選び、parse の後に解析する文を書きます。最後のドット . の前に空白が必要です。

CafeOBJ> select NAT+
NAT+> parse 0 .
(0):Nat

これで 0 が Nat だと言う事が分かります。「0 が自然数に含まれる」事を表現するのに、「0 が自然数型を返す関数である」と記述する所が大変面白いです。「型とは集合の事である」の逆だから同じ事です。他にも色々試してみます。

NAT+> parse s(0) .
(s(0)):Nat
NAT+> parse 0(s) .
[Error] no successfull parse
  (parsed:[ 0 ], rest:[ (( s )) ])
(parsed:[ 0 ], rest:[ (( s )) ]):SyntaxErr
NAT+> parse s(s(s(0))) + s(s(s(s(0)))) .
(s(s(s(0))) + s(s(s(s(0))))):Nat

parse というのは文を読んで型と op 定義だけを使い型チェックを行う機能だと考えても良いと思います。ここではまだ eq で作った等式は使われていません。あと set verbose on を使うと解析木が表示されて面白いです。

NAT+> set verbose on
NAT+> parse s(0) + s(s(0)) .

(s(0) + s(s(0))):Nat
  _+_:Nat   
  /      \   
s:Nat  s:Nat
  |      |   
0:Nat  s:Nat
         |   
       0:Nat

parse の代わりに reduce を使うと等式 eq を使って文を簡約します。

NAT+> reduce s(0) + s(s(0)) .
-- reduce in NAT+ : (s(0) + s(s(0))):Nat
(s(s(s(0)))):Nat
(0.000 sec for parse, 2 rewrites(0.000 sec), 3 matches)

set trace on でトレース表示

NAT+> set trace on
NAT+> reduce s(0) + s(s(0)) .
-- reduce in NAT+ : (s(0) + s(s(0))):Nat
1>[1] rule: eq (s(N:Nat) + M:Nat) = s((N + M))
    { N:Nat |-> 0, M:Nat |-> s(s(0)) }
1<[1] (s(0) + s(s(0))) --> s((0 + s(s(0))))
1>[2] rule: eq (0 + M:Nat) = M
    { M:Nat |-> s(s(0)) }
1<[2] (0 + s(s(0))) --> s(s(0))
(s(s(s(0)))):Nat

set trace whole on で簡潔にトレース。

NAT+> set trace whole on
NAT+> reduce s(0) + s(s(0)) .
-- reduce in NAT+ : (s(0) + s(s(0))):Nat
[1]: (s(0) + s(s(0)))
---> s((0 + s(s(0))))
[2]: s((0 + s(s(0))))
---> s(s(s(0)))
(s(s(s(0)))):Nat

内蔵モジュール EQL を使うと、= が使えるようになります。= は両辺が同じ形に簡約された時だけ true を返します。それ以外は何もしません。

NAT+> select NAT+ + EQL
NAT+ + EQL> reduce 0 + 0 = 0 .
-- reduce in NAT+ + EQL : ((0 + 0) = 0):Bool
(true):Bool
NAT+ + EQL> reduce 0 + s(0) = 0 .
-- reduce in NAT+ + EQL : ((0 + s(0)) = 0):Bool
(s(0) = 0):Bool
NAT+ + EQL> reduce s(s(s(0))) + s(s(s(s(0)))) = s(s(s(s(s(s(s(0))))))) .
-- reduce in NAT+ + EQL : ((s(s(s(0))) + s(s(s(s(0))))) = s(s(s(s(s(s(s(0)))))))):Bool
(true):Bool

もう一つ select の代わりに使われる open があります。open を使うとさらに一時的に定義を追加出来るので、これを証明の「仮定」と考える事ができます。例えば結合律 (i + j) + k = i + (j + k) を証明してみましょう。

$ cafeobj # 最初からやりなおし
CafeOBJ> in simple-nat    -- ファイル読み込み
CafeOBJ> open NAT+ + EQL  -- モジュール読み込み
%NAT+ + EQL> ops i j k : -> Nat .  -- 任意の自然数 i j k
%NAT+ + EQL> reduce (i + j) + k = i + (j + k) . -- 簡約してみる。
-- reduce in %NAT+ + EQL : (((i + j) + k) = (i + (j + k))):Bool
(((i + j) + k) = (i + (j + k))):Bool

ありゃ、うまくいきません。CafeOBJ は 結合律を自分で推論する事はできないので、人間が数学的帰納法を使って証明する必要があります。

%NAT+ + EQL> reduce (0 + j) + k = 0 + (j + k) . -- 基底: i = 0 の時
-- reduce in %NAT+ + EQL : (((0 + j) + k) = (0 + (j + k))):Bool
(true):Bool

%NAT+ + EQL> eq (i + j) + k = i + (j + k) . -- もし仮に命題が正しいとしたら
%NAT+ + EQL> reduce (s(i) + j) + k = s(i) + (j + k) . -- i を s(i) に変えても正しい。
-- reduce in %NAT+ + EQL : (((s(i) + j) + k) = (s(i) + (j + k))):Bool
(true):Bool

これで、0 とそれ以外のケースを証明したので、i がどんな自然数でも (i + j) + k = i + (j + k) が成り立つ事を証明したと言えるでしょう。個人的には、最後の数学的帰納法の所こそ直感的に分かりにくい所なので、ここを機械にやらせろよ！と思うのですが、さすがにそれは無理なのでしょう。

シェルに打ち込んだ式をそのままモジュールと一緒にファイルに書いて、in で読み出す事もできます。その場合、--> で所々コメントを書くと読み込み中にエコーバックされるので、ちゃんと reduce の結果が true かどうか確認する事ができます。