Mercurial > cpdt > repo

comparison src/OpSem.v @ 292:2c88fc1dbe33

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of double-quotes and LaTeX operator beautification
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 16:31:04 -0500
parents dce88a5c170c
children d5787b70cf48
comparison
equal deleted inserted replaced
291:da9ccc6bf572 292:2c88fc1dbe33
1 (* Copyright (c) 2009, Adam Chlipala 1 (* Copyright (c) 2009-2010, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
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? 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 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. *) 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 24
25 Section exp. 25 Section exp.
26 Variable var : Type. 26 Variable var : Type.
27 27
28 Inductive exp : Type := 28 Inductive exp : Type :=
56 [[ 56 [[
57 Fixpoint expV := exp (val expV). 57 Fixpoint expV := exp (val expV).
58 58
59 ]] 59 ]]
60 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. 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 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. *) 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 64
65 65
66 (** * Closure Heaps *) 66 (** * Closure Heaps *)
81 Infix "##" := lookup (left associativity, at level 1). 81 Infix "##" := lookup (left associativity, at level 1).
82 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]. *) 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 84
85 Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1. 85 Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1.
86 (** printing ~> $\leadsto$ *)
86 Infix "~>" := extends (no associativity, at level 80). 87 Infix "~>" := extends (no associativity, at level 80).
87 88
88 (** We prove and add as hints a few basic theorems about [lookup] and [extends]. *) 89 (** We prove and add as hints a few basic theorems about [lookup] and [extends]. *)
89 90
90 Theorem lookup1 : forall x ls, 91 Theorem lookup1 : forall x ls,
290 291
291 Import Source CPS. 292 Import Source CPS.
292 293
293 (** Finally, we define a CPS translation in the same way as in our previous example for simply-typed lambda calculus. *) 294 (** Finally, we define a CPS translation in the same way as in our previous example for simply-typed lambda calculus. *)
294 295
296 (** printing <-- $\longleftarrow$ *)
295 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level). 297 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
296 298
297 Section cpsExp. 299 Section cpsExp.
298 Variable var : Type. 300 Variable var : Type.
299 301
362 -> s1 ## l1 = Some f1 364 -> s1 ## l1 = Some f1
363 -> s2 ## l2 = Some (cpsFunc f2) 365 -> s2 ## l2 = Some (cpsFunc f2)
364 -> cr (Source.VFun l1) (CPS.VFun l2). 366 -> cr (Source.VFun l1) (CPS.VFun l2).
365 End cr. 367 End cr.
366 368
369 (** printing |-- $\vdash$ *)
370 (** printing ~~ $\sim$ *)
367 Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70). 371 Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70).
368 372
369 Hint Constructors cr. 373 Hint Constructors cr.
370 374
371 (** To prove our main lemma, it will be useful to know that source-level evaluation never removes old closures from a closure heap. *) 375 (** To prove our main lemma, it will be useful to know that source-level evaluation never removes old closures from a closure heap. *)