今日のCoq: eval

前回作ったラムダ式の上に、evalを定義しました。

覚えたこと

全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。

• 再帰関数の定義は、かなり厳しい制約があるっぽい

よく分からないこと

最初、termを与えると値になるまで評価するevalを書いてみました。

....

Function eval (t :term) {measure term_length t} : term :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        eval (subst body x t2)
      else
      	eval (Apply t1 (eval t2))
  | Apply t1 t2 =>
      eval (Apply (eval t1) t2)
  end.

そしたら、evalがないよ、と言われてしまった。

coqc lambda.v
File "./lambda.v", line 66, characters 0-319:
Error: No such section variable or assumption: eval.

いろいろ書き換えて試したところ

eval (Apply (eval t1) t2)

みたいな、evalを二回呼び出しているところがダメらしい。

回避方法

どっちにしろ、上記のようなevalだと停止しないことがありそうだったので、1ステップだけ簡約するstepという関数を定義しました。

...
Fixpoint step (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        subst body x t2
      else
      	Apply t1 (step t2)
  | Apply t1 t2 =>
      Apply (step t1) t2
  end.

ソースコード

(* simple typed lambda calculus *)
Require Import Arith.EqNat.

(* simple type *)
Inductive type : Set :=
    BoolT : type
  | FunT  : type -> type -> type.

Inductive term : Set :=
    Var     : nat -> term
  | Bool    : bool   -> term
  | Lambda  : nat -> type -> term -> term
  | Apply   : term  -> term -> term.

(* Eval *)
Fixpoint subst (t : term) (old : nat) (new : term) :=
  match t with
  | Bool _ =>
      t
  | Var x =>
      if beq_nat x old then
      	new
      else
      	t
  | Lambda x type body =>
      if beq_nat x old then
      	t
      else
        Lambda x type (subst body old new)
  | Apply t1 t2 =>
      Apply (subst t1 old new) (subst t2 old new)
  end.

Definition is_value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      true
  | Apply _ _  =>
      false
  end.

Fixpoint step (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        subst body x t2
      else
      	Apply t1 (step t2)
  | Apply t1 t2 =>
      Apply (step t1) t2
  end.

(*
Function eval (t :term) {measure term_length t} : term :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      t
  | Apply (Lambda x _ body as t1) t2 =>
      if is_value t2 then
        eval (subst body x t2)
      else
      	eval (Apply t1 (eval t2))
  | Apply t1 t2 =>
      eval (Apply (eval t1) t2)
  end.*)