第 7 回
演習

• プリント

• Benjamin C. Pierce
  "Types and Programming Languages"


• term
  Coq での true や false と区別するため，tm_... としている。
  • tm_true … true
  • tm_false … false
  • tm_if t t t … if t then t else t
  • tm_zero … zero
  • tm_succ t … succ t (t + 1)
  • tm_pred t … pred t (t > 0 なら t - 1，t = 0 なら 0)
  • tm_iszero t … iszero t (t = 0 なら tm_true，t <> 0 なら tm_false)
• 簡約規則
  one step evaluation なので，たとえば
      Lemma le : eval (tm_iszero (tm_pred (tm_succ tm_zero))) tm_true.
  といった命題は証明出来ない。
• 型
  term と同じく，Coq での bool や nat と区別するため， Bool，Nat としている。