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?

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.

Inductive val : Type :=
| VAbs : (val -> exp val) -> val.

Error: Non strictly positive occurrence of "val" in
 "(val -> exp val) -> val".
 



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.

We can try an alternate approach based on defining val like a usual class of syntax.

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:


Fixpoint expV := exp (val expV).




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.

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 closure heap that our operational semantics maintains alongside the expression being evaluated.

Closure Heaps

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.

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.

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.

We prove and add as hints a few basic theorems about lookup and extends.

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 global 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.

Languages and Translation

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.

We define the syntax of source expressions in our usual way.

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.

A closure, then, follows the usual representation of function abstraction bodies, where we represent variables as values.

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.

A simple wrapper produces an evaluation relation suitable for use on the main expression type Exp.

To prove our translation's correctness, we will need the usual notions of expression equivalence and well-formedness.

Our target language can be defined without introducing any additional tricks.

Finally, we define a CPS translation in the same way as in our previous example for simply-typed lambda calculus.

Correctness Proof

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.

Now we can define our correctness relation cr, which is parameterized by source-level and CPS-level closure heaps.

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.

To prove our main lemma, it will be useful to know that source-level evaluation never removes old closures from a closure heap.

Further, cr continues to hold when its closure heap arguments are evolved in legal ways.

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.

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 head normal form 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.

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.

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.

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.

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.

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.

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.

The final theorem follows easily from this lemma.