comparison src/StackMachine.v @ 363:7e57c909f0f2

Explicit note about primitive recursion restriction, early on
author Adam Chlipala <adam@chlipala.net>
date Thu, 03 Nov 2011 17:04:41 -0400
parents cbeccef45f4e
children d1276004eec9
comparison
equal deleted inserted replaced
362:70ffa4d3726e 363:7e57c909f0f2
105 | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2) 105 | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
106 end. 106 end.
107 107
108 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *) 108 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *)
109 109
110 (** It is convenient to be able to test definitions before starting to prove things about them. We can verify that our semantics is sensible by evaluating some sample uses, using the command %\index{Vernacular commands!Eval}%[Eval]. This command takes an argument expressing a %\index{reduction strategy}\emph{%#<i>#reduction strategy#</i>#%}%, or an %``%#"#order of evaluation.#"#%''% Unlike with ML, which hardcodes an %\emph{%#<i>#eager#</i>#%}% reduction strategy, or Haskell, which hardcodes a %\emph{%#<i>#lazy#</i>#%}% strategy, in Coq we are free to choose between these and many other orders of evaluation, because all Coq programs terminate. In fact, Coq silently checked %\index{termination checking}%termination of our [Fixpoint] definition above, using a simple heuristic based on monotonically decreasing size of arguments across recursive calls. 110 (** It is convenient to be able to test definitions before starting to prove things about them. We can verify that our semantics is sensible by evaluating some sample uses, using the command %\index{Vernacular commands!Eval}%[Eval]. This command takes an argument expressing a %\index{reduction strategy}\emph{%#<i>#reduction strategy#</i>#%}%, or an %``%#"#order of evaluation.#"#%''% Unlike with ML, which hardcodes an %\emph{%#<i>#eager#</i>#%}% reduction strategy, or Haskell, which hardcodes a %\emph{%#<i>#lazy#</i>#%}% strategy, in Coq we are free to choose between these and many other orders of evaluation, because all Coq programs terminate. In fact, Coq silently checked %\index{termination checking}%termination of our [Fixpoint] definition above, using a simple heuristic based on monotonically decreasing size of arguments across recursive calls. Specifically, recursive calls must be made on arguments that were pulled out of the original recursive argument with [match] expressions. (In Chapter 7, we will see some ways of getting around this restriction, though simply removing the restriction would leave Coq useless as a theorem proving tool, for reasons we will start to learn about in the next chapter.)
111 111
112 To return to our test evaluations, we run the [Eval] command using the [simpl] evaluation strategy, whose definition is best postponed until we have learned more about Coq's foundations, but which usually gets the job done. *) 112 To return to our test evaluations, we run the [Eval] command using the [simpl] evaluation strategy, whose definition is best postponed until we have learned more about Coq's foundations, but which usually gets the job done. *)
113 113
114 Eval simpl in expDenote (Const 42). 114 Eval simpl in expDenote (Const 42).
115 (** [= 42 : nat] *) 115 (** [= 42 : nat] *)