Mercurial > cpdt > repo

comparison src/ProgLang.v @ 434:92f386c33e94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass taking advantage of new coqdoc features
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 16:38:44 -0400
parents 73f8165a3c1d
children e53d051681b0
comparison
equal deleted inserted replaced
433:5eebaaa9f952 434:92f386c33e94
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *) 18 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *)
19 19
20 (** Reasoning about the syntax and semantics of programming languages is a popular application of proof assistants. Before proving the first theorem of this kind, it is necessary to choose a formal encoding of the informal notions of syntax, dealing with such issues as %\index{variable binding}%variable binding conventions. I believe the pragmatic questions in this domain are far from settled and remain as important open research problems. However, in this chapter, I will demonstrate two underused encoding approaches. Note that I am not recommending either approach as a silver bullet! Mileage will vary across concrete problems, and I expect there to be significant future advances in our knowledge of encoding techniques. For a broader introduction to programming language formalization, using more elementary techniques, see %\emph{%#<a href="http://www.cis.upenn.edu/~bcpierce/sf/"><i>#Software Foundations#</i></a>#%}\footnote{\url{http://www.cis.upenn.edu/~bcpierce/sf/}}% by Pierce et al. 20 (** Reasoning about the syntax and semantics of programming languages is a popular application of proof assistants. Before proving the first theorem of this kind, it is necessary to choose a formal encoding of the informal notions of syntax, dealing with such issues as %\index{variable binding}%variable binding conventions. I believe the pragmatic questions in this domain are far from settled and remain as important open research problems. However, in this chapter, I will demonstrate two underused encoding approaches. Note that I am not recommending either approach as a silver bullet! Mileage will vary across concrete problems, and I expect there to be significant future advances in our knowledge of encoding techniques. For a broader introduction to programming language formalization, using more elementary techniques, see %\emph{%{{http://www.cis.upenn.edu/~bcpierce/sf/}Software Foundations}%}% by Pierce et al.
21 21
22 This chapter is also meant as a case study, bringing together what we have learned in the previous chapters. We will see a concrete example of the importance of representation choices; translating mathematics from paper to Coq is not a deterministic process, and different creative choices can have big impacts. We will also see dependent types and scripted proof automation in action, applied to solve a particular problem as well as possible, rather than to demonstrate new Coq concepts. 22 This chapter is also meant as a case study, bringing together what we have learned in the previous chapters. We will see a concrete example of the importance of representation choices; translating mathematics from paper to Coq is not a deterministic process, and different creative choices can have big impacts. We will also see dependent types and scripted proof automation in action, applied to solve a particular problem as well as possible, rather than to demonstrate new Coq concepts.
23 23
24 I apologize in advance to those readers not familiar with the theory of programming language semantics. I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip. 24 I apologize in advance to those readers not familiar with the theory of programming language semantics. I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip.
25 25
183 end; t). 183 end; t).
184 Qed. 184 Qed.
185 185
186 (** The transformations we have tried so far have been straightforward because they do not have interesting effects on the variable binding structure of terms. The dependent de Bruijn representation is called%\index{first-order syntax}% _first-order_ because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure. 186 (** The transformations we have tried so far have been straightforward because they do not have interesting effects on the variable binding structure of terms. The dependent de Bruijn representation is called%\index{first-order syntax}% _first-order_ because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure.
187 187
188 As an example of a tricky transformation, consider one that removes all uses of %``%#"#[let x = e1 in e2]#"#%''% by substituting [e1] for [x] in [e2]. We will implement the translation by pairing the %``%#"#compile-time#"#%''% typing environment with a %``%#"#run-time#"#%''% value environment or _substitution_, mapping each variable to a value to be substituted for it. Such a substitute term may be placed within a program in a position with a larger typing environment than applied at the point where the substitute term was chosen. To support such context transplantation, we need _lifting_, a standard de Bruijn indices operation. With dependent typing, lifting corresponds to weakening for typing judgments. 188 As an example of a tricky transformation, consider one that removes all uses of "[let x = e1 in e2]" by substituting [e1] for [x] in [e2]. We will implement the translation by pairing the "compile-time" typing environment with a "run-time" value environment or _substitution_, mapping each variable to a value to be substituted for it. Such a substitute term may be placed within a program in a position with a larger typing environment than applied at the point where the substitute term was chosen. To support such context transplantation, we need _lifting_, a standard de Bruijn indices operation. With dependent typing, lifting corresponds to weakening for typing judgments.
189 189
190 The fundamental goal of lifting is to add a new variable to a typing context, maintaining the validity of a term in the expanded context. To express the operation of adding a type to a context, we use a helper function [insertAt]. *) 190 The fundamental goal of lifting is to add a new variable to a typing context, maintaining the validity of a term in the expanded context. To express the operation of adding a type to a context, we use a helper function [insertAt]. *)
191 191
192 Fixpoint insertAt (t : type) (G : list type) (n : nat) {struct n} : list type := 192 Fixpoint insertAt (t : type) (G : list type) (n : nat) {struct n} : list type :=
193 match n with 193 match n with
694 Have we really avoided first-order reasoning about the output terms of translations? The answer depends on some subtle issues, which deserve a subsection of their own. *) 694 Have we really avoided first-order reasoning about the output terms of translations? The answer depends on some subtle issues, which deserve a subsection of their own. *)
695 695
696 696
697 (** ** Establishing Term Well-Formedness *) 697 (** ** Establishing Term Well-Formedness *)
698 698
699 (** Can there be values of type [Term t] that are not well-formed according to [Wf]? We expect that Gallina satisfies key%\index{parametricity}% _parametricity_ %\cite{parametricity}% properties, which indicate how polymorphic types may only be inhabited by specific values. We omit details of parametricity theorems here, but [forall t (E : Term t), Wf E] follows the flavor of such theorems. One option would be to assert that fact as an axiom, %``%#"#proving#"#%''% that any output of any of our translations is well-formed. We could even prove the soundness of the theorem on paper meta-theoretically, say by considering some particular model of CIC. 699 (** Can there be values of type [Term t] that are not well-formed according to [Wf]? We expect that Gallina satisfies key%\index{parametricity}% _parametricity_ %\cite{parametricity}% properties, which indicate how polymorphic types may only be inhabited by specific values. We omit details of parametricity theorems here, but [forall t (E : Term t), Wf E] follows the flavor of such theorems. One option would be to assert that fact as an axiom, "proving" that any output of any of our translations is well-formed. We could even prove the soundness of the theorem on paper meta-theoretically, say by considering some particular model of CIC.
700 700
701 To be more cautious, we could prove [Wf] for every term that interests us, threading such proofs through all transformations. Here is an example exercise of that kind, for [Unlet]. 701 To be more cautious, we could prove [Wf] for every term that interests us, threading such proofs through all transformations. Here is an example exercise of that kind, for [Unlet].
702 702
703 First, we prove that [wf] is _monotone_, in that a given instance continues to hold as we add new variable pairs to the variable isomorphism. *) 703 First, we prove that [wf] is _monotone_, in that a given instance continues to hold as we add new variable pairs to the variable isomorphism. *)
704 704