## Mercurial > cpdt > repo

### annotate src/ProgLang.v @ 561:c800306b0e32

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Two more users

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Fri, 10 Nov 2017 19:02:44 -0500 |

parents | dac7a2705b00 |

children |

rev | line source |
---|---|

adam@534 | 1 (* Copyright (c) 2011-2012, 2015, Adam Chlipala |

adam@381 | 2 * |

adam@381 | 3 * This work is licensed under a |

adam@381 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |

adam@381 | 5 * Unported License. |

adam@381 | 6 * The license text is available at: |

adam@381 | 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ |

adam@381 | 8 *) |

adam@381 | 9 |

adam@381 | 10 (* begin hide *) |

adam@381 | 11 Require Import FunctionalExtensionality List. |

adam@381 | 12 |

adam@534 | 13 Require Import Cpdt.CpdtTactics Cpdt.DepList. |

adam@381 | 14 |

adam@381 | 15 Set Implicit Arguments. |

adam@534 | 16 Set Asymmetric Patterns. |

adam@381 | 17 (* end hide *) |

adam@381 | 18 |

adam@381 | 19 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *) |

adam@381 | 20 |

adam@434 | 21 (** 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. |

adam@381 | 22 |

adam@381 | 23 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. |

adam@381 | 24 |

adam@381 | 25 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. |

adam@381 | 26 |

adam@534 | 27 We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book. It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs. We also use [f_equal] to simplify goals of a particular form that will come up with the term denotation function that we define shortly. *) |

adam@381 | 28 |

adam@381 | 29 Ltac ext := let x := fresh "x" in extensionality x. |

adam@534 | 30 Ltac pl := crush; repeat (match goal with |

adam@534 | 31 | [ |- (fun x => _) = (fun y => _) ] => ext |

adam@534 | 32 | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal |

adam@535 | 33 | [ |- ?E ::: _ = ?E ::: _ ] => f_equal |

adam@535 | 34 | [ |- hmap _ ?E = hmap _ ?E ] => f_equal |

adam@534 | 35 end; crush). |

adam@381 | 36 |

adam@381 | 37 (** At this point in the book source, some auxiliary proofs also appear. *) |

adam@381 | 38 |

adam@381 | 39 (* begin hide *) |

adam@381 | 40 Section hmap. |

adam@381 | 41 Variable A : Type. |

adam@381 | 42 Variables B1 B2 B3 : A -> Type. |

adam@381 | 43 |

adam@381 | 44 Variable f1 : forall x, B1 x -> B2 x. |

adam@381 | 45 Variable f2 : forall x, B2 x -> B3 x. |

adam@381 | 46 |

adam@381 | 47 Theorem hmap_hmap : forall ls (hl : hlist B1 ls), hmap f2 (hmap f1 hl) = hmap (fun i (x : B1 i) => f2 (f1 x)) hl. |

adam@381 | 48 induction hl; crush. |

adam@381 | 49 Qed. |

adam@381 | 50 End hmap. |

adam@381 | 51 |

adam@381 | 52 Section Forall. |

adam@381 | 53 Variable A : Type. |

adam@381 | 54 Variable P : A -> Prop. |

adam@381 | 55 |

adam@381 | 56 Theorem Forall_In : forall ls, Forall P ls -> forall x, In x ls -> P x. |

adam@381 | 57 induction 1; crush. |

adam@381 | 58 Qed. |

adam@381 | 59 |

adam@381 | 60 Theorem Forall_In' : forall ls, (forall x, In x ls -> P x) -> Forall P ls. |

adam@381 | 61 induction ls; crush. |

adam@381 | 62 Qed. |

adam@381 | 63 |

adam@381 | 64 Variable P' : A -> Prop. |

adam@381 | 65 |

adam@381 | 66 Theorem Forall_weaken : forall ls, Forall P ls |

