comparison src/StackMachine.v @ 475:1fd4109f7b31

Batch of changes based on proofreader feedback
author Adam Chlipala <adam@chlipala.net>
date Mon, 22 Oct 2012 14:23:52 -0400
parents 51a8472aca68
children fa2eb72446a8
comparison
equal deleted inserted replaced
474:d9e1fb184672 475:1fd4109f7b31
40 40
41 A note for readers following along in the PDF version: %\index{coqdoc}%coqdoc supports pretty-printing of tokens in %\LaTeX{}%#LaTeX# or HTML. Where you see a right arrow character, the source contains the ASCII text <<->>>. Other examples of this substitution appearing in this chapter are a double right arrow for <<=>>>, the inverted %`%#'#A' symbol for <<forall>>, and the Cartesian product %`%#'#X' for <<*>>. When in doubt about the ASCII version of a symbol, you can consult the chapter source code. 41 A note for readers following along in the PDF version: %\index{coqdoc}%coqdoc supports pretty-printing of tokens in %\LaTeX{}%#LaTeX# or HTML. Where you see a right arrow character, the source contains the ASCII text <<->>>. Other examples of this substitution appearing in this chapter are a double right arrow for <<=>>>, the inverted %`%#'#A' symbol for <<forall>>, and the Cartesian product %`%#'#X' for <<*>>. When in doubt about the ASCII version of a symbol, you can consult the chapter source code.
42 42
43 %\medskip% 43 %\medskip%
44 44
45 Now we are ready to say what programs in our expression language mean. We will do this by writing an %\index{interpreters}%interpreter that can be thought of as a trivial operational or denotational semantics. (If you are not familiar with these semantic techniques, no need to worry; we will stick to "common sense" constructions.)%\index{Vernacular commands!Definition}% *) 45 Now we are ready to say what programs in our expression language mean. We will do this by writing an %\index{interpreters}%interpreter that can be thought of as a trivial operational or denotational semantics. (If you are not familiar with these semantic techniques, no need to worry: we will stick to "common sense" constructions.)%\index{Vernacular commands!Definition}% *)
46 46
47 Definition binopDenote (b : binop) : nat -> nat -> nat := 47 Definition binopDenote (b : binop) : nat -> nat -> nat :=
48 match b with 48 match b with
49 | Plus => plus 49 | Plus => plus
50 | Times => mult 50 | Times => mult
66 | Plus => plus 66 | Plus => plus
67 | Times => mult 67 | Times => mult
68 end. 68 end.
69 ]] 69 ]]
70 70
71 Languages like Haskell and ML have a convenient%\index{principal types}\index{type inference}% _principal types_ property, which gives us strong guarantees about how effective type inference will be. Unfortunately, Coq's type system is so expressive that any kind of "complete" type inference is impossible, and the task even seems to be hard heuristically in practice. Nonetheless, Coq includes some very helpful heuristics, many of them copying the workings of Haskell and ML type-checkers for programs that fall in simple fragments of Coq's language. 71 Languages like Haskell and ML have a convenient%\index{principal types}\index{type inference}% _principal types_ property, which gives us strong guarantees about how effective type inference will be. Unfortunately, Coq's type system is so expressive that any kind of "complete" type inference is impossible, and the task even seems to be hard in practice. Nonetheless, Coq includes some very helpful heuristics, many of them copying the workings of Haskell and ML type-checkers for programs that fall in simple fragments of Coq's language.
72 72
73 This is as good a time as any to mention the preponderance of different languages associated with Coq. The theoretical foundation of Coq is a formal system called the%\index{Calculus of Inductive Constructions}\index{CIC|see{Calculus of Inductive Constructions}}% _Calculus of Inductive Constructions_ (CIC)%~\cite{CIC}%, which is an extension of the older%\index{Calculus of Constructions}\index{CoC|see{Calculus of Constructions}}% _Calculus of Constructions_ (CoC)%~\cite{CoC}%. CIC is quite a spartan foundation, which is helpful for proving metatheory but not so helpful for real development. Still, it is nice to know that it has been proved that CIC enjoys properties like%\index{strong normalization}% _strong normalization_ %\cite{CIC}%, meaning that every program (and, more importantly, every proof term) terminates; and%\index{relative consistency}% _relative consistency_ %\cite{SetsInTypes}% with systems like versions of %\index{Zermelo-Fraenkel set theory}%Zermelo-Fraenkel set theory, which roughly means that you can believe that Coq proofs mean that the corresponding propositions are "really true," if you believe in set theory. 73 This is as good a time as any to mention the profusion of different languages associated with Coq. The theoretical foundation of Coq is a formal system called the%\index{Calculus of Inductive Constructions}\index{CIC|see{Calculus of Inductive Constructions}}% _Calculus of Inductive Constructions_ (CIC)%~\cite{CIC}%, which is an extension of the older%\index{Calculus of Constructions}\index{CoC|see{Calculus of Constructions}}% _Calculus of Constructions_ (CoC)%~\cite{CoC}%. CIC is quite a spartan foundation, which is helpful for proving metatheory but not so helpful for real development. Still, it is nice to know that it has been proved that CIC enjoys properties like%\index{strong normalization}% _strong normalization_ %\cite{CIC}%, meaning that every program (and, more importantly, every proof term) terminates; and%\index{relative consistency}% _relative consistency_ %\cite{SetsInTypes}% with systems like versions of %\index{Zermelo-Fraenkel set theory}%Zermelo-Fraenkel set theory, which roughly means that you can believe that Coq proofs mean that the corresponding propositions are "really true," if you believe in set theory.
74 74
75 Coq is actually based on an extension of CIC called%\index{Gallina}% _Gallina_. The text after the [:=] and before the period in the last code example is a term of Gallina. Gallina includes several useful features that must be considered as extensions to CIC. The important metatheorems about CIC have not been extended to the full breadth of these features, but most Coq users do not seem to lose much sleep over this omission. 75 Coq is actually based on an extension of CIC called %\index{Gallina}%Gallina. The text after the [:=] and before the period in the last code example is a term of Gallina. Gallina includes several useful features that must be considered as extensions to CIC. The important metatheorems about CIC have not been extended to the full breadth of the features that go beyond the formalized language, but most Coq users do not seem to lose much sleep over this omission.
76 76
77 Next, there is%\index{Ltac}% _Ltac_, Coq's domain-specific language for writing proofs and decision procedures. We will see some basic examples of Ltac later in this chapter, and much of this book is devoted to more involved Ltac examples. 77 Next, there is %\index{Ltac}%Ltac, Coq's domain-specific language for writing proofs and decision procedures. We will see some basic examples of Ltac later in this chapter, and much of this book is devoted to more involved Ltac examples.
78 78
79 Finally, commands like [Inductive] and [Definition] are part of%\index{Vernacular commands}% _the Vernacular_, which includes all sorts of useful queries and requests to the Coq system. Every Coq source file is a series of vernacular commands, where many command forms take arguments that are Gallina or Ltac programs. (Actually, Coq source files are more like _trees_ of vernacular commands, thanks to various nested scoping constructs.) 79 Finally, commands like [Inductive] and [Definition] are part of %\index{Vernacular commands}%the Vernacular, which includes all sorts of useful queries and requests to the Coq system. Every Coq source file is a series of vernacular commands, where many command forms take arguments that are Gallina or Ltac programs. (Actually, Coq source files are more like _trees_ of vernacular commands, thanks to various nested scoping constructs.)
80 80
81 %\medskip% 81 %\medskip%
82 82
83 We can give a simple definition of the meaning of an expression:%\index{Vernacular commands!Fixpoint}% *) 83 We can give a simple definition of the meaning of an expression:%\index{Vernacular commands!Fixpoint}% *)
84 84
522 522
523 reflexivity. 523 reflexivity.
524 Qed. 524 Qed.
525 (* end thide *) 525 (* end thide *)
526 526
527 (** This proof can be shortened and made automated, but we leave that task as an exercise for the reader. *) 527 (** This proof can be shortened and automated, but we leave that task as an exercise for the reader. *)
528 528
529 529
530 (** * Typed Expressions *) 530 (** * Typed Expressions *)
531 531
532 (** In this section, we will build on the initial example by adding additional expression forms that depend on static typing of terms for safety. *) 532 (** In this section, we will build on the initial example by adding additional expression forms that depend on static typing of terms for safety. *)