Mercurial > cpdt > repo
comparison src/OpSem.v @ 292:2c88fc1dbe33
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. *) |