adam@381 | 67 -> (forall x, P x -> P' x) |

adam@381 | 68 -> Forall P' ls. |

adam@381 | 69 induction 1; crush. |

adam@381 | 70 Qed. |

adam@381 | 71 End Forall. |

adam@381 | 72 (* end hide *) |

adam@381 | 73 |

adam@381 | 74 (** Here is a definition of the type system we will use throughout the chapter. It is for simply typed lambda calculus with natural numbers as the base type. *) |

adam@381 | 75 |

adam@381 | 76 Inductive type : Type := |

adam@381 | 77 | Nat : type |

adam@381 | 78 | Func : type -> type -> type. |

adam@381 | 79 |

adam@381 | 80 Fixpoint typeDenote (t : type) : Type := |

adam@381 | 81 match t with |

adam@381 | 82 | Nat => nat |

adam@381 | 83 | Func t1 t2 => typeDenote t1 -> typeDenote t2 |

adam@381 | 84 end. |

adam@381 | 85 |

adam@381 | 86 (** Now we have some choices as to how we represent the syntax of programs. The two sections of the chapter explore two such choices, demonstrating the effect the choice has on proof complexity. *) |

adam@381 | 87 |

adam@381 | 88 |

adam@381 | 89 (** * Dependent de Bruijn Indices *) |

adam@381 | 90 |

adam@465 | 91 (** The first encoding is one we met first in Chapter 9, the _dependent de Bruijn index_ encoding. We represent program syntax terms in a type family parameterized by a list of types, representing the _typing context_, or information on which free variables are in scope and what their types are. Variables are represented in a way isomorphic to the natural numbers, where number 0 represents the first element in the context, number 1 the second element, and so on. Actually, instead of numbers, we use the [member] dependent type family from Chapter 9. *) |

adam@381 | 92 |

adam@381 | 93 Module FirstOrder. |

adam@381 | 94 |

adam@381 | 95 (** Here is the definition of the [term] type, including variables, constants, addition, function abstraction and application, and let binding of local variables. *) |

adam@381 | 96 |

adam@381 | 97 Inductive term : list type -> type -> Type := |

adam@381 | 98 | Var : forall G t, member t G -> term G t |

adam@381 | 99 |

adam@381 | 100 | Const : forall G, nat -> term G Nat |

adam@381 | 101 | Plus : forall G, term G Nat -> term G Nat -> term G Nat |

adam@381 | 102 |

adam@381 | 103 | Abs : forall G dom ran, term (dom :: G) ran -> term G (Func dom ran) |

adam@381 | 104 | App : forall G dom ran, term G (Func dom ran) -> term G dom -> term G ran |

adam@381 | 105 |

adam@381 | 106 | Let : forall G t1 t2, term G t1 -> term (t1 :: G) t2 -> term G t2. |

adam@381 | 107 |

adam@381 | 108 Implicit Arguments Const [G]. |

adam@381 | 109 |

adam@381 | 110 (** Here are two example term encodings, the first of addition packaged as a two-argument curried function, and the second of a sample application of addition to constants. *) |

adam@381 | 111 |

adam@381 | 112 Example add : term nil (Func Nat (Func Nat Nat)) := |

adam@381 | 113 Abs (Abs (Plus (Var (HNext HFirst)) (Var HFirst))). |

adam@381 | 114 |

adam@381 | 115 Example three_the_hard_way : term nil Nat := |

adam@381 | 116 App (App add (Const 1)) (Const 2). |

adam@381 | 117 |

adam@381 | 118 (** Since dependent typing ensures that any term is well-formed in its context and has a particular type, it is easy to translate syntactic terms into Coq values. *) |

adam@381 | 119 |

adam@381 | 120 Fixpoint termDenote G t (e : term G t) : hlist typeDenote G -> typeDenote t := |

adam@381 | 121 match e with |

adam@381 | 122 | Var _ _ x => fun s => hget s x |

adam@381 | 123 |

adam@381 | 124 | Const _ n => fun _ => n |

adam@381 | 125 | Plus _ e1 e2 => fun s => termDenote e1 s + termDenote e2 s |

adam@381 | 126 |

adam@381 | 127 | Abs _ _ _ e1 => fun s => fun x => termDenote e1 (x ::: s) |

adam@381 | 128 | App _ _ _ e1 e2 => fun s => (termDenote e1 s) (termDenote e2 s) |

adam@381 | 129 |

adam@381 | 130 | Let _ _ _ e1 e2 => fun s => termDenote e2 (termDenote e1 s ::: s) |

adam@381 | 131 end. |

adam@381 | 132 |

adam@398 | 133 (** With this term representation, some program transformations are easy to implement and prove correct. Certainly we would be worried if this were not the the case for the _identity_ transformation, which takes a term apart and reassembles it. *) |

adam@381 | 134 |

adam@381 | 135 Fixpoint ident G t (e : term G t) : term G t := |

adam@381 | 136 match e with |

adam@381 | 137 | Var _ _ x => Var x |

adam@381 | 138 |

adam@381 | 139 | Const _ n => Const n |

adam@381 | 140 | Plus _ e1 e2 => Plus (ident e1) (ident e2) |

adam@381 | 141 |

adam@381 | 142 | Abs _ _ _ e1 => Abs (ident e1) |

adam@381 | 143 | App _ _ _ e1 e2 => App (ident e1) (ident e2) |

adam@381 | 144 |

adam@381 | 145 | Let _ _ _ e1 e2 => Let (ident e1) (ident e2) |

adam@381 | 146 end. |

adam@381 | 147 |

adam@381 | 148 Theorem identSound : forall G t (e : term G t) s, |

adam@381 | 149 termDenote (ident e) s = termDenote e s. |

adam@497 | 150 induction e; pl. |

adam@381 | 151 Qed. |

adam@381 | 152 |

adam@398 | 153 (** A slightly more ambitious transformation belongs to the family of _constant folding_ optimizations we have used as examples in other chapters. *) |

adam@398 | 154 |

adam@381 | 155 Fixpoint cfold G t (e : term G t) : term G t := |

adam@381 | 156 match e with |

adam@381 | 157 | Plus G e1 e2 => |

adam@381 | 158 let e1' := cfold e1 in |

adam@381 | 159 let e2' := cfold e2 in |

adam@398 | 160 let maybeOpt := match e1' return _ with |

adam@398 | 161 | Const _ n1 => |

adam@398 | 162 match e2' return _ with |

adam@398 | 163 | Const _ n2 => Some (Const (n1 + n2)) |

adam@398 | 164 | _ => None |

adam@398 | 165 end |

adam@398 | 166 | _ => None |

adam@398 | 167 end in |

adam@398 | 168 match maybeOpt with |

adam@398 | 169 | None => Plus e1' e2' |

adam@398 | 170 | Some e' => e' |

adam@398 | 171 end |

adam@381 | 172 |

adam@381 | 173 | Abs _ _ _ e1 => Abs (cfold e1) |

adam@381 | 174 | App _ _ _ e1 e2 => App (cfold e1) (cfold e2) |

adam@381 | 175 |

adam@381 | 176 | Let _ _ _ e1 e2 => Let (cfold e1) (cfold e2) |

adam@381 | 177 |

adam@381 | 178 | e => e |

adam@381 | 179 end. |

adam@381 | 180 |

adam@381 | 181 (** The correctness proof is more complex, but only slightly so. *) |

adam@381 | 182 |

adam@381 | 183 Theorem cfoldSound : forall G t (e : term G t) s, |

adam@381 | 184 termDenote (cfold e) s = termDenote e s. |

adam@497 | 185 induction e; pl; |

adam@381 | 186 repeat (match goal with |

adam@414 | 187 | [ |- context[match ?E with Var _ _ _ => _ | _ => _ end] ] => |

adam@414 | 188 dep_destruct E |

adam@497 | 189 end; pl). |

adam@381 | 190 Qed. |

adam@381 | 191 |

adam@414 | 192 (** 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. |

adam@381 | 193 |

adam@434 | 194 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. |

adam@381 | 195 |

adam@381 | 196 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]. *) |

adam@381 | 197 |

adam@381 | 198 Fixpoint insertAt (t : type) (G : list type) (n : nat) {struct n} : list type := |

adam@381 | 199 match n with |

adam@381 | 200 | O => t :: G |

adam@381 | 201 | S n' => match G with |

adam@381 | 202 | nil => t :: G |

adam@381 | 203 | t' :: G' => t' :: insertAt t G' n' |

adam@381 | 204 end |

adam@381 | 205 end. |

adam@381 | 206 |

adam@381 | 207 (** Another function lifts bound variable instances, which we represent with [member] values. *) |

adam@381 | 208 |

adam@381 | 209 Fixpoint liftVar t G (x : member t G) t' n : member t (insertAt t' G n) := |

adam@381 | 210 match x with |

adam@381 | 211 | HFirst G' => match n return member t (insertAt t' (t :: G') n) with |

adam@381 | 212 | O => HNext HFirst |

adam@381 | 213 | _ => HFirst |

adam@381 | 214 end |

adam@381 | 215 | HNext t'' G' x' => match n return member t (insertAt t' (t'' :: G') n) with |

adam@381 | 216 | O => HNext (HNext x') |

adam@381 | 217 | S n' => HNext (liftVar x' t' n') |

adam@381 | 218 end |

adam@381 | 219 end. |

adam@381 | 220 |

adam@381 | 221 (** The final helper function for lifting allows us to insert a new variable anywhere in a typing context. *) |

adam@381 | 222 |

