CoqのType classでExpression problemに挑戦する
Coq8.2からType classが導入された。
もともとType classはHaskellにあったものである。
よって、Expression problemもHaskellからやり始めるのが楽である。
だが、私は残念ながらHaskellの世界の住人ではないので、Haskellによる解決に関しては私がこれをやるにいたった原因であるmaoeさんの記事を参照してほしい。
HaskellのType classなんてわからん！という人のために、Expression problemに関してだけ説明*1。
要は、式を計算するようなプログラムを書いて、今まで書いた部分に手を加えることなく新しい演算子を入れたり新しい処理を定義してみたい、と*2。
たとえば、足し算と引き算しかない小学校一年生の世界を、小学校二年生の世界へ広げるために掛け算を加えよう、ということだ。
・・・我ながら意味がわからない例だ。
さて、さっそくCoqで書いていくのだが。
まず通常のデータ型定義のやり方でやってみる*3。
Inductive Exp := EConst (n : nat) | EAdd (e1 e2 : Exp). Fixpoint Eval e := match e with | EConst n => n | EAdd e1 e2 => Eval e1 + Eval e2 end.
これで計算する関数の定義が完了である。
しかし、これだけでは面白くない。とはいえ、文字列に変換など、Coqらしくもない*4。
よって、少し回り道をして、簡単なスタックマシンの定義と、式のコードへのコンパイルを行ってみる。
用いるコードは以下の通り。
Require Import List. Inductive Word := WPush (n : nat) | WPlus. Fixpoint Execute p s := match p with | nil => match s with | n :: nil => Some n | _ => None end | WPush n :: p' => Execute p' (n :: s) | WPlus :: p' => match s with | n1 :: n2 :: s' => Execute p' ((n2 + n1) :: s') | _ => None end end.
これがスタックマシン。
そしてコンパイル用の関数を定義して、それが正しいことを証明する。
Fixpoint Compile e := match e with | EConst n => WPush n :: nil | EAdd e1 e2 => Compile e1 ++ Compile e2 ++ WPlus :: nil end. Goal forall e, Execute (Compile e) nil = Some (Eval e).
あとはこれを証明する・・・のだが、証明については省略しておこう。
ただし、一つだけ言っておくと、実はこの補題を証明しないとうまくいかない（または非常に難しい）。
Goal forall e p s, Execute (Compile e ++ p) s = Execute p (Eval e :: s).
これで一通り終わった。
さて、これに新たな動作を定義するのはどうするか？
普通に関数を定義すればよい。証明も同様。
こちらは非常に簡単なのである。
では、これに掛け算を導入しようと考えたら、一体どこを変更すればいいだろうか？
実は、スタックマシンの命令が足りないことも考慮すると、最後の定理以外全て、である。
つまりExpression problemに対応できていないわけだ。
これを解決するのに使えるのがType classである。
さて、記事が長くなってきたので、本題のType classは次の記事に書こう。
