Coqで多変数多項式の簡約 - にわとり小屋でのプログラミング

変数全体の集合varを{ $x_0,x_1,x_2,...$ }というように自然数の対応で与えられると考え、式expを以下のように定義する。

Inductive exp : Set :=
| Var : var -> exp
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp.

ここで binop型の値は二項演算子(binary operation)の種類(＋または×)を表すものとして以下で定義されるものとし、定数項は簡単のため自然数(nat)に限るとする。

Inductive binop : Set := Plus | Times.

つまり、この定義のもとでは以下のように多項式が表現される。

多項式	Coqでの表現
$x_0+1$	Binop Plus (Var 0) (Const 1)
$x_0^2+x_1^2$	Binop Plus (Binop Times (Var 0) (Var 0)) (Binop Times (Var 1) (Var 1)

各変数から値への対応 (var -> nat) を環境として、ある環境ctxにおける式eの意味を次で再帰的に与える。

Fixpoint expDenote (ctx: var -> nat) (e : exp) : nat :=
  match e with
    | Var v => ctx v
    | Const n => n
    | Binop b e1 e2 => (binopDenote b) (expDenote ctx e1) (expDenote ctx e2)
  end.

そして式e1とe2の意味が同じという事を $\forall$ ctx, expDenote ctx e1 = expDenote ctx e2として考える事ができる。

ここで式eに対して、定数部分に関する部分的に簡単な形にする畳み込み関数を次で定義し、その健全性を示す。

Fixpoint constFold (e : exp) : exp :=
  match e with
    | Var v => Var v
    | Const n => Const n
    | Binop b e1 e2 =>
      match (constFold e1, constFold e2) with
        | (Const m, Const n) => Const ((binopDenote b) m n)
        | (e1', e2') => Binop b e1' e2'
      end
  end.

eを深さ優先に探索し、定数同士の2項演算を評価している。

ここで、この部分的な評価関数において、式eの意味が絶対変わらないことを証明する。

Lemma const_fold_preserved : forall e ctx,
  expDenote ctx e = expDenote ctx (constFold e).
Proof.

induction e.
 reflexivity.
 
 reflexivity.
 
 intro ctx; simpl; rewrite IHe1; rewrite IHe2.
 destruct (constFold e1); destruct (constFold e2); reflexivity.
Qed.

今回のネタはCPDTのExcercise 3.2 から取ってきた。CPDTはCoqでプログラムするときに必要な知識や便利な技を紹介していて非常にためになるので、Coqプログラミングをやりたい人にはぜひともオススメである。また、現在CPDTを勉強しているグループはFormal Method勉強会やProofCafe - coqグループなどあるので、参加してみてはいかがだろうか。

ソースコード全体と問題文は以下: http://ideone.com/kGLVw