Mercurial > cpdt > repo
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] *) |