adam@381 | 223 Fixpoint lift' G t' n t (e : term G t) : term (insertAt t' G n) t := |

adam@381 | 224 match e with |

adam@381 | 225 | Var _ _ x => Var (liftVar x t' n) |

adam@381 | 226 |

adam@381 | 227 | Const _ n => Const n |

adam@381 | 228 | Plus _ e1 e2 => Plus (lift' t' n e1) (lift' t' n e2) |

adam@381 | 229 |

adam@381 | 230 | Abs _ _ _ e1 => Abs (lift' t' (S n) e1) |

adam@381 | 231 | App _ _ _ e1 e2 => App (lift' t' n e1) (lift' t' n e2) |

adam@381 | 232 |

adam@381 | 233 | Let _ _ _ e1 e2 => Let (lift' t' n e1) (lift' t' (S n) e2) |

adam@381 | 234 end. |

adam@381 | 235 |

adam@398 | 236 (** In the [Let] removal transformation, we only need to apply lifting to add a new variable at the _beginning_ of a typing context, so we package lifting into this final, simplified form. *) |

adam@381 | 237 |

adam@381 | 238 Definition lift G t' t (e : term G t) : term (t' :: G) t := |

adam@381 | 239 lift' t' O e. |

adam@381 | 240 |

adam@381 | 241 (** Finally, we can implement [Let] removal. The argument of type [hlist (term G') G] represents a substitution mapping each variable from context [G] into a term that is valid in context [G']. Note how the [Abs] case (1) extends via lifting the substitution [s] to hold in the broader context of the abstraction body [e1] and (2) maps the new first variable to itself. It is only the [Let] case that maps a variable to any substitute beside itself. *) |

adam@381 | 242 |

adam@381 | 243 Fixpoint unlet G t (e : term G t) G' : hlist (term G') G -> term G' t := |

adam@381 | 244 match e with |

adam@381 | 245 | Var _ _ x => fun s => hget s x |

adam@381 | 246 |

adam@381 | 247 | Const _ n => fun _ => Const n |

adam@381 | 248 | Plus _ e1 e2 => fun s => Plus (unlet e1 s) (unlet e2 s) |

adam@381 | 249 |

adam@381 | 250 | Abs _ _ _ e1 => fun s => Abs (unlet e1 (Var HFirst ::: hmap (lift _) s)) |

adam@381 | 251 | App _ _ _ e1 e2 => fun s => App (unlet e1 s) (unlet e2 s) |

adam@381 | 252 |

adam@381 | 253 | Let _ t1 _ e1 e2 => fun s => unlet e2 (unlet e1 s ::: s) |

adam@381 | 254 end. |

adam@381 | 255 |

adam@381 | 256 (** We have finished defining the transformation, but the parade of helper functions is not over. To prove correctness, we will use one more helper function and a few lemmas. First, we need an operation to insert a new value into a substitution at a particular position. *) |

adam@381 | 257 |

adam@381 | 258 Fixpoint insertAtS (t : type) (x : typeDenote t) (G : list type) (n : nat) {struct n} |

adam@381 | 259 : hlist typeDenote G -> hlist typeDenote (insertAt t G n) := |

adam@381 | 260 match n with |

adam@381 | 261 | O => fun s => x ::: s |

adam@381 | 262 | S n' => match G return hlist typeDenote G |

adam@381 | 263 -> hlist typeDenote (insertAt t G (S n')) with |

adam@381 | 264 | nil => fun s => x ::: s |

adam@381 | 265 | t' :: G' => fun s => hhd s ::: insertAtS t x n' (htl s) |

adam@381 | 266 end |

adam@381 | 267 end. |

adam@381 | 268 |

adam@381 | 269 Implicit Arguments insertAtS [t G]. |

adam@381 | 270 |

adam@381 | 271 (** Next we prove that [liftVar] is correct. That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *) |

adam@381 | 272 |

adam@381 | 273 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n, |

adam@381 | 274 hget s m = hget (insertAtS x n s) (liftVar m t' n). |

adam@497 | 275 induction m; destruct n; dep_destruct s; pl. |

adam@381 | 276 Qed. |

adam@381 | 277 |

adam@381 | 278 Hint Resolve liftVarSound. |

adam@381 | 279 |

adam@381 | 280 (** An analogous lemma establishes correctness of [lift']. *) |

adam@381 | 281 |

adam@381 | 282 Lemma lift'Sound : forall G t' (x : typeDenote t') t (e : term G t) n s, |

adam@381 | 283 termDenote e s = termDenote (lift' t' n e) (insertAtS x n s). |

adam@497 | 284 induction e; pl; |

adam@381 | 285 repeat match goal with |

adam@381 | 286 | [ IH : forall n s, _ = termDenote (lift' _ n ?E) _ |

adam@381 | 287 |- context[lift' _ (S ?N) ?E] ] => specialize (IH (S N)) |

adam@497 | 288 end; pl. |

adam@381 | 289 Qed. |

adam@381 | 290 |

adam@381 | 291 (** Correctness of [lift] itself is an easy corollary. *) |

adam@381 | 292 |

adam@381 | 293 Lemma liftSound : forall G t' (x : typeDenote t') t (e : term G t) s, |

adam@381 | 294 termDenote (lift t' e) (x ::: s) = termDenote e s. |

adam@381 | 295 unfold lift; intros; rewrite (lift'Sound _ x e O); trivial. |

adam@381 | 296 Qed. |

adam@381 | 297 |

adam@381 | 298 Hint Rewrite hget_hmap hmap_hmap liftSound. |

adam@381 | 299 |

adam@381 | 300 (** Finally, we can prove correctness of [unletSound] for terms in arbitrary typing environments. *) |

adam@381 | 301 |

adam@381 | 302 Lemma unletSound' : forall G t (e : term G t) G' (s : hlist (term G') G) s1, |

adam@381 | 303 termDenote (unlet e s) s1 |

adam@381 | 304 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s). |

adam@497 | 305 induction e; pl. |

adam@381 | 306 Qed. |

adam@381 | 307 |

adam@510 | 308 (** The lemma statement is a mouthful, with all its details of typing contexts and substitutions. It is usually prudent to state a final theorem in as simple a way as possible, to help your readers believe that you have proved what they expect. We follow that advice here for the simple case of terms with empty typing contexts. *) |

adam@381 | 309 |

adam@381 | 310 Theorem unletSound : forall t (e : term nil t), |

adam@381 | 311 termDenote (unlet e HNil) HNil = termDenote e HNil. |

adam@381 | 312 intros; apply unletSound'. |

adam@381 | 313 Qed. |

adam@381 | 314 |

adam@381 | 315 End FirstOrder. |

adam@381 | 316 |

adam@381 | 317 (** The [Let] removal optimization is a good case study of a simple transformation that may turn out to be much more work than expected, based on representation choices. In the second part of this chapter, we consider an alternate choice that produces a more pleasant experience. *) |

adam@381 | 318 |

adam@381 | 319 |

adam@381 | 320 (** * Parametric Higher-Order Abstract Syntax *) |

adam@381 | 321 |

adam@510 | 322 (** In contrast to first-order encodings,%\index{higher-order syntax}% _higher-order_ encodings avoid explicit modeling of variable identity. Instead, the binding constructs of an%\index{object language}% _object language_ (the language being formalized) can be represented using the binding constructs of the%\index{meta language}% _meta language_ (the language in which the formalization is done). The best known higher-order encoding is called%\index{higher-order abstract syntax}% _higher-order abstract syntax_ (HOAS) %\cite{HOAS}%, and we can start by attempting to apply it directly in Coq. *) |

adam@381 | 323 |

adam@381 | 324 Module HigherOrder. |

adam@381 | 325 |

adam@398 | 326 (** With HOAS, each object language binding construct is represented with a _function_ of the meta language. Here is what we get if we apply that idea within an inductive definition of term syntax. *) |

adam@381 | 327 |

adam@381 | 328 (** %\vspace{-.15in}%[[ |

adam@381 | 329 Inductive term : type -> Type := |

adam@381 | 330 | Const : nat -> term Nat |

adam@381 | 331 | Plus : term Nat -> term Nat -> term Nat |

adam@381 | 332 |

adam@381 | 333 | Abs : forall dom ran, (term dom -> term ran) -> term (Func dom ran) |

adam@381 | 334 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran |

adam@381 | 335 |

adam@381 | 336 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2. |

adam@381 | 337 ]] |

adam@381 | 338 |

adam@464 | 339 However, Coq rejects this definition for failing to meet the %\index{strict positivity requirement}%strict positivity restriction. For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining. Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic. |

adam@381 | 340 |

adam@510 | 341 An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS|see{parametric higher-order abstract syntax}}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq. Here the idea is to parameterize the syntax type by a type family standing for a _representation of variables_. *) |

adam@381 | 342 |

adam@381 | 343 Section var. |

adam@381 | 344 Variable var : type -> Type. |

adam@381 | 345 |

adam@381 | 346 Inductive term : type -> Type := |

adam@381 | 347 | Var : forall t, var t -> term t |

adam@381 | 348 |

adam@381 | 349 | Const : nat -> term Nat |

adam@381 | 350 | Plus : term Nat -> term Nat -> term Nat |

adam@381 | 351 |

adam@381 | 352 | Abs : forall dom ran, (var dom -> term ran) -> term (Func dom ran) |

adam@381 | 353 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran |

adam@381 | 354 |

adam@381 | 355 | Let : forall t1 t2, term t1 -> (var t1 -> term t2) -> term t2. |

adam@381 | 356 End var. |

adam@381 | 357 |

adam@381 | 358 Implicit Arguments Var [var t]. |

adam@381 | 359 Implicit Arguments Const [var]. |

adam@381 | 360 Implicit Arguments Abs [var dom ran]. |

adam@381 | 361 |

adam@398 | 362 (** Coq accepts this definition because our embedded functions now merely take _variables_ as arguments, instead of arbitrary terms. One might wonder whether there is an easy loophole to exploit here, instantiating the parameter [var] as [term] itself. However, to do that, we would need to choose a variable representation for this nested mention of [term], and so on through an infinite descent into [term] arguments. |

adam@381 | 363 |

adam@381 | 364 We write the final type of a closed term using polymorphic quantification over all possible choices of [var] type family. *) |

adam@381 | 365 |

adam@381 | 366 Definition Term t := forall var, term var t. |

adam@381 | 367 |

adam@398 | 368 (** Here are the new representations of the example terms from the last section. Note how each is written as a function over a [var] choice, such that the specific choice has no impact on the _structure_ of the term. *) |

adam@381 | 369 |

adam@381 | 370 Example add : Term (Func Nat (Func Nat Nat)) := fun var => |

adam@381 | 371 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))). |

adam@381 | 372 |

adam@381 | 373 Example three_the_hard_way : Term Nat := fun var => |

adam@381 | 374 App (App (add var) (Const 1)) (Const 2). |

adam@381 | 375 |

adam@510 | 376 (** The argument [var] does not even appear in the function body for [add]. How can that be? By giving our terms expressive types, we allow Coq to infer many arguments for us. In fact, we do not even need to name the [var] argument! *) |

adam@381 | 377 |

adam@381 | 378 Example add' : Term (Func Nat (Func Nat Nat)) := fun _ => |

adam@381 | 379 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))). |

adam@381 | 380 |

adam@381 | 381 Example three_the_hard_way' : Term Nat := fun _ => |

adam@381 | 382 App (App (add' _) (Const 1)) (Const 2). |

adam@381 | 383 |

adam@510 | 384 (** Even though the [var] formal parameters appear as underscores, they _are_ mentioned in the function bodies that type inference calculates. *) |

adam@510 | 385 |

adam@381 | 386 |

adam@381 | 387 (** ** Functional Programming with PHOAS *) |

adam@381 | 388 |

adam@398 | 389 (** It may not be at all obvious that the PHOAS representation admits the crucial computable operations. The key to effective deconstruction of PHOAS terms is one principle: treat the [var] parameter as an unconstrained choice of _which data should be annotated on each variable_. We will begin with a simple example, that of counting how many variable nodes appear in a PHOAS term. This operation requires no data annotated on variables, so we simply annotate variables with [unit] values. Note that, when we go under binders in the cases for [Abs] and [Let], we must provide the data value to annotate on the new variable we pass beneath. For our current choice of [unit] data, we always pass [tt]. *) |

adam@381 | 390 |

adam@381 | 391 Fixpoint countVars t (e : term (fun _ => unit) t) : nat := |

adam@381 | 392 match e with |

adam@381 | 393 | Var _ _ => 1 |

adam@381 | 394 |

adam@381 | 395 | Const _ => 0 |

adam@381 | 396 | Plus e1 e2 => countVars e1 + countVars e2 |

adam@381 | 397 |

adam@381 | 398 | Abs _ _ e1 => countVars (e1 tt) |

adam@381 | 399 | App _ _ e1 e2 => countVars e1 + countVars e2 |

adam@381 | 400 |

adam@381 | 401 | Let _ _ e1 e2 => countVars e1 + countVars (e2 tt) |

adam@381 | 402 end. |

adam@381 | 403 |

adam@381 | 404 (** The above definition may seem a bit peculiar. What gave us the right to represent variables as [unit] values? Recall that our final representation of closed terms is as polymorphic functions. We merely specialize a closed term to exactly the right variable representation for the transformation we wish to perform. *) |

adam@381 | 405 |

adam@381 | 406 Definition CountVars t (E : Term t) := countVars (E (fun _ => unit)). |

adam@381 | 407 |

adam@381 | 408 (** It is easy to test that [CountVars] operates properly. *) |

adam@381 | 409 |

adam@381 | 410 Eval compute in CountVars three_the_hard_way. |

adam@381 | 411 (** %\vspace{-.15in}%[[ |

adam@381 | 412 = 2 |

adam@381 | 413 ]] |

adam@381 | 414 *) |

adam@381 | 415 |

adam@381 | 416 (** In fact, PHOAS can be used anywhere that first-order representations can. We will not go into all the details here, but the intuition is that it is possible to interconvert between PHOAS and any reasonable first-order representation. Here is a suggestive example, translating PHOAS terms into strings giving a first-order rendering. To implement this translation, the key insight is to tag variables with strings, giving their names. The function takes as an additional input a string giving the name to be assigned to the next variable introduced. We evolve this name by adding a prime to its end. To avoid getting bogged down in orthogonal details, we render all constants as the string ["N"]. *) |

adam@381 | 417 |

adam@381 | 418 Require Import String. |

adam@381 | 419 Open Scope string_scope. |

adam@381 | 420 |

adam@381 | 421 Fixpoint pretty t (e : term (fun _ => string) t) (x : string) : string := |

adam@381 | 422 match e with |

adam@381 | 423 | Var _ s => s |

adam@381 | 424 |

adam@381 | 425 | Const _ => "N" |

adam@381 | 426 | Plus e1 e2 => "(" ++ pretty e1 x ++ " + " ++ pretty e2 x ++ ")" |

adam@381 | 427 |

adam@381 | 428 | Abs _ _ e1 => "(fun " ++ x ++ " => " ++ pretty (e1 x) (x ++ "'") ++ ")" |

adam@381 | 429 | App _ _ e1 e2 => "(" ++ pretty e1 x ++ " " ++ pretty e2 x ++ ")" |

adam@381 | 430 |

adam@381 | 431 | Let _ _ e1 e2 => "(let " ++ x ++ " = " ++ pretty e1 x ++ " in " |

adam@381 | 432 ++ pretty (e2 x) (x ++ "'") ++ ")" |

adam@381 | 433 end. |

adam@381 | 434 |

adam@381 | 435 Definition Pretty t (E : Term t) := pretty (E (fun _ => string)) "x". |

adam@381 | 436 |

adam@381 | 437 Eval compute in Pretty three_the_hard_way. |

adam@381 | 438 (** %\vspace{-.15in}%[[ |

adam@381 | 439 = "(((fun x => (fun x' => (x + x'))) N) N)" |

adam@381 | 440 ]] |

adam@381 | 441 *) |

adam@381 | 442 |

adam@497 | 443 (** However, it is not necessary to convert to first-order form to support many common operations on terms. For instance, we can implement substitution of terms for variables. The key insight here is to _tag variables with terms_, so that, on encountering a variable, we can simply replace it by the term in its tag. We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute. During recursion, new variables are added, but they are only tagged with their own term equivalents. Note that this function [squash] is parameterized over a specific [var] choice. *) |

adam@381 | 444 |

adam@381 | 445 Fixpoint squash var t (e : term (term var) t) : term var t := |

adam@381 | 446 match e with |

adam@381 | 447 | Var _ e1 => e1 |

adam@381 | 448 |

adam@381 | 449 | Const n => Const n |

adam@381 | 450 | Plus e1 e2 => Plus (squash e1) (squash e2) |

adam@381 | 451 |

adam@381 | 452 | Abs _ _ e1 => Abs (fun x => squash (e1 (Var x))) |

adam@381 | 453 | App _ _ e1 e2 => App (squash e1) (squash e2) |

adam@381 | 454 |

adam@381 | 455 | Let _ _ e1 e2 => Let (squash e1) (fun x => squash (e2 (Var x))) |

adam@381 | 456 end. |

adam@381 | 457 |

adam@381 | 458 (** To define the final substitution function over terms with single free variables, we define [Term1], an analogue to [Term] that we defined before for closed terms. *) |

adam@381 | 459 |

adam@381 | 460 Definition Term1 (t1 t2 : type) := forall var, var t1 -> term var t2. |

adam@381 | 461 |

adam@381 | 462 (** Substitution is defined by (1) instantiating a [Term1] to tag variables with terms and (2) applying the result to a specific term to be substituted. Note how the parameter [var] of [squash] is instantiated: the body of [Subst] is itself a polymorphic quantification over [var], standing for a variable tag choice in the output term; and we use that input to compute a tag choice for the input term. *) |

adam@381 | 463 |

adam@381 | 464 Definition Subst (t1 t2 : type) (E : Term1 t1 t2) (E' : Term t1) : Term t2 := |

adam@381 | 465 fun var => squash (E (term var) (E' var)). |

adam@381 | 466 |

adam@381 | 467 Eval compute in Subst (fun _ x => Plus (Var x) (Const 3)) three_the_hard_way. |

adam@381 | 468 (** %\vspace{-.15in}%[[ |

adam@381 | 469 = fun var : type -> Type => |

adam@381 | 470 Plus |

adam@381 | 471 (App |

adam@381 | 472 (App |

adam@381 | 473 (Abs |

adam@381 | 474 (fun x : var Nat => |

adam@381 | 475 Abs (fun y : var Nat => Plus (Var x) (Var y)))) |

adam@381 | 476 (Const 1)) (Const 2)) (Const 3) |

adam@381 | 477 ]] |

adam@381 | 478 |

adam@398 | 479 One further development, which may seem surprising at first, is that we can also implement a usual term denotation function, when we _tag variables with their denotations_. *) |

adam@381 | 480 |

adam@381 | 481 Fixpoint termDenote t (e : term typeDenote t) : typeDenote t := |

adam@381 | 482 match e with |

adam@381 | 483 | Var _ v => v |

adam@381 | 484 |

adam@381 | 485 | Const n => n |

adam@381 | 486 | Plus e1 e2 => termDenote e1 + termDenote e2 |

adam@381 | 487 |

adam@381 | 488 | Abs _ _ e1 => fun x => termDenote (e1 x) |

adam@381 | 489 | App _ _ e1 e2 => (termDenote e1) (termDenote e2) |

adam@381 | 490 |

adam@381 | 491 | Let _ _ e1 e2 => termDenote (e2 (termDenote e1)) |

adam@381 | 492 end. |

adam@381 | 493 |

adam@381 | 494 Definition TermDenote t (E : Term t) : typeDenote t := |

adam@381 | 495 termDenote (E typeDenote). |

adam@381 | 496 |

adam@381 | 497 Eval compute in TermDenote three_the_hard_way. |

adam@381 | 498 (** %\vspace{-.15in}%[[ |

adam@381 | 499 = 3 |

adam@381 | 500 ]] |

adam@381 | 501 |

adam@381 | 502 To summarize, the PHOAS representation has all the expressive power of more standard first-order encodings, and a variety of translations are actually much more pleasant to implement than usual, thanks to the novel ability to tag variables with data. *) |

adam@381 | 503 |

adam@381 | 504 |

adam@381 | 505 (** ** Verifying Program Transformations *) |

adam@381 | 506 |

adam@381 | 507 (** Let us now revisit the three example program transformations from the last section. Each is easy to implement with PHOAS, and the last is substantially easier than with first-order representations. |

adam@381 | 508 |

adam@381 | 509 First, we have the recursive identity function, following the same pattern as in the previous subsection, with a helper function, polymorphic in a tag choice; and a final function that instantiates the choice appropriately. *) |

adam@381 | 510 |

adam@381 | 511 Fixpoint ident var t (e : term var t) : term var t := |

adam@381 | 512 match e with |

adam@381 | 513 | Var _ x => Var x |

adam@381 | 514 |

adam@381 | 515 | Const n => Const n |

adam@381 | 516 | Plus e1 e2 => Plus (ident e1) (ident e2) |

adam@381 | 517 |

adam@381 | 518 | Abs _ _ e1 => Abs (fun x => ident (e1 x)) |

adam@381 | 519 | App _ _ e1 e2 => App (ident e1) (ident e2) |

adam@381 | 520 |

adam@381 | 521 | Let _ _ e1 e2 => Let (ident e1) (fun x => ident (e2 x)) |

adam@381 | 522 end. |

adam@381 | 523 |

adam@381 | 524 Definition Ident t (E : Term t) : Term t := fun var => |

adam@381 | 525 ident (E var). |

adam@381 | 526 |

adam@381 | 527 (** Proving correctness is both easier and harder than in the last section, easier because we do not need to manipulate substitutions, and harder because we do the induction in an extra lemma about [ident], to establish the correctness theorem for [Ident]. *) |

adam@381 | 528 |

adam@381 | 529 Lemma identSound : forall t (e : term typeDenote t), |

adam@381 | 530 termDenote (ident e) = termDenote e. |

adam@497 | 531 induction e; pl. |

adam@381 | 532 Qed. |

adam@381 | 533 |

adam@381 | 534 Theorem IdentSound : forall t (E : Term t), |

adam@381 | 535 TermDenote (Ident E) = TermDenote E. |

adam@381 | 536 intros; apply identSound. |

adam@381 | 537 Qed. |

adam@381 | 538 |

adam@381 | 539 (** The translation of the constant-folding function and its proof work more or less the same way. *) |

adam@381 | 540 |

adam@381 | 541 Fixpoint cfold var t (e : term var t) : term var t := |

adam@381 | 542 match e with |

adam@381 | 543 | Plus e1 e2 => |

adam@381 | 544 let e1' := cfold e1 in |

adam@381 | 545 let e2' := cfold e2 in |

adam@381 | 546 match e1', e2' with |

adam@381 | 547 | Const n1, Const n2 => Const (n1 + n2) |

adam@381 | 548 | _, _ => Plus e1' e2' |

adam@381 | 549 end |

adam@381 | 550 |

adam@381 | 551 | Abs _ _ e1 => Abs (fun x => cfold (e1 x)) |

adam@381 | 552 | App _ _ e1 e2 => App (cfold e1) (cfold e2) |

adam@381 | 553 |

adam@381 | 554 | Let _ _ e1 e2 => Let (cfold e1) (fun x => cfold (e2 x)) |

adam@381 | 555 |

adam@381 | 556 | e => e |

adam@381 | 557 end. |

adam@381 | 558 |

adam@381 | 559 Definition Cfold t (E : Term t) : Term t := fun var => |

adam@381 | 560 cfold (E var). |

adam@381 | 561 |

adam@381 | 562 Lemma cfoldSound : forall t (e : term typeDenote t), |

adam@381 | 563 termDenote (cfold e) = termDenote e. |

adam@497 | 564 induction e; pl; |

adam@381 | 565 repeat (match goal with |

adam@414 | 566 | [ |- context[match ?E with Var _ _ => _ | _ => _ end] ] => |

adam@414 | 567 dep_destruct E |

adam@497 | 568 end; pl). |

adam@381 | 569 Qed. |

adam@381 | 570 |

adam@381 | 571 Theorem CfoldSound : forall t (E : Term t), |

adam@381 | 572 TermDenote (Cfold E) = TermDenote E. |

adam@381 | 573 intros; apply cfoldSound. |

adam@381 | 574 Qed. |

adam@381 | 575 |

adam@381 | 576 (** Things get more interesting in the [Let]-removal optimization. Our recursive helper function adapts the key idea from our earlier definitions of [squash] and [Subst]: tag variables with terms. We have a straightforward generalization of [squash], where only the [Let] case has changed, to tag the new variable with the term it is bound to, rather than just tagging the variable with itself as a term. *) |

adam@381 | 577 |

adam@381 | 578 Fixpoint unlet var t (e : term (term var) t) : term var t := |

adam@381 | 579 match e with |

adam@381 | 580 | Var _ e1 => e1 |

adam@381 | 581 |

adam@381 | 582 | Const n => Const n |

adam@381 | 583 | Plus e1 e2 => Plus (unlet e1) (unlet e2) |

adam@381 | 584 |

adam@381 | 585 | Abs _ _ e1 => Abs (fun x => unlet (e1 (Var x))) |

adam@381 | 586 | App _ _ e1 e2 => App (unlet e1) (unlet e2) |

adam@381 | 587 |

adam@381 | 588 | Let _ _ e1 e2 => unlet (e2 (unlet e1)) |

adam@381 | 589 end. |

adam@381 | 590 |

adam@381 | 591 Definition Unlet t (E : Term t) : Term t := fun var => |

adam@381 | 592 unlet (E (term var)). |

adam@381 | 593 |

adam@381 | 594 (** We can test [Unlet] first on an uninteresting example, [three_the_hard_way], which does not use [Let]. *) |

adam@381 | 595 |

adam@381 | 596 Eval compute in Unlet three_the_hard_way. |

adam@381 | 597 (** %\vspace{-.15in}%[[ |

adam@381 | 598 = fun var : type -> Type => |

adam@381 | 599 App |

adam@381 | 600 (App |

adam@381 | 601 (Abs |

adam@381 | 602 (fun x : var Nat => |

adam@381 | 603 Abs (fun x0 : var Nat => Plus (Var x) (Var x0)))) |

adam@381 | 604 (Const 1)) (Const 2) |

adam@381 | 605 ]] |

adam@381 | 606 |

adam@381 | 607 Next, we try a more interesting example, with some extra [Let]s introduced in [three_the_hard_way]. *) |

adam@381 | 608 |

adam@381 | 609 Definition three_a_harder_way : Term Nat := fun _ => |

adam@381 | 610 Let (Const 1) (fun x => Let (Const 2) (fun y => App (App (add _) (Var x)) (Var y))). |

adam@381 | 611 |

adam@381 | 612 Eval compute in Unlet three_a_harder_way. |

adam@381 | 613 (** %\vspace{-.15in}%[[ |

adam@381 | 614 = fun var : type -> Type => |

adam@381 | 615 App |

adam@381 | 616 (App |

adam@381 | 617 (Abs |

adam@381 | 618 (fun x : var Nat => |

adam@381 | 619 Abs (fun x0 : var Nat => Plus (Var x) (Var x0)))) |

adam@381 | 620 (Const 1)) (Const 2) |

adam@381 | 621 ]] |

adam@381 | 622 |

adam@381 | 623 The output is the same as in the previous test, confirming that [Unlet] operates properly here. |

adam@381 | 624 |

adam@381 | 625 Now we need to state a correctness theorem for [Unlet], based on an inductively proved lemma about [unlet]. It is not at all obvious how to arrive at a proper induction principle for the lemma. The problem is that we want to relate two instantiations of the same [Term], in a way where we know they share the same structure. Note that, while [Unlet] is defined to consider all possible [var] choices in the output term, the correctness proof conveniently only depends on the case of [var := typeDenote]. Thus, one parallel instantiation will set [var := typeDenote], to take the denotation of the original term. The other parallel instantiation will set [var := term typeDenote], to perform the [unlet] transformation in the original term. |

adam@381 | 626 |

adam@381 | 627 Here is a relation formalizing the idea that two terms are structurally the same, differing only by replacing the variable data of one with another isomorphic set of variable data in some possibly different type family. *) |

adam@381 | 628 |

adam@381 | 629 Section wf. |

adam@381 | 630 Variables var1 var2 : type -> Type. |

adam@381 | 631 |

adam@381 | 632 (** To formalize the tag isomorphism, we will use lists of values with the following record type. Each entry has an object language type and an appropriate tag for that type, in each of the two tag families [var1] and [var2]. *) |

adam@381 | 633 |

adam@381 | 634 Record varEntry := { |

adam@381 | 635 Ty : type; |

adam@381 | 636 First : var1 Ty; |

adam@381 | 637 Second : var2 Ty |

adam@381 | 638 }. |

adam@381 | 639 |

adam@381 | 640 (** Here is the inductive relation definition. An instance [wf G e1 e2] asserts that terms [e1] and [e2] are equivalent up to the variable tag isomorphism [G]. Note how the [Var] rule looks up an entry in [G], and the [Abs] and [Let] rules include recursive [wf] invocations inside the scopes of quantifiers to introduce parallel tag values to be considered as isomorphic. *) |

adam@381 | 641 |

adam@381 | 642 Inductive wf : list varEntry -> forall t, term var1 t -> term var2 t -> Prop := |

adam@381 | 643 | WfVar : forall G t x x', In {| Ty := t; First := x; Second := x' |} G |

adam@381 | 644 -> wf G (Var x) (Var x') |

adam@381 | 645 |

adam@381 | 646 | WfConst : forall G n, wf G (Const n) (Const n) |

adam@381 | 647 |

adam@381 | 648 | WfPlus : forall G e1 e2 e1' e2', wf G e1 e1' |

adam@381 | 649 -> wf G e2 e2' |

adam@381 | 650 -> wf G (Plus e1 e2) (Plus e1' e2') |

adam@381 | 651 |

adam@381 | 652 | WfAbs : forall G dom ran (e1 : _ dom -> term _ ran) e1', |

adam@381 | 653 (forall x1 x2, wf ({| First := x1; Second := x2 |} :: G) (e1 x1) (e1' x2)) |

adam@381 | 654 -> wf G (Abs e1) (Abs e1') |

adam@381 | 655 |

adam@381 | 656 | WfApp : forall G dom ran (e1 : term _ (Func dom ran)) (e2 : term _ dom) e1' e2', |

adam@381 | 657 wf G e1 e1' |

adam@381 | 658 -> wf G e2 e2' |

adam@381 | 659 -> wf G (App e1 e2) (App e1' e2') |

adam@381 | 660 |

adam@381 | 661 | WfLet : forall G t1 t2 e1 e1' (e2 : _ t1 -> term _ t2) e2', wf G e1 e1' |

adam@381 | 662 -> (forall x1 x2, wf ({| First := x1; Second := x2 |} :: G) (e2 x1) (e2' x2)) |

adam@381 | 663 -> wf G (Let e1 e2) (Let e1' e2'). |

adam@381 | 664 End wf. |

adam@381 | 665 |

adam@381 | 666 (** We can state a well-formedness condition for closed terms: for any two choices of tag type families, the parallel instantiations belong to the [wf] relation, starting from an empty variable isomorphism. *) |

adam@381 | 667 |

adam@381 | 668 Definition Wf t (E : Term t) := forall var1 var2, wf nil (E var1) (E var2). |

adam@381 | 669 |

adam@465 | 670 (** After digesting the syntactic details of [Wf], it is probably not hard to see that reasonable term encodings will satisfy it. For example: *) |

adam@381 | 671 |

adam@381 | 672 Theorem three_the_hard_way_Wf : Wf three_the_hard_way. |

adam@381 | 673 red; intros; repeat match goal with |

adam@381 | 674 | [ |- wf _ _ _ ] => constructor; intros |

adam@381 | 675 end; intuition. |

adam@381 | 676 Qed. |

adam@381 | 677 |

adam@497 | 678 (** Now we are ready to give a nice simple proof of correctness for [unlet]. First, we add one hint to apply a small variant of a standard library theorem connecting [Forall], a higher-order predicate asserting that every element of a list satisfies some property; and [In], the list membership predicate. *) |

adam@381 | 679 |

adam@381 | 680 Hint Extern 1 => match goal with |

adam@381 | 681 | [ H1 : Forall _ _, H2 : In _ _ |- _ ] => apply (Forall_In H1 _ H2) |

adam@381 | 682 end. |

adam@381 | 683 |

adam@381 | 684 (** The rest of the proof is about as automated as we could hope for. *) |

adam@381 | 685 |

adam@381 | 686 Lemma unletSound : forall G t (e1 : term _ t) e2, |

adam@381 | 687 wf G e1 e2 |

adam@381 | 688 -> Forall (fun ve => termDenote (First ve) = Second ve) G |

adam@381 | 689 -> termDenote (unlet e1) = termDenote e2. |

adam@497 | 690 induction 1; pl. |

adam@381 | 691 Qed. |

adam@381 | 692 |

adam@381 | 693 Theorem UnletSound : forall t (E : Term t), Wf E |

adam@381 | 694 -> TermDenote (Unlet E) = TermDenote E. |

adam@381 | 695 intros; eapply unletSound; eauto. |

adam@381 | 696 Qed. |

adam@381 | 697 |

adam@381 | 698 (** With this example, it is not obvious that the PHOAS encoding is more tractable than dependent de Bruijn. Where the de Bruijn version had [lift] and its helper functions, here we have [Wf] and its auxiliary definitions. In practice, [Wf] is defined once per object language, while such operations as [lift] often need to operate differently for different examples, forcing new implementations for new transformations. |

adam@381 | 699 |

adam@381 | 700 The reader may also have come up with another objection: via Curry-Howard, [wf] proofs may be thought of as first-order encodings of term syntax! For instance, the [In] hypothesis of rule [WfVar] is equivalent to a [member] value. There is some merit to this objection. However, as the proofs above show, we are able to reason about transformations using first-order representation only for their inputs, not their outputs. Furthermore, explicit numbering of variables remains absent from the proofs. |

adam@381 | 701 |

adam@381 | 702 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. *) |

adam@381 | 703 |

adam@381 | 704 |

adam@381 | 705 (** ** Establishing Term Well-Formedness *) |

adam@381 | 706 |

adam@434 | 707 (** 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. |

adam@381 | 708 |

adam@381 | 709 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]. |

adam@381 | 710 |

adam@398 | 711 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. *) |

adam@381 | 712 |

adam@381 | 713 Hint Constructors wf. |

adam@381 | 714 Hint Extern 1 (In _ _) => simpl; tauto. |

adam@381 | 715 Hint Extern 1 (Forall _ _) => eapply Forall_weaken; [ eassumption | simpl ]. |

adam@381 | 716 |

adam@381 | 717 Lemma wf_monotone : forall var1 var2 G t (e1 : term var1 t) (e2 : term var2 t), |

adam@381 | 718 wf G e1 e2 |

adam@381 | 719 -> forall G', Forall (fun x => In x G') G |

adam@381 | 720 -> wf G' e1 e2. |

adam@497 | 721 induction 1; pl; auto 6. |

adam@381 | 722 Qed. |

adam@381 | 723 |

adam@381 | 724 Hint Resolve wf_monotone Forall_In'. |

adam@381 | 725 |

adam@381 | 726 (** Now we are ready to prove that [unlet] preserves any [wf] instance. The key invariant has to do with the parallel execution of [unlet] on two different [var] instantiations of a particular term. Since [unlet] uses [term] as the type of variable data, our variable isomorphism context [G] contains pairs of terms, which, conveniently enough, allows us to state the invariant that any pair of terms in the context is also related by [wf]. *) |

adam@381 | 727 |

adam@381 | 728 Hint Extern 1 (wf _ _ _) => progress simpl. |

adam@381 | 729 |

adam@381 | 730 Lemma unletWf : forall var1 var2 G t (e1 : term (term var1) t) (e2 : term (term var2) t), |

adam@381 | 731 wf G e1 e2 |

adam@381 | 732 -> forall G', Forall (fun ve => wf G' (First ve) (Second ve)) G |

adam@381 | 733 -> wf G' (unlet e1) (unlet e2). |

adam@497 | 734 induction 1; pl; eauto 9. |

adam@381 | 735 Qed. |

adam@381 | 736 |

adam@381 | 737 (** Repackaging [unletWf] into a theorem about [Wf] and [Unlet] is straightforward. *) |

adam@381 | 738 |

adam@381 | 739 Theorem UnletWf : forall t (E : Term t), Wf E |

adam@381 | 740 -> Wf (Unlet E). |

adam@381 | 741 red; intros; apply unletWf with nil; auto. |

adam@381 | 742 Qed. |

adam@381 | 743 |

adam@381 | 744 (** This example demonstrates how we may need to use reasoning reminiscent of that associated with first-order representations, though the bookkeeping details are generally easier to manage, and bookkeeping theorems may generally be proved separately from the independently interesting theorems about program transformations. *) |

adam@381 | 745 |

adam@381 | 746 |

adam@381 | 747 (** ** A Few More Remarks *) |

adam@381 | 748 |

adam@381 | 749 (** Higher-order encodings derive their strength from reuse of the meta language's binding constructs. As a result, we can write encoded terms so that they look very similar to their informal counterparts, without variable numbering schemes like for de Bruijn indices. The example encodings above have demonstrated this fact, but modulo the clunkiness of explicit use of the constructors of [term]. After defining a few new Coq syntax notations, we can work with terms in an even more standard form. *) |

adam@381 | 750 |

adam@381 | 751 Infix "-->" := Func (right associativity, at level 52). |

adam@381 | 752 |

adam@381 | 753 Notation "^" := Var. |

adam@381 | 754 Notation "#" := Const. |

adam@381 | 755 Infix "@" := App (left associativity, at level 50). |

adam@381 | 756 Infix "@+" := Plus (left associativity, at level 50). |

adam@381 | 757 Notation "\ x : t , e" := (Abs (dom := t) (fun x => e)) |

adam@381 | 758 (no associativity, at level 51, x at level 0). |

adam@381 | 759 Notation "[ e ]" := (fun _ => e). |

adam@381 | 760 |

adam@381 | 761 Example Add : Term (Nat --> Nat --> Nat) := |

adam@381 | 762 [\x : Nat, \y : Nat, ^x @+ ^y]. |

adam@381 | 763 |

adam@381 | 764 Example Three_the_hard_way : Term Nat := |

adam@381 | 765 [Add _ @ #1 @ #2]. |

adam@381 | 766 |

adam@381 | 767 Eval compute in TermDenote Three_the_hard_way. |

adam@381 | 768 (** %\vspace{-.15in}%[[ |

adam@381 | 769 = 3 |

adam@381 | 770 ]] |

adam@381 | 771 *) |

adam@381 | 772 |

adam@381 | 773 End HigherOrder. |

adam@381 | 774 |

adam@381 | 775 (** The PHOAS approach shines here because we are working with an object language that has an easy embedding into Coq. That is, there is a straightforward recursive function translating object terms into terms of Gallina. All Gallina programs terminate, so clearly we cannot hope to find such embeddings for Turing-complete languages; and non-Turing-complete languages may still require much more involved translations. I have some work%~\cite{CompilerPOPL10}% on modeling semantics of Turing-complete languages with PHOAS, but my impression is that there are many more advances left to be made in this field, possibly with completely new term representations that we have not yet been clever enough to think up. *) |