Mercurial > cpdt > repo
comparison src/OpSem.v @ 263:af6f6d8dcfe7
Prose for OpSem
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 28 Dec 2009 14:31:40 -0500 |
parents | de53c8bcfa8d |
children | dce88a5c170c |
comparison
equal
deleted
inserted
replaced
262:de53c8bcfa8d | 263:af6f6d8dcfe7 |
---|---|
16 (* end hide *) | 16 (* end hide *) |
17 | 17 |
18 | 18 |
19 (** %\chapter{Higher-Order Operational Semantics}% *) | 19 (** %\chapter{Higher-Order Operational Semantics}% *) |
20 | 20 |
21 (** The last few chapters have shown how PHOAS can make it relatively painless to reason about program transformations. Each of our example languages so far has had a semantics that is easy to implement with an interpreter in Gallina. Since Gallina is designed to rule out non-termination, we cannot hope to give interpreter-based semantics to Turing-complete programming languages. Falling back on standard operational semantics leaves us with the old bureaucratic concerns about capture-avoiding substitution. Can we encode Turing-complete, higher-order languages in Coq without sacrificing the advantages of higher-order encoding? | |
22 | |
23 Any approach that applies to basic untyped lambda calculus is likely to extend to most object languages of interest. We can attempt the "obvious" way of equipping a PHOAS definition for use in an operational semantics, without mentioning substitution explicitly. Specifically, we try to work with expressions with [var] instantiated with a type of values. *) | |
24 | |
25 Section exp. | |
26 Variable var : Type. | |
27 | |
28 Inductive exp : Type := | |
29 | Var : var -> exp | |
30 | App : exp -> exp -> exp | |
31 | Abs : (var -> exp) -> exp. | |
32 End exp. | |
33 | |
34 (** [[ | |
35 Inductive val : Type := | |
36 | VAbs : (val -> exp val) -> val. | |
37 | |
38 Error: Non strictly positive occurrence of "val" in | |
39 "(val -> exp val) -> val". | |
40 | |
41 ]] | |
42 | |
43 We would like to represent values (which are all function abstractions) as functions from variables to expressions, where we represent variables as the same value type that we are defining. That way, a value can be substituted in a function body simply by applying the body to the value. Unfortunately, the positivity restriction rejects this definition, for much the same reason that we could not use the classical HOAS encoding. | |
44 | |
45 We can try an alternate approach based on defining [val] like a usual class of syntax. *) | |
46 | |
47 Section val. | |
48 Variable var : Type. | |
49 | |
50 Inductive val : Type := | |
51 | VAbs : (var -> exp var) -> val. | |
52 End val. | |
53 | |
54 (** Now the puzzle is how to write the type of an expression whose variables are represented as values. We would like to be able to write a recursive definition like this one: | |
55 | |
56 [[ | |
57 Fixpoint expV := exp (val expV). | |
58 | |
59 ]] | |
60 | |
61 Of course, this kind of definition is not structurally recursive, so Coq will not allow it. Getting "substitution for free" seems to require some similar kind of self-reference. | |
62 | |
63 In this chapter, we will consider an alternate take on the problem. We add a level of indirection, introducing more explicit syntax to break the cycle in type definitions. Specifically, we represent function values as numbers that index into a %\emph{%#<i>#closure heap#</i>#%}% that our operational semantics maintains alongside the expression being evaluated. *) | |
64 | |
65 | |
21 (** * Closure Heaps *) | 66 (** * Closure Heaps *) |
67 | |
68 (** The essence of the technique is to store function bodies in lists that are extended monotonically as function abstractions are evaluated. We can define a set of functions and theorems that implement the core functionality generically. *) | |
22 | 69 |
23 Section lookup. | 70 Section lookup. |
24 Variable A : Type. | 71 Variable A : Type. |
72 | |
73 (** We start with a [lookup] function that generalizes last chapter's function of the same name. It selects the element at a particular position in a list, where we number the elements starting from the end of the list, so that prepending new elements does not change the indices of old elements. *) | |
25 | 74 |
26 Fixpoint lookup (ls : list A) (n : nat) : option A := | 75 Fixpoint lookup (ls : list A) (n : nat) : option A := |
27 match ls with | 76 match ls with |
28 | nil => None | 77 | nil => None |
29 | v :: ls' => if eq_nat_dec n (length ls') then Some v else lookup ls' n | 78 | v :: ls' => if eq_nat_dec n (length ls') then Some v else lookup ls' n |
30 end. | 79 end. |
31 | 80 |
81 Infix "##" := lookup (left associativity, at level 1). | |
82 | |
83 (** The second of our two definitions expresses when one list extends another. We will write [ls1 ~> ls2] to indicate that [ls1] could evolve into [ls2]; that is, [ls1] is a suffix of [ls2]. *) | |
84 | |
32 Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1. | 85 Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1. |
33 | |
34 Infix "##" := lookup (left associativity, at level 1). | |
35 Infix "~>" := extends (no associativity, at level 80). | 86 Infix "~>" := extends (no associativity, at level 80). |
87 | |
88 (** We prove and add as hints a few basic theorems about [lookup] and [extends]. *) | |
36 | 89 |
37 Theorem lookup1 : forall x ls, | 90 Theorem lookup1 : forall x ls, |
38 (x :: ls) ## (length ls) = Some x. | 91 (x :: ls) ## (length ls) = Some x. |
39 crush; match goal with | 92 crush; match goal with |
40 | [ |- context[if ?E then _ else _] ] => destruct E | 93 | [ |- context[if ?E then _ else _] ] => destruct E |
82 Infix "##" := lookup (left associativity, at level 1). | 135 Infix "##" := lookup (left associativity, at level 1). |
83 Infix "~>" := extends (no associativity, at level 80). | 136 Infix "~>" := extends (no associativity, at level 80). |
84 | 137 |
85 Hint Resolve lookup1 extends_refl extends1 extends_trans extends_lookup. | 138 Hint Resolve lookup1 extends_refl extends1 extends_trans extends_lookup. |
86 | 139 |
140 (** We are dealing explicitly with the nitty-gritty of closure heaps. Why is this better than dealing with the nitty-gritty of variables? The inconvenience of modeling lambda calculus-style binders comes from the presence of nested scopes. Program evaluation will only involve one %\emph{%#<i>#global#</i>#%}% closure heap. Also, the short development that we just finished can be reused for many different object languages. None of these definitions or theorems needs to be redone to handle specific object language features. By adding the theorems as hints, no per-object-language effort is required to apply the critical facts as needed. *) | |
141 | |
87 | 142 |
88 (** * Languages and Translation *) | 143 (** * Languages and Translation *) |
89 | 144 |
145 (** For the rest of this chapter, we will consider the example of CPS translation for untyped lambda calculus with boolean constants. It is convenient to include these constants, because their presence makes it easy to state a final translation correctness theorem. *) | |
146 | |
90 Module Source. | 147 Module Source. |
148 (** We define the syntax of source expressions in our usual way. *) | |
149 | |
91 Section exp. | 150 Section exp. |
92 Variable var : Type. | 151 Variable var : Type. |
93 | 152 |
94 Inductive exp : Type := | 153 Inductive exp : Type := |
95 | Var : var -> exp | 154 | Var : var -> exp |
100 | 159 |
101 Implicit Arguments Bool [var]. | 160 Implicit Arguments Bool [var]. |
102 | 161 |
103 Definition Exp := forall var, exp var. | 162 Definition Exp := forall var, exp var. |
104 | 163 |
164 (** We will implement a big-step operational semantics, where expressions are mapped to values. A value is either a function or a boolean. We represent a function as a number that will be interpreted as an index into the global closure heap. *) | |
165 | |
105 Inductive val : Set := | 166 Inductive val : Set := |
106 | VFun : nat -> val | 167 | VFun : nat -> val |
107 | VBool : bool -> val. | 168 | VBool : bool -> val. |
108 | 169 |
170 (** A closure, then, follows the usual representation of function abstraction bodies, where we represent variables as values. *) | |
171 | |
109 Definition closure := val -> exp val. | 172 Definition closure := val -> exp val. |
110 Definition closures := list closure. | 173 Definition closures := list closure. |
174 | |
175 (** Our evaluation relation has four places. We map an initial closure heap and an expression into a final closure heap and a value. The interesting cases are for [Abs], where we push the body onto the closure heap; and for [App], where we perform a lookup in a closure heap, to find the proper function body to execute next. *) | |
111 | 176 |
112 Inductive eval : closures -> exp val -> closures -> val -> Prop := | 177 Inductive eval : closures -> exp val -> closures -> val -> Prop := |
113 | EvVar : forall cs v, | 178 | EvVar : forall cs v, |
114 eval cs (Var v) cs v | 179 eval cs (Var v) cs v |
115 | 180 |
124 eval cs (Abs c) (c :: cs) (VFun (length cs)) | 189 eval cs (Abs c) (c :: cs) (VFun (length cs)) |
125 | 190 |
126 | EvBool : forall cs b, | 191 | EvBool : forall cs b, |
127 eval cs (Bool b) cs (VBool b). | 192 eval cs (Bool b) cs (VBool b). |
128 | 193 |
129 Definition Eval (cs1 : closures) (E : Exp) (cs2 : closures) (v : val) := eval cs1 (E _) cs2 v. | 194 (** A simple wrapper produces an evaluation relation suitable for use on the main expression type [Exp]. *) |
195 | |
196 Definition Eval (cs1 : closures) (E : Exp) (cs2 : closures) (v : val) := | |
197 eval cs1 (E _) cs2 v. | |
198 | |
199 (** To prove our translation's correctness, we will need the usual notions of expression equivalence and well-formedness. *) | |
130 | 200 |
131 Section exp_equiv. | 201 Section exp_equiv. |
132 Variables var1 var2 : Type. | 202 Variables var1 var2 : Type. |
133 | 203 |
134 Inductive exp_equiv : list (var1 * var2) -> exp var1 -> exp var2 -> Prop := | 204 Inductive exp_equiv : list (var1 * var2) -> exp var1 -> exp var2 -> Prop := |
149 End exp_equiv. | 219 End exp_equiv. |
150 | 220 |
151 Definition Wf (E : Exp) := forall var1 var2, exp_equiv nil (E var1) (E var2). | 221 Definition Wf (E : Exp) := forall var1 var2, exp_equiv nil (E var1) (E var2). |
152 End Source. | 222 End Source. |
153 | 223 |
224 (** Our target language can be defined without introducing any additional tricks. *) | |
225 | |
154 Module CPS. | 226 Module CPS. |
155 Section exp. | 227 Section exp. |
156 Variable var : Type. | 228 Variable var : Type. |
157 | 229 |
158 Inductive prog : Type := | 230 Inductive prog : Type := |
215 | 287 |
216 Definition Eval (cs : closures) (P : Prog) (v : val) := eval cs (P _) v. | 288 Definition Eval (cs : closures) (P : Prog) (v : val) := eval cs (P _) v. |
217 End CPS. | 289 End CPS. |
218 | 290 |
219 Import Source CPS. | 291 Import Source CPS. |
292 | |
293 (** Finally, we define a CPS translation in the same way as in our previous example for simply-typed lambda calculus. *) | |
220 | 294 |
221 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level). | 295 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level). |
222 | 296 |
223 Section cpsExp. | 297 Section cpsExp. |
224 Variable var : Type. | 298 Variable var : Type. |
257 Definition CpsExp (E : Exp) : Prog := fun _ => cpsExp (E _) (Halt (var := _)). | 331 Definition CpsExp (E : Exp) : Prog := fun _ => cpsExp (E _) (Halt (var := _)). |
258 | 332 |
259 | 333 |
260 (** * Correctness Proof *) | 334 (** * Correctness Proof *) |
261 | 335 |
336 (** Our proof for simply-typed lambda calculus relied on a logical relation to state the key induction hypothesis. Since logical relations proceed by recursion on type structure, we cannot apply them directly in an untyped setting. Instead, we will use an inductive judgment to relate source-level and CPS-level values. First, it is helpful to define an abbreviation for the compiled version of a function body. *) | |
337 | |
262 Definition cpsFunc var (e' : var -> Source.exp var) := | 338 Definition cpsFunc var (e' : var -> Source.exp var) := |
263 fun p : var => | 339 fun p : var => |
264 x <- Fst p; | 340 x <- Fst p; |
265 kf <- Snd p; | 341 kf <- Snd p; |
266 r <-- e' x; | 342 r <-- e' x; |
267 CPS.App kf r. | 343 CPS.App kf r. |
268 | 344 |
345 (** Now we can define our correctness relation [cr], which is parameterized by source-level and CPS-level closure heaps. *) | |
346 | |
269 Section cr. | 347 Section cr. |
270 Variable s1 : Source.closures. | 348 Variable s1 : Source.closures. |
271 Variable s2 : CPS.closures. | 349 Variable s2 : CPS.closures. |
272 | 350 |
273 Import Source. | 351 Import Source. |
274 | 352 |
353 (** Only equal booleans are related. For two function addresses [l1] and [l2] to be related, they must point to valid functions in their respective closure heaps. The address [l1] must point to a function [f1], and [l2] must point to the result of compiling function [f2]. Further, [f1] and [f2] must be equivalent syntactically in some variable environment [G], and every variable pair in [G] must itself belong to the relation we are defining. *) | |
354 | |
275 Inductive cr : Source.val -> CPS.val -> Prop := | 355 Inductive cr : Source.val -> CPS.val -> Prop := |
356 | CrBool : forall b, | |
357 cr (Source.VBool b) (CPS.VBool b) | |
358 | |
276 | CrFun : forall l1 l2 G f1 f2, | 359 | CrFun : forall l1 l2 G f1 f2, |
277 (forall x1 x2, exp_equiv ((x1, x2) :: G) (f1 x1) (f2 x2)) | 360 (forall x1 x2, exp_equiv ((x1, x2) :: G) (f1 x1) (f2 x2)) |
278 -> (forall x1 x2, In (x1, x2) G -> cr x1 x2) | 361 -> (forall x1 x2, In (x1, x2) G -> cr x1 x2) |
279 -> s1 ## l1 = Some f1 | 362 -> s1 ## l1 = Some f1 |
280 -> s2 ## l2 = Some (cpsFunc f2) | 363 -> s2 ## l2 = Some (cpsFunc f2) |
281 -> cr (Source.VFun l1) (CPS.VFun l2) | 364 -> cr (Source.VFun l1) (CPS.VFun l2). |
282 | |
283 | CrBool : forall b, | |
284 cr (Source.VBool b) (CPS.VBool b). | |
285 End cr. | 365 End cr. |
286 | 366 |
287 Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70). | 367 Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70). |
288 | 368 |
289 Hint Constructors cr. | 369 Hint Constructors cr. |
370 | |
371 (** To prove our main lemma, it will be useful to know that source-level evaluation never removes old closures from a closure heap. *) | |
290 | 372 |
291 Lemma eval_monotone : forall cs1 e cs2 v, | 373 Lemma eval_monotone : forall cs1 e cs2 v, |
292 Source.eval cs1 e cs2 v | 374 Source.eval cs1 e cs2 v |
293 -> cs1 ~> cs2. | 375 -> cs1 ~> cs2. |
294 induction 1; crush; eauto. | 376 induction 1; crush; eauto. |
295 Qed. | 377 Qed. |
378 | |
379 (** Further, [cr] continues to hold when its closure heap arguments are evolved in legal ways. *) | |
296 | 380 |
297 Lemma cr_monotone : forall cs1 cs2 cs1' cs2', | 381 Lemma cr_monotone : forall cs1 cs2 cs1' cs2', |
298 cs1 ~> cs1' | 382 cs1 ~> cs1' |
299 -> cs2 ~> cs2' | 383 -> cs2 ~> cs2' |
300 -> forall v1 v2, cs1 & cs2 |-- v1 ~~ v2 | 384 -> forall v1 v2, cs1 & cs2 |-- v1 ~~ v2 |
302 induction 3; crush; eauto. | 386 induction 3; crush; eauto. |
303 Qed. | 387 Qed. |
304 | 388 |
305 Hint Resolve eval_monotone cr_monotone. | 389 Hint Resolve eval_monotone cr_monotone. |
306 | 390 |
391 (** We state a trivial fact about the validity of variable environments, so that we may add this fact as a hint that [eauto] will apply. *) | |
392 | |
307 Lemma push : forall G s1 s2 v1' v2', | 393 Lemma push : forall G s1 s2 v1' v2', |
308 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2) | 394 (forall v1 v2, In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2) |
309 -> s1 & s2 |-- v1' ~~ v2' | 395 -> s1 & s2 |-- v1' ~~ v2' |
310 -> (forall v1 v2, (v1', v2') = (v1, v2) \/ In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2). | 396 -> (forall v1 v2, (v1', v2') = (v1, v2) \/ In (v1, v2) G -> s1 & s2 |-- v1 ~~ v2). |
311 crush. | 397 crush. |
312 Qed. | 398 Qed. |
313 | 399 |
314 Hint Resolve push. | 400 Hint Resolve push. |
401 | |
402 (** Our final preparation for the main lemma involves adding effective hints about the CPS language's operational semantics. The following tactic performs one step of evaluation. It uses the Ltac code [eval hnf in e] to compute the %\emph{%#<i>#head normal form#</i>#%}% of [e], where the head normal form of an expression in an inductive type is an application of one of that inductive type's constructors. The final line below uses [solve] to ensure that we only take a [Bind] step if a full evaluation derivation for the associated primop may be found before proceeding. *) | |
315 | 403 |
316 Ltac evalOne := | 404 Ltac evalOne := |
317 match goal with | 405 match goal with |
318 | [ |- CPS.eval ?cs ?e ?v ] => | 406 | [ |- CPS.eval ?cs ?e ?v ] => |
319 let e := eval hnf in e in | 407 let e := eval hnf in e in |
320 change (CPS.eval cs e v); | 408 change (CPS.eval cs e v); |
321 econstructor; [ solve [ eauto ] | ] | 409 econstructor; [ solve [ eauto ] | ] |
322 end. | 410 end. |
323 | 411 |
412 (** For primops, we rely on [eauto]'s usual approach. For goals that evaluate programs, we instead ask to treat one or more applications of [evalOne] as a single step, which helps us avoid passing [eauto] an excessively large bound on proof tree depth. *) | |
413 | |
324 Hint Constructors evalP. | 414 Hint Constructors evalP. |
325 Hint Extern 1 (CPS.eval _ _ _) => evalOne; repeat evalOne. | 415 Hint Extern 1 (CPS.eval _ _ _) => evalOne; repeat evalOne. |
416 | |
417 (** The final lemma proceeds by induction on an evaluation derivation for an expression [e1] that is equivalent to some [e2] in some environment [G]. An initial closure heap for each language is quantified over, such that all variable pairs in [G] are compatible. The lemma's conclusion applies to an arbitrary continuation [k], asserting that a final CPS-level closure heap [s2] and a CPS-level program result value [r2] exist. | |
418 | |
419 Three conditions establish that [s2] and [r2] are chosen properly: Evaluation of [e2]'s compilation with continuation [k] must be equivalent to evaluation of [k r2]. The original program result [r1] must be compatible with [r2] in the final closure heaps. Finally, [s2'] must be a proper evolution of the original CPS-level heap [s2]. *) | |
326 | 420 |
327 Lemma cpsExp_correct : forall s1 e1 s1' r1, | 421 Lemma cpsExp_correct : forall s1 e1 s1' r1, |
328 Source.eval s1 e1 s1' r1 | 422 Source.eval s1 e1 s1' r1 |
329 -> forall G (e2 : exp CPS.val), | 423 -> forall G (e2 : exp CPS.val), |
330 exp_equiv G e1 e2 | 424 exp_equiv G e1 e2 |
333 -> forall k, exists s2', exists r2, | 427 -> forall k, exists s2', exists r2, |
334 (forall r, CPS.eval s2' (k r2) r | 428 (forall r, CPS.eval s2' (k r2) r |
335 -> CPS.eval s2 (cpsExp e2 k) r) | 429 -> CPS.eval s2 (cpsExp e2 k) r) |
336 /\ s1' & s2' |-- r1 ~~ r2 | 430 /\ s1' & s2' |-- r1 ~~ r2 |
337 /\ s2 ~> s2'. | 431 /\ s2 ~> s2'. |
432 | |
433 (** The proof script follows our standard approach. Its main loop applies three hints. First, we perform inversion on any derivation of equivalence between a source-level function value and some other value. Second, we eliminate redundant equality hypotheses. Finally, we look for opportunities to instantiate inductive hypotheses. | |
434 | |
435 We identify an IH by its syntactic form, noting the expression [E] that it applies to. It is important to instantiate IHes in the right order, since existentially-quantified variables in the conclusion of one IH may need to be used in instantiating the universal quantifiers of a different IH. Thus, we perform a quick check to [fail 1] if the IH we found applies to an expression that was evaluated after another expression [E'] whose IH we did not yet instantiate. The flow of closure heaps through source-level evaluation is used to implement the check. | |
436 | |
437 If the hypothesis [H] is indeed the right IH to handle next, we use the [guess] tactic to guess values for its universal quantifiers and prove its hypotheses with [eauto]. This tactic is very similar to [inster] from Chapter 12. It takes two arguments: the first is a value to use for any properly-typed universal quantifier, and the second is the hypothesis to instantiate. The final inner [match] deduces if we are at the point of executing the body of a called function. If so, we help [guess] by saying that the initial closure heap will be the current closure heap [cs] extended with the current continuation [k]. In all other cases, [guess] is smart enough to operate alone. *) | |
438 | |
338 induction 1; inversion 1; crush; | 439 induction 1; inversion 1; crush; |
339 repeat (match goal with | 440 repeat (match goal with |
340 | [ H : _ & _ |-- Source.VFun _ ~~ _ |- _ ] => inversion H; clear H | 441 | [ H : _ & _ |-- Source.VFun _ ~~ _ |- _ ] => inversion H; clear H |
341 | [ H1 : ?E = _, H2 : ?E = _ |- _ ] => rewrite H1 in H2; clear H1 | 442 | [ H1 : ?E = _, H2 : ?E = _ |- _ ] => rewrite H1 in H2; clear H1 |
342 | [ H : forall G e2, exp_equiv G ?E e2 -> _ |- _ ] => | 443 | [ H : forall G e2, exp_equiv G ?E e2 -> _ |- _ ] => |
343 match goal with | 444 match goal with |
344 | [ _ : Source.eval ?CS E _ _, _ : Source.eval _ ?E' ?CS _, | 445 | [ _ : Source.eval ?CS E _ _, _ : Source.eval _ ?E' ?CS _, |
345 _ : forall G e2, exp_equiv G ?E' e2 -> _ |- _ ] => fail 1 | 446 _ : forall G e2, exp_equiv G ?E' e2 -> _ |- _ ] => fail 1 |
346 | _ => match goal with | 447 | _ => match goal with |
347 | [ k : val -> prog val, _ : _ & ?cs |-- _ ~~ _, _ : context[VFun] |- _ ] => | 448 | [ k : val -> prog val, _ : _ & ?cs |-- _ ~~ _, |
449 _ : context[VFun] |- _ ] => | |
348 guess (k :: cs) H | 450 guess (k :: cs) H |
349 | _ => guess tt H | 451 | _ => guess tt H |
350 end | 452 end |
351 end | 453 end |
352 end; crush); eauto 13. | 454 end; crush); eauto 13. |
353 Qed. | 455 Qed. |
354 | 456 |
355 Lemma CpsExp_correct : forall E cs b, | 457 (** The final theorem follows easily from this lemma. *) |
458 | |
459 Theorem CpsExp_correct : forall E cs b, | |
356 Source.Eval nil E cs (Source.VBool b) | 460 Source.Eval nil E cs (Source.VBool b) |
357 -> Wf E | 461 -> Wf E |
358 -> CPS.Eval nil (CpsExp E) (CPS.VBool b). | 462 -> CPS.Eval nil (CpsExp E) (CPS.VBool b). |
359 Hint Constructors CPS.eval. | 463 Hint Constructors CPS.eval. |
360 | 464 |