Mercurial > cpdt > repo

annotate src/ProgLang.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents fd6ec9b2dccb
children dac7a2705b00
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@534 33 end; crush).
adam@381 34
adam@381 35 (** At this point in the book source, some auxiliary proofs also appear. *)
adam@381 36
adam@381 37 (* begin hide *)
adam@381 38 Section hmap.
adam@381 39 Variable A : Type.
adam@381 40 Variables B1 B2 B3 : A -> Type.
adam@381 41
adam@381 42 Variable f1 : forall x, B1 x -> B2 x.
adam@381 43 Variable f2 : forall x, B2 x -> B3 x.
adam@381 44
adam@381 45 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 46 induction hl; crush.
adam@381 47 Qed.
adam@381 48 End hmap.
adam@381 49
adam@381 50 Section Forall.
adam@381 51 Variable A : Type.
adam@381 52 Variable P : A -> Prop.
adam@381 53
adam@381 54 Theorem Forall_In : forall ls, Forall P ls -> forall x, In x ls -> P x.
adam@381 55 induction 1; crush.
adam@381 56 Qed.
adam@381 57
adam@381 58 Theorem Forall_In' : forall ls, (forall x, In x ls -> P x) -> Forall P ls.
adam@381 59 induction ls; crush.
adam@381 60 Qed.
adam@381 61
adam@381 62 Variable P' : A -> Prop.
adam@381 63
adam@381 64 Theorem Forall_weaken : forall ls, Forall P ls
adam@381 65 -> (forall x, P x -> P' x)
adam@381 66 -> Forall P' ls.
adam@381 67 induction 1; crush.
adam@381 68 Qed.
adam@381 69 End Forall.
adam@381 70 (* end hide *)
adam@381 71
adam@381 72 (** 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 73
adam@381 74 Inductive type : Type :=
adam@381 75 | Nat : type
adam@381 76 | Func : type -> type -> type.
adam@381 77
adam@381 78 Fixpoint typeDenote (t : type) : Type :=
adam@381 79 match t with
adam@381 80 | Nat => nat
adam@381 81 | Func t1 t2 => typeDenote t1 -> typeDenote t2
adam@381 82 end.
adam@381 83
adam@381 84 (** 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 85
adam@381 86
adam@381 87 (** * Dependent de Bruijn Indices *)
adam@381 88
adam@465 89 (** 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 90
adam@381 91 Module FirstOrder.
adam@381 92
adam@381 93 (** Here is the definition of the [term] type, including variables, constants, addition, function abstraction and application, and let binding of local variables. *)
adam@381 94
adam@381 95 Inductive term : list type -> type -> Type :=
adam@381 96 | Var : forall G t, member t G -> term G t
adam@381 97
adam@381 98 | Const : forall G, nat -> term G Nat
adam@381 99 | Plus : forall G, term G Nat -> term G Nat -> term G Nat
adam@381 100
adam@381 101 | Abs : forall G dom ran, term (dom :: G) ran -> term G (Func dom ran)
adam@381 102 | App : forall G dom ran, term G (Func dom ran) -> term G dom -> term G ran
adam@381 103
adam@381 104 | Let : forall G t1 t2, term G t1 -> term (t1 :: G) t2 -> term G t2.
adam@381 105
adam@381 106 Implicit Arguments Const [G].
adam@381 107
adam@381 108 (** 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 109
adam@381 110 Example add : term nil (Func Nat (Func Nat Nat)) :=
adam@381 111 Abs (Abs (Plus (Var (HNext HFirst)) (Var HFirst))).
adam@381 112
adam@381 113 Example three_the_hard_way : term nil Nat :=
adam@381 114 App (App add (Const 1)) (Const 2).
adam@381 115
adam@381 116 (** 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 117
adam@381 118 Fixpoint termDenote G t (e : term G t) : hlist typeDenote G -> typeDenote t :=
adam@381 119 match e with
adam@381 120 | Var _ _ x => fun s => hget s x
adam@381 121
adam@381 122 | Const _ n => fun _ => n
adam@381 123 | Plus _ e1 e2 => fun s => termDenote e1 s + termDenote e2 s
adam@381 124
adam@381 125 | Abs _ _ _ e1 => fun s => fun x => termDenote e1 (x ::: s)
adam@381 126 | App _ _ _ e1 e2 => fun s => (termDenote e1 s) (termDenote e2 s)
adam@381 127
adam@381 128 | Let _ _ _ e1 e2 => fun s => termDenote e2 (termDenote e1 s ::: s)
adam@381 129 end.
adam@381 130
adam@398 131 (** 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 132
adam@381 133 Fixpoint ident G t (e : term G t) : term G t :=
adam@381 134 match e with
adam@381 135 | Var _ _ x => Var x
adam@381 136
adam@381 137 | Const _ n => Const n
adam@381 138 | Plus _ e1 e2 => Plus (ident e1) (ident e2)
adam@381 139
adam@381 140 | Abs _ _ _ e1 => Abs (ident e1)
adam@381 141 | App _ _ _ e1 e2 => App (ident e1) (ident e2)
adam@381 142
adam@381 143 | Let _ _ _ e1 e2 => Let (ident e1) (ident e2)
adam@381 144 end.
adam@381 145
adam@381 146 Theorem identSound : forall G t (e : term G t) s,
adam@381 147 termDenote (ident e) s = termDenote e s.
adam@497 148 induction e; pl.
adam@381 149 Qed.
adam@381 150
adam@398 151 (** A slightly more ambitious transformation belongs to the family of _constant folding_ optimizations we have used as examples in other chapters. *)
adam@398 152
adam@381 153 Fixpoint cfold G t (e : term G t) : term G t :=
adam@381 154 match e with
adam@381 155 | Plus G e1 e2 =>
adam@381 156 let e1' := cfold e1 in
adam@381 157 let e2' := cfold e2 in
adam@398 158 let maybeOpt := match e1' return _ with
adam@398 159 | Const _ n1 =>
adam@398 160 match e2' return _ with
adam@398 161 | Const _ n2 => Some (Const (n1 + n2))
adam@398 162 | _ => None
adam@398 163 end
adam@398 164 | _ => None
adam@398 165 end in
adam@398 166 match maybeOpt with
adam@398 167 | None => Plus e1' e2'
adam@398 168 | Some e' => e'
adam@398 169 end
adam@381 170
adam@381 171 | Abs _ _ _ e1 => Abs (cfold e1)
adam@381 172 | App _ _ _ e1 e2 => App (cfold e1) (cfold e2)
adam@381 173
adam@381 174 | Let _ _ _ e1 e2 => Let (cfold e1) (cfold e2)
adam@381 175
adam@381 176 | e => e
adam@381 177 end.
adam@381 178
adam@381 179 (** The correctness proof is more complex, but only slightly so. *)
adam@381 180
adam@381 181 Theorem cfoldSound : forall G t (e : term G t) s,
adam@381 182 termDenote (cfold e) s = termDenote e s.
adam@497 183 induction e; pl;
adam@381 184 repeat (match goal with
adam@414 185 | [ |- context[match ?E with Var _ _ _ => _ | _ => _ end] ] =>
adam@414 186 dep_destruct E
adam@497 187 end; pl).
adam@381 188 Qed.
adam@381 189
adam@414 190 (** 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 191
adam@434 192 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 193
adam@381 194 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 195
adam@381 196 Fixpoint insertAt (t : type) (G : list type) (n : nat) {struct n} : list type :=
adam@381 197 match n with
adam@381 198 | O => t :: G
adam@381 199 | S n' => match G with
adam@381 200 | nil => t :: G
adam@381 201 | t' :: G' => t' :: insertAt t G' n'
adam@381 202 end
adam@381 203 end.
adam@381 204
adam@381 205 (** Another function lifts bound variable instances, which we represent with [member] values. *)
adam@381 206
adam@381 207 Fixpoint liftVar t G (x : member t G) t' n : member t (insertAt t' G n) :=
adam@381 208 match x with
adam@381 209 | HFirst G' => match n return member t (insertAt t' (t :: G') n) with
adam@381 210 | O => HNext HFirst
adam@381 211 | _ => HFirst
adam@381 212 end
adam@381 213 | HNext t'' G' x' => match n return member t (insertAt t' (t'' :: G') n) with
adam@381 214 | O => HNext (HNext x')
adam@381 215 | S n' => HNext (liftVar x' t' n')
adam@381 216 end
adam@381 217 end.
adam@381 218
adam@381 219 (** The final helper function for lifting allows us to insert a new variable anywhere in a typing context. *)
adam@381 220
adam@381 221 Fixpoint lift' G t' n t (e : term G t) : term (insertAt t' G n) t :=
adam@381 222 match e with
adam@381 223 | Var _ _ x => Var (liftVar x t' n)
adam@381 224
adam@381 225 | Const _ n => Const n
adam@381 226 | Plus _ e1 e2 => Plus (lift' t' n e1) (lift' t' n e2)
adam@381 227
adam@381 228 | Abs _ _ _ e1 => Abs (lift' t' (S n) e1)
adam@381 229 | App _ _ _ e1 e2 => App (lift' t' n e1) (lift' t' n e2)
adam@381 230
adam@381 231 | Let _ _ _ e1 e2 => Let (lift' t' n e1) (lift' t' (S n) e2)
adam@381 232 end.
adam@381 233
adam@398 234 (** 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 235
adam@381 236 Definition lift G t' t (e : term G t) : term (t' :: G) t :=
adam@381 237 lift' t' O e.
adam@381 238
adam@381 239 (** 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 240
adam@381 241 Fixpoint unlet G t (e : term G t) G' : hlist (term G') G -> term G' t :=
adam@381 242 match e with
adam@381 243 | Var _ _ x => fun s => hget s x
adam@381 244
adam@381 245 | Const _ n => fun _ => Const n
adam@381 246 | Plus _ e1 e2 => fun s => Plus (unlet e1 s) (unlet e2 s)
adam@381 247
adam@381 248 | Abs _ _ _ e1 => fun s => Abs (unlet e1 (Var HFirst ::: hmap (lift _) s))
adam@381 249 | App _ _ _ e1 e2 => fun s => App (unlet e1 s) (unlet e2 s)
adam@381 250
adam@381 251 | Let _ t1 _ e1 e2 => fun s => unlet e2 (unlet e1 s ::: s)
adam@381 252 end.
adam@381 253
adam@381 254 (** 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 255
adam@381 256 Fixpoint insertAtS (t : type) (x : typeDenote t) (G : list type) (n : nat) {struct n}
adam@381 257 : hlist typeDenote G -> hlist typeDenote (insertAt t G n) :=
adam@381 258 match n with
adam@381 259 | O => fun s => x ::: s
adam@381 260 | S n' => match G return hlist typeDenote G
adam@381 261 -> hlist typeDenote (insertAt t G (S n')) with
adam@381 262 | nil => fun s => x ::: s
adam@381 263 | t' :: G' => fun s => hhd s ::: insertAtS t x n' (htl s)
adam@381 264 end
adam@381 265 end.
adam@381 266
adam@381 267 Implicit Arguments insertAtS [t G].
adam@381 268
adam@381 269 (** 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 270
adam@381 271 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n,
adam@381 272 hget s m = hget (insertAtS x n s) (liftVar m t' n).
adam@497 273 induction m; destruct n; dep_destruct s; pl.
adam@381 274 Qed.
adam@381 275
adam@381 276 Hint Resolve liftVarSound.
adam@381 277
adam@381 278 (** An analogous lemma establishes correctness of [lift']. *)
adam@381 279
adam@381 280 Lemma lift'Sound : forall G t' (x : typeDenote t') t (e : term G t) n s,
adam@381 281 termDenote e s = termDenote (lift' t' n e) (insertAtS x n s).
adam@497 282 induction e; pl;
adam@381 283 repeat match goal with
adam@381 284 | [ IH : forall n s, _ = termDenote (lift' _ n ?E) _
adam@381 285 |- context[lift' _ (S ?N) ?E] ] => specialize (IH (S N))
adam@497 286 end; pl.
adam@381 287 Qed.
adam@381 288
adam@381 289 (** Correctness of [lift] itself is an easy corollary. *)
adam@381 290
adam@381 291 Lemma liftSound : forall G t' (x : typeDenote t') t (e : term G t) s,
adam@381 292 termDenote (lift t' e) (x ::: s) = termDenote e s.
adam@381 293 unfold lift; intros; rewrite (lift'Sound _ x e O); trivial.
adam@381 294 Qed.
adam@381 295
adam@381 296 Hint Rewrite hget_hmap hmap_hmap liftSound.
adam@381 297
adam@381 298 (** Finally, we can prove correctness of [unletSound] for terms in arbitrary typing environments. *)
adam@381 299
adam@381 300 Lemma unletSound' : forall G t (e : term G t) G' (s : hlist (term G') G) s1,
adam@381 301 termDenote (unlet e s) s1
adam@381 302 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s).
adam@497 303 induction e; pl.
adam@381 304 Qed.
adam@381 305
adam@510 306 (** 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 307
adam@381 308 Theorem unletSound : forall t (e : term nil t),
adam@381 309 termDenote (unlet e HNil) HNil = termDenote e HNil.
adam@381 310 intros; apply unletSound'.
adam@381 311 Qed.
adam@381 312
adam@381 313 End FirstOrder.
adam@381 314
adam@381 315 (** 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 316
adam@381 317
adam@381 318 (** * Parametric Higher-Order Abstract Syntax *)
adam@381 319
adam@510 320 (** 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 321
adam@381 322 Module HigherOrder.
adam@381 323
adam@398 324 (** 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 325
adam@381 326 (** %\vspace{-.15in}%[[
adam@381 327 Inductive term : type -> Type :=
adam@381 328 | Const : nat -> term Nat
adam@381 329 | Plus : term Nat -> term Nat -> term Nat
adam@381 330
adam@381 331 | Abs : forall dom ran, (term dom -> term ran) -> term (Func dom ran)
adam@381 332 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran
adam@381 333
adam@381 334 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2.
adam@381 335 ]]
adam@381 336
adam@464 337 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 338
adam@510 339 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 340
adam@381 341 Section var.
adam@381 342 Variable var : type -> Type.
adam@381 343
adam@381 344 Inductive term : type -> Type :=
adam@381 345 | Var : forall t, var t -> term t
adam@381 346
adam@381 347 | Const : nat -> term Nat
adam@381 348 | Plus : term Nat -> term Nat -> term Nat
adam@381 349
adam@381 350 | Abs : forall dom ran, (var dom -> term ran) -> term (Func dom ran)
adam@381 351 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran
adam@381 352
adam@381 353 | Let : forall t1 t2, term t1 -> (var t1 -> term t2) -> term t2.
adam@381 354 End var.
adam@381 355
adam@381 356 Implicit Arguments Var [var t].
adam@381 357 Implicit Arguments Const [var].
adam@381 358 Implicit Arguments Abs [var dom ran].
adam@381 359
adam@398 360 (** 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 361
adam@381 362 We write the final type of a closed term using polymorphic quantification over all possible choices of [var] type family. *)
adam@381 363
adam@381 364 Definition Term t := forall var, term var t.
adam@381 365
adam@398 366 (** 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 367
adam@381 368 Example add : Term (Func Nat (Func Nat Nat)) := fun var =>
adam@381 369 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))).
adam@381 370
adam@381 371 Example three_the_hard_way : Term Nat := fun var =>
adam@381 372 App (App (add var) (Const 1)) (Const 2).
adam@381 373
adam@510 374 (** 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 375
adam@381 376 Example add' : Term (Func Nat (Func Nat Nat)) := fun _ =>
adam@381 377 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))).
adam@381 378
adam@381 379 Example three_the_hard_way' : Term Nat := fun _ =>
adam@381 380 App (App (add' _) (Const 1)) (Const 2).
adam@381 381
adam@510 382 (** Even though the [var] formal parameters appear as underscores, they _are_ mentioned in the function bodies that type inference calculates. *)
adam@510 383
adam@381 384
adam@381 385 (** ** Functional Programming with PHOAS *)
adam@381 386
adam@398 387 (** 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 388
adam@381 389 Fixpoint countVars t (e : term (fun _ => unit) t) : nat :=
adam@381 390 match e with
adam@381 391 | Var _ _ => 1
adam@381 392
adam@381 393 | Const _ => 0
adam@381 394 | Plus e1 e2 => countVars e1 + countVars e2
adam@381 395
adam@381 396 | Abs _ _ e1 => countVars (e1 tt)
adam@381 397 | App _ _ e1 e2 => countVars e1 + countVars e2
adam@381 398
adam@381 399 | Let _ _ e1 e2 => countVars e1 + countVars (e2 tt)
adam@381 400 end.
adam@381 401
adam@381 402 (** 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 403
adam@381 404 Definition CountVars t (E : Term t) := countVars (E (fun _ => unit)).
adam@381 405
adam@381 406 (** It is easy to test that [CountVars] operates properly. *)
adam@381 407
adam@381 408 Eval compute in CountVars three_the_hard_way.
adam@381 409 (** %\vspace{-.15in}%[[
adam@381 410 = 2
adam@381 411 ]]
adam@381 412 *)
adam@381 413
adam@381 414 (** 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 415
adam@381 416 Require Import String.
adam@381 417 Open Scope string_scope.
adam@381 418
adam@381 419 Fixpoint pretty t (e : term (fun _ => string) t) (x : string) : string :=
adam@381 420 match e with
adam@381 421 | Var _ s => s
adam@381 422
adam@381 423 | Const _ => "N"
adam@381 424 | Plus e1 e2 => "(" ++ pretty e1 x ++ " + " ++ pretty e2 x ++ ")"
adam@381 425
adam@381 426 | Abs _ _ e1 => "(fun " ++ x ++ " => " ++ pretty (e1 x) (x ++ "'") ++ ")"
adam@381 427 | App _ _ e1 e2 => "(" ++ pretty e1 x ++ " " ++ pretty e2 x ++ ")"
adam@381 428
adam@381 429 | Let _ _ e1 e2 => "(let " ++ x ++ " = " ++ pretty e1 x ++ " in "
adam@381 430 ++ pretty (e2 x) (x ++ "'") ++ ")"
adam@381 431 end.
adam@381 432
adam@381 433 Definition Pretty t (E : Term t) := pretty (E (fun _ => string)) "x".
adam@381 434
adam@381 435 Eval compute in Pretty three_the_hard_way.
adam@381 436 (** %\vspace{-.15in}%[[
adam@381 437 = "(((fun x => (fun x' => (x + x'))) N) N)"
adam@381 438 ]]
adam@381 439 *)
adam@381 440
adam@497 441 (** 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 442
adam@381 443 Fixpoint squash var t (e : term (term var) t) : term var t :=
adam@381 444 match e with
adam@381 445 | Var _ e1 => e1
adam@381 446
adam@381 447 | Const n => Const n
adam@381 448 | Plus e1 e2 => Plus (squash e1) (squash e2)
adam@381 449
adam@381 450 | Abs _ _ e1 => Abs (fun x => squash (e1 (Var x)))
adam@381 451 | App _ _ e1 e2 => App (squash e1) (squash e2)
adam@381 452
adam@381 453 | Let _ _ e1 e2 => Let (squash e1) (fun x => squash (e2 (Var x)))
adam@381 454 end.
adam@381 455
adam@381 456 (** 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 457
adam@381 458 Definition Term1 (t1 t2 : type) := forall var, var t1 -> term var t2.
adam@381 459
adam@381 460 (** 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 461
adam@381 462 Definition Subst (t1 t2 : type) (E : Term1 t1 t2) (E' : Term t1) : Term t2 :=
adam@381 463 fun var => squash (E (term var) (E' var)).
adam@381 464
adam@381 465 Eval compute in Subst (fun _ x => Plus (Var x) (Const 3)) three_the_hard_way.
adam@381 466 (** %\vspace{-.15in}%[[
adam@381 467 = fun var : type -> Type =>
adam@381 468 Plus
adam@381 469 (App
adam@381 470 (App
adam@381 471 (Abs
adam@381 472 (fun x : var Nat =>
adam@381 473 Abs (fun y : var Nat => Plus (Var x) (Var y))))
adam@381 474 (Const 1)) (Const 2)) (Const 3)
adam@381 475 ]]
adam@381 476
adam@398 477 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 478
adam@381 479 Fixpoint termDenote t (e : term typeDenote t) : typeDenote t :=
adam@381 480 match e with
adam@381 481 | Var _ v => v
adam@381 482
adam@381 483 | Const n => n
adam@381 484 | Plus e1 e2 => termDenote e1 + termDenote e2
adam@381 485
adam@381 486 | Abs _ _ e1 => fun x => termDenote (e1 x)
adam@381 487 | App _ _ e1 e2 => (termDenote e1) (termDenote e2)
adam@381 488
adam@381 489 | Let _ _ e1 e2 => termDenote (e2 (termDenote e1))
adam@381 490 end.
adam@381 491
adam@381 492 Definition TermDenote t (E : Term t) : typeDenote t :=
adam@381 493 termDenote (E typeDenote).
adam@381 494
adam@381 495 Eval compute in TermDenote three_the_hard_way.
adam@381 496 (** %\vspace{-.15in}%[[
adam@381 497 = 3
adam@381 498 ]]
adam@381 499
adam@381 500 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 501
adam@381 502
adam@381 503 (** ** Verifying Program Transformations *)
adam@381 504
adam@381 505 (** 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 506
adam@381 507 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 508
adam@381 509 Fixpoint ident var t (e : term var t) : term var t :=
adam@381 510 match e with
adam@381 511 | Var _ x => Var x
adam@381 512
adam@381 513 | Const n => Const n
adam@381 514 | Plus e1 e2 => Plus (ident e1) (ident e2)
adam@381 515
adam@381 516 | Abs _ _ e1 => Abs (fun x => ident (e1 x))
adam@381 517 | App _ _ e1 e2 => App (ident e1) (ident e2)
adam@381 518
adam@381 519 | Let _ _ e1 e2 => Let (ident e1) (fun x => ident (e2 x))
adam@381 520 end.
adam@381 521
adam@381 522 Definition Ident t (E : Term t) : Term t := fun var =>
adam@381 523 ident (E var).
adam@381 524
adam@381 525 (** 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 526
adam@381 527 Lemma identSound : forall t (e : term typeDenote t),
adam@381 528 termDenote (ident e) = termDenote e.
adam@497 529 induction e; pl.
adam@381 530 Qed.
adam@381 531
adam@381 532 Theorem IdentSound : forall t (E : Term t),
adam@381 533 TermDenote (Ident E) = TermDenote E.
adam@381 534 intros; apply identSound.
adam@381 535 Qed.
adam@381 536
adam@381 537 (** The translation of the constant-folding function and its proof work more or less the same way. *)
adam@381 538
adam@381 539 Fixpoint cfold var t (e : term var t) : term var t :=
adam@381 540 match e with
adam@381 541 | Plus e1 e2 =>
adam@381 542 let e1' := cfold e1 in
adam@381 543 let e2' := cfold e2 in
adam@381 544 match e1', e2' with
adam@381 545 | Const n1, Const n2 => Const (n1 + n2)
adam@381 546 | _, _ => Plus e1' e2'
adam@381 547 end
adam@381 548
adam@381 549 | Abs _ _ e1 => Abs (fun x => cfold (e1 x))
adam@381 550 | App _ _ e1 e2 => App (cfold e1) (cfold e2)
adam@381 551
adam@381 552 | Let _ _ e1 e2 => Let (cfold e1) (fun x => cfold (e2 x))
adam@381 553
adam@381 554 | e => e
adam@381 555 end.
adam@381 556
adam@381 557 Definition Cfold t (E : Term t) : Term t := fun var =>
adam@381 558 cfold (E var).
adam@381 559
adam@381 560 Lemma cfoldSound : forall t (e : term typeDenote t),
adam@381 561 termDenote (cfold e) = termDenote e.
adam@497 562 induction e; pl;
adam@381 563 repeat (match goal with
adam@414 564 | [ |- context[match ?E with Var _ _ => _ | _ => _ end] ] =>
adam@414 565 dep_destruct E
adam@497 566 end; pl).
adam@381 567 Qed.
adam@381 568
adam@381 569 Theorem CfoldSound : forall t (E : Term t),
adam@381 570 TermDenote (Cfold E) = TermDenote E.
adam@381 571 intros; apply cfoldSound.
adam@381 572 Qed.
adam@381 573
adam@381 574 (** 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 575
adam@381 576 Fixpoint unlet var t (e : term (term var) t) : term var t :=
adam@381 577 match e with
adam@381 578 | Var _ e1 => e1
adam@381 579
adam@381 580 | Const n => Const n
adam@381 581 | Plus e1 e2 => Plus (unlet e1) (unlet e2)
adam@381 582
adam@381 583 | Abs _ _ e1 => Abs (fun x => unlet (e1 (Var x)))
adam@381 584 | App _ _ e1 e2 => App (unlet e1) (unlet e2)
adam@381 585
adam@381 586 | Let _ _ e1 e2 => unlet (e2 (unlet e1))
adam@381 587 end.
adam@381 588
adam@381 589 Definition Unlet t (E : Term t) : Term t := fun var =>
adam@381 590 unlet (E (term var)).
adam@381 591
adam@381 592 (** We can test [Unlet] first on an uninteresting example, [three_the_hard_way], which does not use [Let]. *)
adam@381 593
adam@381 594 Eval compute in Unlet three_the_hard_way.
adam@381 595 (** %\vspace{-.15in}%[[
adam@381 596 = fun var : type -> Type =>
adam@381 597 App
adam@381 598 (App
adam@381 599 (Abs
adam@381 600 (fun x : var Nat =>
adam@381 601 Abs (fun x0 : var Nat => Plus (Var x) (Var x0))))
adam@381 602 (Const 1)) (Const 2)
adam@381 603 ]]
adam@381 604
adam@381 605 Next, we try a more interesting example, with some extra [Let]s introduced in [three_the_hard_way]. *)
adam@381 606
adam@381 607 Definition three_a_harder_way : Term Nat := fun _ =>
adam@381 608 Let (Const 1) (fun x => Let (Const 2) (fun y => App (App (add _) (Var x)) (Var y))).
adam@381 609
adam@381 610 Eval compute in Unlet three_a_harder_way.
adam@381 611 (** %\vspace{-.15in}%[[
adam@381 612 = fun var : type -> Type =>
adam@381 613 App
adam@381 614 (App
adam@381 615 (Abs
adam@381 616 (fun x : var Nat =>
adam@381 617 Abs (fun x0 : var Nat => Plus (Var x) (Var x0))))
adam@381 618 (Const 1)) (Const 2)
adam@381 619 ]]
adam@381 620
adam@381 621 The output is the same as in the previous test, confirming that [Unlet] operates properly here.
adam@381 622
adam@381 623 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 624
adam@381 625 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 626
adam@381 627 Section wf.
adam@381 628 Variables var1 var2 : type -> Type.
adam@381 629
adam@381 630 (** 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 631
adam@381 632 Record varEntry := {
adam@381 633 Ty : type;
adam@381 634 First : var1 Ty;
adam@381 635 Second : var2 Ty
adam@381 636 }.
adam@381 637
adam@381 638 (** 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 639
adam@381 640 Inductive wf : list varEntry -> forall t, term var1 t -> term var2 t -> Prop :=
adam@381 641 | WfVar : forall G t x x', In {| Ty := t; First := x; Second := x' |} G
adam@381 642 -> wf G (Var x) (Var x')
adam@381 643
adam@381 644 | WfConst : forall G n, wf G (Const n) (Const n)
adam@381 645
adam@381 646 | WfPlus : forall G e1 e2 e1' e2', wf G e1 e1'
adam@381 647 -> wf G e2 e2'
adam@381 648 -> wf G (Plus e1 e2) (Plus e1' e2')
adam@381 649
adam@381 650 | WfAbs : forall G dom ran (e1 : _ dom -> term _ ran) e1',
adam@381 651 (forall x1 x2, wf ({| First := x1; Second := x2 |} :: G) (e1 x1) (e1' x2))
adam@381 652 -> wf G (Abs e1) (Abs e1')
adam@381 653
adam@381 654 | WfApp : forall G dom ran (e1 : term _ (Func dom ran)) (e2 : term _ dom) e1' e2',
adam@381 655 wf G e1 e1'
adam@381 656 -> wf G e2 e2'
adam@381 657 -> wf G (App e1 e2) (App e1' e2')
adam@381 658
adam@381 659 | WfLet : forall G t1 t2 e1 e1' (e2 : _ t1 -> term _ t2) e2', wf G e1 e1'
adam@381 660 -> (forall x1 x2, wf ({| First := x1; Second := x2 |} :: G) (e2 x1) (e2' x2))
adam@381 661 -> wf G (Let e1 e2) (Let e1' e2').
adam@381 662 End wf.
adam@381 663
adam@381 664 (** 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 665
adam@381 666 Definition Wf t (E : Term t) := forall var1 var2, wf nil (E var1) (E var2).
adam@381 667
adam@465 668 (** 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 669
adam@381 670 Theorem three_the_hard_way_Wf : Wf three_the_hard_way.
adam@381 671 red; intros; repeat match goal with
adam@381 672 | [ |- wf _ _ _ ] => constructor; intros
adam@381 673 end; intuition.
adam@381 674 Qed.
adam@381 675
adam@497 676 (** 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 677
adam@381 678 Hint Extern 1 => match goal with
adam@381 679 | [ H1 : Forall _ _, H2 : In _ _ |- _ ] => apply (Forall_In H1 _ H2)
adam@381 680 end.
adam@381 681
adam@381 682 (** The rest of the proof is about as automated as we could hope for. *)
adam@381 683
adam@381 684 Lemma unletSound : forall G t (e1 : term _ t) e2,
adam@381 685 wf G e1 e2
adam@381 686 -> Forall (fun ve => termDenote (First ve) = Second ve) G
adam@381 687 -> termDenote (unlet e1) = termDenote e2.
adam@497 688 induction 1; pl.
adam@381 689 Qed.
adam@381 690
adam@381 691 Theorem UnletSound : forall t (E : Term t), Wf E
adam@381 692 -> TermDenote (Unlet E) = TermDenote E.
adam@381 693 intros; eapply unletSound; eauto.
adam@381 694 Qed.
adam@381 695
adam@381 696 (** 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 697
adam@381 698 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 699
adam@381 700 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 701
adam@381 702
adam@381 703 (** ** Establishing Term Well-Formedness *)
adam@381 704
adam@434 705 (** 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 706
adam@381 707 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 708
adam@398 709 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 710
adam@381 711 Hint Constructors wf.
adam@381 712 Hint Extern 1 (In _ _) => simpl; tauto.
adam@381 713 Hint Extern 1 (Forall _ _) => eapply Forall_weaken; [ eassumption | simpl ].
adam@381 714
adam@381 715 Lemma wf_monotone : forall var1 var2 G t (e1 : term var1 t) (e2 : term var2 t),
adam@381 716 wf G e1 e2
adam@381 717 -> forall G', Forall (fun x => In x G') G
adam@381 718 -> wf G' e1 e2.
adam@497 719 induction 1; pl; auto 6.
adam@381 720 Qed.
adam@381 721
adam@381 722 Hint Resolve wf_monotone Forall_In'.
adam@381 723
adam@381 724 (** 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 725
adam@381 726 Hint Extern 1 (wf _ _ _) => progress simpl.
adam@381 727
adam@381 728 Lemma unletWf : forall var1 var2 G t (e1 : term (term var1) t) (e2 : term (term var2) t),
adam@381 729 wf G e1 e2
adam@381 730 -> forall G', Forall (fun ve => wf G' (First ve) (Second ve)) G
adam@381 731 -> wf G' (unlet e1) (unlet e2).
adam@497 732 induction 1; pl; eauto 9.
adam@381 733 Qed.
adam@381 734
adam@381 735 (** Repackaging [unletWf] into a theorem about [Wf] and [Unlet] is straightforward. *)
adam@381 736
adam@381 737 Theorem UnletWf : forall t (E : Term t), Wf E
adam@381 738 -> Wf (Unlet E).
adam@381 739 red; intros; apply unletWf with nil; auto.
adam@381 740 Qed.
adam@381 741
adam@381 742 (** 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 743
adam@381 744
adam@381 745 (** ** A Few More Remarks *)
adam@381 746
adam@381 747 (** 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 748
adam@381 749 Infix "-->" := Func (right associativity, at level 52).
adam@381 750
adam@381 751 Notation "^" := Var.
adam@381 752 Notation "#" := Const.
adam@381 753 Infix "@" := App (left associativity, at level 50).
adam@381 754 Infix "@+" := Plus (left associativity, at level 50).
adam@381 755 Notation "\ x : t , e" := (Abs (dom := t) (fun x => e))
adam@381 756 (no associativity, at level 51, x at level 0).
adam@381 757 Notation "[ e ]" := (fun _ => e).
adam@381 758
adam@381 759 Example Add : Term (Nat --> Nat --> Nat) :=
adam@381 760 [\x : Nat, \y : Nat, ^x @+ ^y].
adam@381 761
adam@381 762 Example Three_the_hard_way : Term Nat :=
adam@381 763 [Add _ @ #1 @ #2].
adam@381 764
adam@381 765 Eval compute in TermDenote Three_the_hard_way.
adam@381 766 (** %\vspace{-.15in}%[[
adam@381 767 = 3
adam@381 768 ]]
adam@381 769 *)
adam@381 770
adam@381 771 End HigherOrder.
adam@381 772
adam@381 773 (** 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. *)