Incremental Lambda Lifting: An Exercise in Almost-Denotational Semantics

(ICFP’97 Paper Code: 7553.203)

Gregory T. Sullivan^{∗} Mitchell Wand^{∗} College of Computer Science Northeastern University 360 Huntington Avenue, 161CN Boston, MA 02115, USA voice: (617) 373-2462, fax: (617) 373-5121

                          {gregs,wand}@ccs.neu.edu
                  http://www.ccs.neu.edu/home/{gregs,wand}

November 17, 1996

Abstract

We prove the correctness of incremental lambda-lifting, an optimization that attempts to reduce the closure allocation overhead of higher-order programs by changing the scope of nested procedures. This optimization is invalid in the standard denotational semantics of Scheme, because it changes the storage behavior of the program. Our method consists of giving Scheme a denotational semantics in an operationally-based term model in which interaction is the basic observable. Lambda lifting is then shown to preserve meaning in the model.

1 Introduction

Compilers for higher-order languages typically perform elaborate program transformations in order to improve performance. Such transformations often change the storage behavior of the program. In [WS97], we introduced a method for proving the correctness of such transformations. The method consists of giving the programs a denotational semantics in an operationally-based term model in which interaction is the basic observable, and showing that the transformation is meaningpreserving. This allows us to consider correctness for programs that interact with their environment without terminating, and also for transformations that change the internal store behavior of the program. In [WS97], we illustrated the method by giving the first proof of the correctness of assignment elimination [KKR^{+}86]. In this paper, we use the method to prove the correctness of incremental lambda lifting as performed by the Twobit Scheme compiler [CH94].

∗Work supported by the National Science Foundation under grants number CCR-9304144 and CCR-9404646.

Consider the Scheme lambda-expression

(lambda (x) \begin{matrix}(letrec \\ ((f_{1} (lambda (y_{1}) e_{1})) \\ (f_{2} (lambda (y_{2}) e_{2}))) \\ e)) \end{matrix}

This abstraction is represented by a closure consisting of the abstraction’s constituent Scheme expressions and any bindings of the abstraction’s free variables. Because Scheme is a higher-order language, the closure can be passed as an argument, bound to variables, and stored in the heap. Each time the closure is used – applied to a value for the argument x – closures for the nested procedures f_{1} and f_{2} must also be created. The environment components of the closures for f_{1} and f_{2} may reference the outer closure’s parameter x, which is in the scope of the nested procedures’ bodies.

The incremental lambda lifting transformation attempts to reduce the closure allocation overhead by hoisting the nested procedures out of the lambda(x) abstraction – rewriting the above abstraction to:

(letrec

((f_{1} (lambda (x y_{1}) e′_{1}))
(f_{2} (lambda (x y_{2}) e′_{2})))

(lambda (x) e′))

The process of moving the nested procedures out of their original scope has a number of consequences. If f_{1} and f_{2} reference the x parameter of the original outer abstraction, then x must be added as to the argument lists of f_{1} and f_{2}. Also, once x has been added to the argument lists of f_{1} and f_{2}, all call sites for those procedures within e, e_{1}, and e_{2} must be modified to pass the value for x. After lambda-lifting, the closures for f_{1} and f_{2} are allocated before the closure for lambda (x) is created. Thus, even if the closure for lambda (x) is copied and used many times, the overhead of creating closures for f_{1} and f_{2} is incurred only once.

Proving the correctness of the incremental lambda lifting transformation is challenging in many respects:

1. The transformation itself is complex, involving changes to the scope, signature and bodies of possibly many related procedures.

2. The conditions under which the transformation is allowed are subtle. For example, we cannot lift procedures which may escape the scope we are considering (e.g. if f_{1} were returned from e in the above example). Also, we do not want to add extra parameters to the lifted procedures, but we must add all referenced variables and all variables which must be passed to other lifted procedures.

3. The lambda lifting transformation is invalid in the standard denotational semantics of Scheme [CR91], as it can significantly change the storage behavior of programs.

The approach we take is to give Scheme a denotational semantics in an event-based model. An event-based model is a term model embedded in a process calculus. Observable behavior is taken from the process calculus; equality of terms in the model is taken to be contextual equivalence as measured by this observable behavior. Equivalence in our semantics does not necessarily imply equivalence in the official denotational semantics of Scheme. In particular, we intend to allow equivalences where the standard semantics would distinguish terms because of differences in nonobservable store behavior. Terms which are equivalent in the standard denotational semantics for Scheme, however, must be equivalent under the semantics we use as well.

Following a review of related work in Section 2, we introduce in Section 3 the incremental lambda lifting transformation. We use a dialect of Scheme called Scheme_{cell} as the source language for the transformation. Whereas Scheme variables always denote locations, the Scheme_{cell} dialect distinguishes value-bound variables from cell-bound (i.e. heap-allocated) variables. Using Scheme_{cell} as the source language lets us ignore any complications from side effects (set!) to local variables which could otherwise invalidate the lambda lifting transformation. A meaning-preserving translation from Scheme to Scheme_{cell} (assignment elimination) was presented and shown correct in [WS97].

Sections 4 and 5 present the semantic framework we will use. In Section 4, we present the syntax and operational semantics of our metalanguage. This metalanguage is an extended PCF with recursive types, a store, and a CPS I/O system. Reduction in the side-effect-free subset of the language is a relation between metalanguage terms. Store and I/O operations, however, take place in term-store pairs we call states. The semantics of Scheme_{cell} is specified by a syntax-directed translation into this metalanguage. In Section 5, we define two metalanguage terms to be contextually equivalent (denoted ≅_{∀C}) if they have the same I/O behavior when inserted into every possible program context. By identifying input/output as the observable actions of the system, we avoid considering the store as part of the “final answer” of a computation. Indeed, we avoid the notion of a “final answer” at all, so that we can study equivalence of terms that have infinite behavior. Contextual equivalence is the natural notion of equivalence given an operational semantics; however, contextual equivalence is unwieldy and difficult to prove directly. We define two metalanguage terms to be extensionally equivalent (denoted ≅_{ext}) if they have the have the same I/O behavior in a limited set of contexts we call extensional contexts. For example, terms of function type are extensionally equivalent if they produce equivalent results when applied to the same argument. Our extensional contexts are similar to Gordon’s experiments [Gor95]. From [WS97], we have a context lemma which proves that our metalanguage is extensional – that is, two metalanguage terms are contextually equivalent iff they are extensionally equivalent.

In Section 6, we give define the semantics of Scheme_{cell} expressions via a syntax-directed CPS translation [[−]]_{cell} into the metalanguage.

Given the incremental lambda-lifting transformation LL on Scheme_{cell} expressions, and the translation [[−]]_{cell} from Scheme_{cell} expressions into the metalanguage, Section 7 sketches the proof of correctness for incremental lambda lifting. The proof obligation is to show that for all Scheme_{cell} expressions e,

[[e]]_{cell} ≅_{∀C} [[LL(e)]]_{cell}

We first invoke the context lemma so that we need only consider extensional contexts. We then construct a relation between metalanguage states which includes the translations of Scheme_{cell} expressions before and after lambda lifting. The construction of this relation is the technically most difficult part of the proof. We then use a coinductive argument to show that the relation we have constructed is a bisimulation up to bisimulation [Mil90], which is easily shown to satisfy the requirements of extensional equivalence. A more detailed presentation of the proof of correctness can be found in [Sul96].

We conclude, in Section 8, with consideration of open problems and future work.

2 Related Work

Operationally-based term models were introduced in [TW96]. Here we extend [TW96] by adding types and a heap, and by considering applications to program transformations. The formulation of input-output both here and in [TW96] is based on Gordon’s CPS input-output system [Gor94].

Observational or contextual equivalence for programming languages was introduced by [Plo77], adapting the work of Morris [Mor68] for the λ-calculus. Plotkin’s formulation, like almost all other work for sequential languages, dealt with conversion to a constant. Context lemmas for proving contextual equivalence were introduced by Milner [Mil77] in a typed functional language. Gordon [Gor95] extended the result to include recursive types with potentially infinite behavior.

The work most closely related to ours is that of Mason and Talcott [MT91] and Felleisen [Fel87]. They considered contextual equivalence for a number of untyped call-by-value languages using operational techniques, and proved context lemmas for these languages. Our approach differs from theirs in that we propose a single metalanguage into which a variety of source languages can be translated; neither Mason and Talcott nor Felleisen consider issues of translation. Our Context Lemma (Theorem 2) also extends their results by considering input-output effects rather than final answers and by validating full β-conversion rather than their β-value.

Bisimulation was introduced by [Par81]. Abramsky [Abr90] used bisimulation to define a λ-model, but his observables were very different from ours. The concept of a relation preserved under computation is probably much older. It was used for program equivalence in [MT91, WO92, ORW95]; [Sta94] uses a similar notion extended to become a logical relation.

Incremental lambda-lifting in the Twobit Scheme compiler is presented in [CH94]. An overview of lambda lifting in a purely functional setting is given in [PJ87]. Lambda lifting differs from closure conversion, such as in [WS94, MMH96]; whereas closure conversion attempts to optimize the representation of closures, lambda lifting attempts change the closure allocation behavior of a program or even to remove the need for some closures entirely. Incremental lambda lifting is also distinct from the super-combinators of [Hug82] in that procedures are not necessarily lifted to the top level. The process of incremental lambda lifting can be performed repeatedly in order to bring a deeply-nested procedure to the top level, as would be done with traditional lambda lifting. However, being able to lift only one level at a time gives the compiler added flexibility.

3 Incremental Lambda Lifting

Incremental lambda lifting transforms terms in the Scheme_{cell} dialect of Scheme. The syntax of Scheme_{cell} is given in Figure 1; note that there is no set! operator. All mutable variables are stored in heap-allocated cells, and operations on cells are explicit in the Scheme_{cell} language. Side-effects to variables added to the parameter lists of lifted procedures would confound the lambda-lifting transformation in Scheme. This is because the side-effects to the once-free-now-bound variables would, as specified in the Scheme semantics, be modifying a different cell in the lambda-lifted body than in the original. The correctness of a translation from Scheme to Scheme_{cell} was shown in [WS97].

Scheme_{cell} has a simple type-checking system to verify that value-bound and cell-bound variables are used consistently. We omit the rules, but judgements of the form Γ ⊢_{cell} e:ok are read as “With type assignment Γ mapping the free variables of Scheme_{cell} term e to {Val, ref (Val)}, e is well-typed.”

e ::= x | n | (lambda (x …) e) | (e e …)
| (let ((x rhs) …) e)
| (letrec ((x e) …) e)
| (cell-ref x) | (cell-set! x e)
rhs ::= x | (make-cell e)

Figure 1: Syntax of Scheme_{cell}

Given e a Scheme_{cell} expression and 𝕏 = ⟨X_{1}, …, X_{n}⟩ a list of lists of variables

if e =  then LL(𝕏, e) =

(lambda (x_{1} … x_{m_{0}}) (letrec ((f_{1} (lambda (y_{1} … y_{m_{1}}) e_{1})) …

(f_{n} (lambda (y_{1} … y_{m_{n}}) e_{n})))

e_{0}))

(letrec

((f_{1} (lambda ([x_{i}]_{∈X_{1}}y_{1} … y_{m_{1}})

LL_{body}(⟨f_{1}, …, f_{n}⟩, 𝕏, e_{1}))) … (f_{n} (lambda ([x_{i}]_{∈X_{n}}y_{1} … y_{m_{n}})

LL_{body}(⟨f_{1}, …, f_{n}⟩, 𝕏, e_{n})))) (lambda (x_{1} … x_{m_{0}})

LL_{body}(⟨f_{1}, …, f_{n}⟩, 𝕏, e′_{0})))

Figure 2: The Lambda Lifting Transformation

Figure 2 summarizes the lambda lifting transformation. If e is of the form on the left in Figure 2, and each element X_{k} in the list of lists 𝕏 defines which variables need to be added to the k^{th} local procedure, then LL(𝕏, e) is the term on the right. The transformation handles any number of mutually recursive nested functions. Each nested function f_{k} has some number (possibly zero) of the identifiers from {x_{1}, …, x_{m_{0}}} added to its parameter list, indicated by the “splicing” notation (f_{k} (lambda ([x_{i}]_{∈X_{k}}y_{1} … y_{m_{k}}))).

The LL_{body} function transforms calls of the lifted local procedure f_{k} by adding the necessary arguments:

LL_{body}(⟨f_{1}, …, f_{n}⟩, 𝕏, (f_{k} e_{1} … e_{m_{k}})) = (f_{k} [x_{i}]_{∈ X_{k}} LL_{body}(F, 𝕏, e_{1}) … LL_{body}(F, 𝕏, e_{m_{k}}))

The rest of the definition of ⇝^{LL_{body}} is a straightforward recursive descent. Note that the variables x_{i} ∈ X_{k} must be in scope at all transformed call sites (f_{k} [x_{i}]_{∈ X_{k}} …).

We use the following notation to denote the different sequences of identifiers, where i ranges from 1 to the number of local procedures, n:

X_{0} = ⟨x_{1}, …, x_{m_{0}}⟩  arguments to outer lambda
F = ⟨f_{1}, …, f_{n}⟩  local procedures
Y_{i} = ⟨y_{1}, …, y_{m_{i}}⟩, 1 ≤ i ≤ n  local procedure arguments
X_{i} = {x_{j} | x_{j} ∈ X_{0} must be added to the argument list of f_{i}}
𝕏 = ⟨X_{1}, …, X_{n}⟩  list of lists of added arguments
𝔽 = ⟨(f_{1}, Y_{1}), …, (f_{n}, Y_{n})⟩  local procedure signatures

We define a Scheme_{cell} term e to be lambda-liftable with respect to a list of lists of variables 𝕏 iff

1. e is of the form of the left-hand side of Figure 2

2. The variables x_{i}, y_{j}, f_{k} are disjoint, for 1 ≤ i ≤ m_{0}, 1 ≤ j ≤ max(m_{k}), 1 ≤ k ≤ n. Also, all binding constructs within e_{0} and the e_{k} bind identifiers distinct from the x_{i}, y_{j}, and f_{k}.

3. All occurrences of each f_{k} in e_{0}, e_{1}, …, e_{n} are in operator position, for 1 ≤ k ≤ n. This guarantees that no f_{k} “escapes”, and thus that all call sites are known.

4. The list of lists of variables, 𝕏, has n elements, X_{1}, …, X_{n}. Letting k range from 1 to n, and treating each X_{k} as a set, we require that for each k,

(a) X_{k} ⊆ {x_{1}, …, x_{m_{0}}}

(b) X_{k} ⊇ (fv(f_{k}) ∩ X_{0}) ∪ (⋃{X_{j} | f_{k} calls f_{j}})

We require that, for a given f_{k}, the arguments to be added are in a solution to a set of constraints, given in Item 4 of the above list. Before lifting f_{k} outside the scope of lambda (x_{1} … x_{m_{0}}), any of the x_{i} referenced in e_{k} must be added to f_{k}’s parameter list. More subtly, if f_{k} calls f_{j}, i.e. if an application (f_{j} e_{1} … e_{m_{j}}) is a subterm of e_{k}, then the new parameters which must be sent to the lifted f_{j} must be added (if not already there) to the incoming parameters of f_{k}. Adding these newly required parameters to f_{k} may have an effect on the parameters added to any f_{i}’s which, in turn, call f_{k} – and so on. Eventually a fixed point will be reached. The list of arguments to the outer lambda, ⟨x_{1}, …, x_{m_{0}}⟩ is always a solution to the set of constraints, though not necessarily the smallest solution.

4 The Metalanguage

In order to prove the correctness of the lambda lifting transformation, we will translate the beforeand-after Scheme_{cell} terms into the metalanguage presented in [WS97]. We then show that the translations are equivalent in the operational term model of the metalanguage.

The metalanguage is based on PCF [Plo77], extended with recursive, sum, and product types and with operators for a global store and I/O. Figure 3 presents the syntax and operational semantics of the metalanguage. In [WS97], we show how the recursive types allow the metalanguage to serve as a model for a variety of source languages, including Scheme and Idealized Algol.

The base types include integers int, booleans bool, processes pr and references ref (τ). Types are possibly infinite trees which respect the grammar given for τ. The typing rules are standard and omitted. A typing judgement is given as Γ ⊢ M:τ and read as “term M has type τ assuming Γ assigns types to each free variable in M.” Location constants l^{τ} are annotated with the type of Syntax:

M ::= x | n | c | l^{τ} | λx:τ.M | MM τ ::= o | τ→τ | τ+τ | τ×τ o ::= unit | bool | int | ref (τ) | pr

Store Operations (→_{sto}):

M →_{pcf} M′ ⇒ ⟨⟨M ; Σ⟩⟩ →_{sto} ⟨⟨M′ ; Σ⟩⟩
⟨⟨new^{τ} MN ; Σ⟩⟩ →_{sto} ⟨⟨Nl^{τ} ; Σ[l^{τ} ↦ M]⟩⟩ if l^{τ} ∉ dom(Σ) ∪ locs(rng(Σ), M, N)
⟨⟨deref^{τ} l^{τ} M ; Σ⟩⟩ →_{sto} ⟨⟨MN ; Σ⟩⟩ if Σ(l^{τ}) = N
⟨⟨update^{τ} l^{τ} MN ; Σ⟩⟩ →_{sto} ⟨⟨N ; Σ[l^{τ} ↦ M]⟩⟩ if l^{τ} ∈ dom(Σ)

I/O Operations (→^{a}_{io}):

\frac{⟨⟨M ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨write n M′ ; Σ′⟩⟩}{⟨⟨M ; Σ⟩⟩ →^{!n}_{io} ⟨⟨M′ ; Σ′⟩⟩}  \frac{⟨⟨M ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨read M′ ; Σ′⟩⟩}{⟨⟨M ; Σ⟩⟩ →^{?n}_{io} ⟨⟨M′ n ; Σ′⟩⟩}

\frac{⟨⟨M ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨stop ; Σ′⟩⟩}{⟨⟨M ; Σ⟩⟩ →^{√}_{io} ⟨⟨stopped ; Σ′⟩⟩}

Figure 3: Syntax and Semantics of the Metalanguage

term they point to, and are given type ref (τ). PCF reduction, →_{pcf} , is the standard call-by-name relation between terms given in [Plo77] and is omitted.

Store and I/O operations take place in a term-store pair called a state. The store component of a state is a finite map from locations to terms. The first rule for →_{sto} says that any PCF-reduction can take place within a state context. The new operator allocates a new location in the store, initializes the fresh location to its first argument, and invokes its second argument with the new location. The deref operator invokes its second argument with the value in the store at the location given by its first argument. The update operator destructively updates the location given by its first argument to be the term given by its second argument and then invokes its third argument. Note that →_{sto} transitions may take place only if a store operator is in the leftmost-outermost position. The reflexive, transitive closure of →_{sto} is denoted →_{sto}^{∗}.

The I/O operators are similarly restricted to firing only when they are in the leftmost-outermost position of the term component of a state. The actions emitted by I/O transitions lead us to a natural notion of state equivalence, namely strong bisimulation. The definition of bisimulation (≈_{bisim}) is standard [Mil90] and is omitted. Roughly speaking, two states are bisimilar if they can always take identical labeled transitions. ≈_{bisim} can be formulated as the greatest fixed point of an operator [−]_{bisim} on relations.

5 Contextual and Extensional Equivalence

Two terms are contextually equivalent (≅_{∀C}) if they give the same observable behavior in all state contexts. That is,

Definition 1 (contextual equivalence, ≅_{∀C}) If Γ ⊢ M, N:τ, then Γ ⊢ M ≅_{∀C} N:τ iff for all closing contexts C[−_{τ}] of type pr that respect Γ, and for all stores Σ,

⟨⟨C[M] ; Σ⟩⟩ ≈_{bisim} ⟨⟨C[N] ; Σ⟩⟩

A context C[−] respects a type assignment Γ if C[−] binds the free variables of any term inserted in the context hole with binders of the correct type.

For terms M and N containing no locations, Definition 1 is equivalent to one in which Σ is fixed to be empty; this includes all of our applications. The meaning of a metalanguage term M is defined to be the ≅_{∀C}-equivalence class of M. Contextual equivalence is, by the form of its definition, a congruence – that is, it is preserved by all term constructors of the language. Furthermore, it is easy to show (using the confluence property for PCF), that if M =_{pcf} N, then M ≅_{∀C} N. Hence the structure obtained by taking equivalence classes of open terms under ≅_{∀C} is a model of typed lambda-calculus. This is our operationally-based term model. Because this is a model, ordinary reasoning using β-conversion is valid in the model.

The quantification over all contexts makes ≅_{∀C} difficult to establish directly. We must consider not only contexts in which the terms are executed, but also contexts that pass the terms around, put many copies of them in the store, etc.

Our major tool for easing this proof burden is a “context lemma” which states that two terms are contextually equivalent if and only if they are equivalent in a smaller set of contexts we call extensional contexts. At function types, extensional contexts are head contexts, as in Milner’s context lemma for PCF [Mil77] – that is, extensionally equivalent functions take the same argument to extensionally equivalent results. Extensional contexts for the other type constructors are natural: for product types, both projections must be extensionally equivalent, and for sum types, summands exposed by the case operator must be equivalent. We omit the formal definition of extensional equivalence, denoted ≅_{ext}, in this abstract. We then have, from [WS97]:

Theorem 2 (Context Lemma)

Γ ⊢ M ≅_{ext} N:τ ⇔ Γ ⊢ M ≅_{∀C} N:τ

6 Translation from Scheme_{cell} to the Metalanguage

Figure 4 defines the semantics of Scheme_{cell} terms via a syntax-directed CPS translation, [[−]]_{cell}, into the metalanguage. The translation is a standard CPS translation, as in [Plo75, Cli84, App92], and closely follows the official denotational semantics of Scheme [CR91].

The type Val of expressed values is a recursive sum:

Val = N + F  expressed values
N = int  integers
F = Val^{∗}→(Val→pr)→pr procedures

[[n]]_{cell} = λκ:Val→pr. in_{N} n κ
[[x]]_{cell} = λκ:Val→pr.κ x
[[(lambda (x_{1} … x_{n}) e)]]_{cell} = λκ:Val→pr.
in_{F} (λv^{∗}:Val^{∗}.λκ′:Val→pr.

[[e]]_{cell}[(listref_{1} v^{∗})/x_{1}, …, (listref_{n} v^{∗})/x_{n}] κ′) κ

[[(e_{0} e_{1} … e_{n})]]_{cell} = λκ:Val→pr.[[e_{0}]]_{cell}(λf:Val.
[[e_{1}]]_{cell}(λv_{1}:Val. · · ·
[[e_{n}]]_{cell}(λv_{n}:Val.
out_{F} f (λf′:Val^{∗}→(Val→pr)→pr.
f′ ⟨v1, …, v_{n}⟩ κ)) …))
[[(make-cell e)]]_{cell} = λκ:ref (Val)→pr.[[e]]_{cell}(λv:Val. new v κ)
[[(cell-ref x)]]_{cell} = λκ:Val→pr. deref x κ

[[(cell-set! x e)]]_{cell} = λκ:Val→pr.[[e]]_{cell}(λv:Val. update x v (κ Ω)))

[[(letrec ((x_{1} e_{1}) … (x_{n} e_{n})) e)]]_{cell} = λκ:Val→pr.

new Ω_{Val}(λx_{1}:ref (Val). · · · new Ω_{Val}(λx_{n}:ref (Val).

[[e_{1}]]_{cell}(λv_{1}:Val. update x_{1}v_{1} ⋯

[[e_{n}]]_{cell}(λv_{n}:Val. update x_{n}v_{n} ([[e]]_{cell}κ) ⋯)

Figure 4: CPS translation from Scheme_{cell} to metalanguage

For each summand S of the Val type, we use CPS injection and extraction combinators, in_{S} :S→(Val→pr)→ pr and out_{S} :Val→(S→pr)→pr. We also use ⟨−, …, −⟩ and listref_{i} for the evident list operations. All these can be easily defined in the metalanguage.

Identifiers denote either values of type Val or cells of type ref (Val).

A Scheme_{cell} lambda-expression returns a closure which expects a list of values v^{∗} and a continuation κ.

The rule for letrec follows the official semantics of Scheme [CR91], which initializes the variables to undefined values while building up the scope (var/loc pairs) and then destructively updates the variables to their correct values.

It is easy to show that if we apply the translation [[−]]_{cell} to well-typed Scheme_{cell} terms, the resultant metalanguage terms will be well-typed:

Lemma 3 For a Scheme_{cell} term e, and a type assumption Γ mapping variables to {Val, ref (Val)},

Γ ⊢_{cell} e:ok ⇒ Γ ⊢ [[e]]_{cell}:(Val→pr)→pr

7 Correctness of Incremental Lambda Lifting

Our goal is to show that the incremental lambda lifting transformation preserves the meaning of Scheme_{cell} terms; that is:

Theorem 4 (Correctness of Incremental Lambda Lifting) For any Scheme_{cell} expression e and list of lists of variables 𝕏 such that e is lambda-liftable with respect to 𝕏, and any Γ mapping the free variables of e to ref (Val), if Γ ⊢_{cell} e:ok, then

Γ ⊢ [[e]]_{cell} ≅_{∀C} [[LL(𝕏, e)]]_{cell}:(Val→pr)→pr

Proof:

1. First we check that the lambda lifting transformation preserves types; that is,

Γ ⊢_{cell} e:ok ⇒ Γ ⊢ [[LL(𝕏, e)]]_{cell}:(Val→pr)→pr

The proof is by structural induction on ⊢_{cell}. We need criterion (4b) from the list of criteria for lambda-liftability in order to be assured that the identifiers in X_{k} added to calls of the lifted procedure f_{k} will be in scope at the modified call sites.

2. By appeal to the Context Lemma (Theorem 2) and the definition of ≅_{ext}, it suffices to show that for all closing substitutions σ mapping free variables to closed terms of type ref (Val), all closed terms K of type Val→pr, and all stores Σ,

⟨⟨([[e]]_{cell}σ) K ; Σ⟩⟩ ≈_{bisim} ⟨⟨([[LL(𝕏, e)]]_{cell}σ) K ; Σ⟩⟩

3. To show these states are bisimilar, we construct a relation S_{LL} between metalanguage states that characterizes the syntactic differences between (non-transformed) Scheme_{cell} programs and those programs after incremental lambda lifting, as they reduce under →^{α}_{io}. As the original program and its lambda-lifted version run, there are several different ways in which corresponding subterms can differ:

(a) The initial translations, before any evaluation takes place, will differ as follows. On the left-hand (non-lambda-lifted) side, the continuation term K will be immediately invoked with a closure for the Scheme_{cell} term

(lambda (X_{0}) (letrec (… (f_{k} (lambda (Y_{k}) e_{k})) …)) e_{0})

The closure sent to K expects values for each identifier in X_{0}, and once invoked with such arguments, will do allocation for each of the local procedure closures. We represent the closure sent to K using a macro^{1} L, which is parameterized by the identifiers used during lambda lifting and by the bodies of the local procedures. The term component of the state will look like:

(K L(X_{0}, 𝔽, [[e_{0}]]_{cell}, …, [[e_{n}]]_{cell} ))

and the store is unchanged.

1The final paper will contain the explicit definitions of L and other macros.

On the right-hand (lambda-lifted) side, much more happens before a closure is sent to K. The closures for the local procedures f_{1}, …, f_{n} are allocated and initialized, and then a closure for the translation of

(lambda (X_{0}) LL_{body}(⟨f_{1}, …, f_{n}⟩, 𝕏, e_{0}))

is sent to K. We represent the closure sent to K on the right-hand side using a macro R(X_{0}, P) which takes only the X_{0} identifier list and the body of the lambda (X_{0}) abstraction. So we will have a state with a term component of:

(K R(X_{0}, [[LL_{body}(F, 𝕏, e_{0})]]_{cell}))[l_{i}/f_{i}]_{i=1}^{n}

The store will have newly allocated locations l_{1}, …, l_{n} initialized to closures, for which we use a macro C′(X_{k}, Y_{k}, P). For 1 ≤ k ≤ n we have:

Σ(l_{k}) = C′(X_{k}, Y_{k}, [[LL_{body}(F, 𝕏, e_{k})]]_{cell})[l_{i}/f_{i}]_{i=1}^{n}

(b) We next consider what happens when the closure sent to K above is actually used. This corresponds to sending the closure a list of arguments, say ⟨M_{1}, …, M_{m_{0}}⟩, which are bound to the identifiers x_{1}, …, x_{m_{0}}. The left-hand side allocates n fresh locations, storing new instances of the closures for its local procedures at these locations. Each of these newly-created closures inherits the bindings of values to the x_{1}, …, x_{m_{0}} identifiers. After creating the new local procedure closures, the body, e_{0}, is executed, at which point we will have a state with a term component something like:

[[e_{0}]]_{cell}[l_{k}/f_{k}]_{k=1}^{n}[M_{j}/x_{j}]_{j=1}^{m_{0}}

and with a store that looks like:

Σ[l_{k} ↦ (C(Y_{k}, M_{f_{k}})[l_{i}/f_{i}]_{i=1}^{n}[M_{j}/x_{j}]_{j=1}^{m_{0}})]_{k=1}^{n}

where the C macro represents a closure for the translation of a local procedure. On the right-hand, lambda-lifted, side, much less happens when the closure for lambda(X_{0}) is applied. Evaluation of the lambda-lifted body, LL_{body}(⟨f_{1}, …, f_{n}⟩, 𝕏, e_{0}) proceeds immediately with the substitution [M_{j}/x_{j}]_{j=1}^{m_{0}}, as the closures were initialized in the previous step, so we will have a state with a term component such as

[[LL_{body}(⟨f_{1}, …, f_{n}⟩, 𝕏, e_{0})]]_{cell}[l_{i}/f_{i}]_{i=1}^{n}[M_{j}/x_{j}]_{j=1}^{m_{0}}

and the store component will not have changed significantly.

(c) Finally, let us consider what happens at runtime when a local procedure f_{k} is applied. On the left-hand side, we represent an application using the A macro, which takes the procedure identifier, each argument, and a continuation. So we will have something like:

A(f_{k}, [[e_{1}]]_{cell}, …, [[e_{m_{k}}]]_{cell}, M_{cont})

On the left-hand side, the application will also take the arguments added by the lambda lifting transformation, and we use the A′ macro, which is the same as A but with an added parameter, so we have:

A′(f_{k}, X_{k}, [[e′_{1}]]_{cell}, …, [[e′_{m_{k}}]]_{cell}, N_{cont})

Given 𝕏 = ⟨X_{1}, …, X_{n}⟩ and 𝔽 = ⟨(f_{1}, Y_{1}), …, (f_{n}, Y_{n})⟩, ⇝^{LL_{body}} is the least relation closed under the following rules:

Γ[x:τ], 𝕏, 𝔽 ⊢ x ⇝^{LL_{body}} x:τ, x ∉ dom(𝔽) (cong-var)
Γ, 𝕏, 𝔽 ⊢ l^{τ} ⇝^{LL_{body}} l^{τ}:ref (τ) (cong-loc)
\frac{Γ, 𝕏, 𝔽 ⊢ M ⇝^{LL_{body}} N:τ′→τ Γ ⊢ M′ ⇝^{LL_{body}} N′:τ′}{Γ, 𝕏, 𝔽 ⊢ (M M′) ⇝^{LL_{body}} (N N′):τ} (cong-app)

Γ, 𝕏, 𝔽 ⊢ M_{i} ⇝^{LL_{body}} N_{i}:(Val→pr)→pr, 1 ≤ i ≤ m_{k}

Γ, 𝕏, 𝔽 ⊢ M_{cont} ⇝^{LL_{body}} N_{cont}:Val→pr M = A(f_{k}, M_{1}, …, M_{m_{k}}, M_{cont}) N = A′(f_{k}, X_{k}, N_{1}, …, N_{m_{k}}, N_{cont})

Γ, 𝕏, 𝔽 ⊢ M ⇝^{LL_{body}} N:pr

(app-f_{k})

Figure 5: Definition of ⇝^{LL_{body}} on Terms

The left-hand side will retrieve its most recently created f_{k} closure and send it a list of m_{k} parameters. When evaluation reaches the translated body of the procedure, e_{k}, references to x_{j} ∈ X_{0} are resolved by the substitution in effect when the closure for f_{k} was created. The right-hand side will retrieve the closure for f_{k} created in Step 3a. Because the closure was stored before the current substitution for x_{j} ∈ X_{0} was in effect, the values for each such x_{j} required by f_{k} must be sent at application time, which happens as a result of the lambda-lifting transformation.

4. Once the closures for lambda (X_{0}) have been evaluated, the differences between the left and

right-hand sides correspond to calls to the lifted local procedures. The relation ⇝^{LL_{body}} between metalanguage terms, defined in Figure 5, encompasses the differences found within translations of procedure bodies. The rule app-f_{k} is the most interesting – it says that two applications (covered by the A and A′ macros) are ⇝^{LL_{body}}-related if the right-hand side adds the correct arguments, X_{k}, at the call site.

5. The candidate bisimulation relation S_{LL} is defined in Figure 6. The “interesting” differences between the translations of Scheme_{cell} terms and their lambda-lifted counterparts are abstracted out using fresh variables u_{i} and v_{i} as placeholders, for i ranging from 1 to the total number of different corresponding subterms.

The u_{i} variables map to the \underline{u}nevaluated closures for lambda (X_{0}) discussed in Step 3a above. On the right-hand side, we have n closures already initialized in the store, at locations l_{1}, …, l_{n}.

The v_{i} variables map to the e\underline{v}aluated closures discussed in Step 3b above. The left-hand side has n freshly allocated locations bound to its local procedure identifiers f_{1}, …, f_{n}. Both sides have an active substitution for the x_{j} ∈ X_{0} arguments. Note that the closures newly stored in Σ (the left-hand store) have substitutions for the x_{j} ∈ X_{0} as part of the closure.

Definition 5 (S_{LL}) Given 𝕏 = ⟨x_{1}, …, x_{n}⟩ and 𝔽 = ⟨(f_{1}, Y_{1}), …, (f_{n}, Y_{n})⟩,

S_{LL} =^{def} {(⟨⟨M ; Σ⟩⟩σ, ⟨⟨M ; Σ′⟩⟩σ′) |

preamble \{ \begin{matrix}∃u, v ∈ Var^{∗} s.t. \\ fv(M, rng(Σ), rng(Σ′)) ⊆ u ∪ v \\ σ = σ_{u} ∪ σ_{v} \\ σ′ = σ′_{u} ∪ σ′_{v} \\ ∃Σ_{0} s.t. dom(Σ_{0}) ⊆ dom(Σ), and dom(Σ_{0}) ⊆ dom(Σ′) \\ (Γ ⊢ M:pr) ⇒ (Γ(u_{i}) = Val, Γ(v_{i}) = pr) \end{matrix}

unevaluated ; lambda (X) ; closures \{ \begin{matrix}σ_{u} = [ u_{i} ↦ (L(X_{0}, 𝔽, M_{0}^{i}, …, M_{n}^{i})) ]_{i=1}^{#u} \\ σ′_{u} = [u_{i} ↦ (R(X_{0}, N_{0}^{i})[l_{k}/f_{k}]_{k=1}^{n}) ]_{i=1}^{#u} \\ Σ′ = Σ_{0}[l_{k} ↦ (C′(X_{k}, Y_{k}, N_{k})[l_{i}/f_{i}]_{i=1}^{n}) ]_{k=1}^{n} \\ \begin{matrix}Γ, 𝕏, 𝔽 ⊢ M_{0}^{i} ⇝^{LL_{body}} N_{0}^{i}:(Val→pr)→pr \\ Γ, 𝕏, 𝔽 ⊢ M_{k}^{i} ⇝^{LL_{body}} N_{k}:(Val→pr)→pr \end{matrix} \} & \begin{matrix}1 ≤ i ≤ #u \\ 1 ≤ k ≤ n \end{matrix} \end{matrix}

evaluated ; lambda (X) ; closures \{ \begin{matrix}σ_{v} = [v_{i} ↦ M_{i}[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} ]_{i=1}^{#v} \\ σ′_{v} = [v_{i} ↦ N_{i}[N_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} [l_{i}/f_{i}]_{i=1}^{n}]_{i=1}^{#v} \\ Σ = Σ_{0}[l_{k}^{i} ↦ (C(Y_{k}, M_{k}^{i})[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}}) ]_{i=1,k=1}^{#v, n} \\ Γ, 𝕏, 𝔽 ⊢ M_{i} ⇝^{LL_{body}} N_{i}:pr, for 1 ≤ i ≤ #v \\ Γ, 𝕏, 𝔽 ⊢ M_{x_{j}}^{i} ⇝^{LL_{body}} N_{x_{j}}^{i}:Val, for 1 ≤ i ≤ #v, 1 ≤ j ≤ m_{0} \end{matrix}

}

Figure 6: The S_{LL} Candidate Simulation

All procedure bodies are related by ⇝^{LL_{body}}.

6. With an eye towards the coinductive definition of bisimulation, we show that:

S_{LL} ⊆ [≈_{bisim} ∘ S_{LL} ∘ ≈_{bisim}]_{bisim}

This requires an induction on the number of steps to an input-output operation, which is done using a case analysis on the form of M; the interesting cases are when M is headed by a u_{i} or v_{i} variable.

7. S_{LL} ⊆ ≈_{bisim} follows by a straightforward application of “bisimulation up to” reasoning, as in [Mil90].

8. Finally, we show that the S_{LL} relation encompasses the translations of all pre- and postlambda-lifted programs, but this is easy, as the S_{LL} was defined with exactly such programs in mind.

8 Conclusion

Given a source-to-source transformation which we wish to show preserves meaning, we do the following:

1. Define a translation from the source language to the metalanguage. The translation must be sound with respect to the semantics of the source language.

2. Define a “candidate bisimulation relation” which characterizes all of the ways in which corresponding metalanguage subterms might differ as the translations of pre- and post-transformed terms execute in a state context.

3. Prove that the relation defined above is contained in ≈_{bisim}. These proofs involve reducing each possible form of the translated terms in extensional contexts of the appropriate type and verifying that as the states reduce they stay within the candidate relation. While translation from the source language to our metalanguage is denotational in style, the proofs of bisimulation tend to involve lots of operational reasoning – thus the moniker “almost denotational” for our approach.

The relations constructed as a basis for a proof of correctness are distillations of the essence of the effects of the transformation being considered. As such, the proof method as a whole serves to clarify and debug the formalization of any complex transformation. We have found that our methods are able to handle relatively complex source-to-source transformations such as incremental lambda lifting and language-to-language transformations such as assignment elimination, even in the presence of a global store and imperative features.

We plan on extending this research to handle more complicated type systems, such as those found in object-oriented languages. We also plan to investigate using our method to justify transformations which rely on flow analysis. Also, the process of inventing candidate bisimulation relations and verifying their correctness is both tricky and time consuming, and we would like to pursue possible tools to facilitate the process.

References

[Abr90] Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, pages 65–116. Addison-Wesley, 1990.

[App92] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, Cambridge, 1992.

[CH94] William D. Clinger and Lars Thomas Hansen. Lambda, the ultimate label; or a simple optimizing compiler for scheme. In Proc. 1994 ACM Symposium on Lisp and Functional Programming, pages 128–139, 1994.

[Cli84] William Clinger. The scheme 311 compiler: An exercise in denotational semantics. In Proc. 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, August 1984.

[CR91] William Clinger and Jonathan A. Rees. The revised^{4} report on the algorithmic language scheme. ACM LISP Pointers, 4(3), 1991.

[Fel87] Matthias Felleisen. The Calculi of Lambda-v-cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Indiana University, 1987.

[Gor94] Andrew D. Gordon. Functional Programming and Input/Output. Cambridge University Press, Cambridge, 1994.

[Gor95] Andrew D. Gordon. Bisimilarity as a theory of functional programming. In Proceedings of 11th Conference on Mathematical Foundations of Programming Semantics, 1995.

[Hug82] R. J. M. Hughes. Super-combinators: A new implementation method for applicative languages. In Proc. 1982 ACM Symposium on Lisp and Functional Programming, pages 1–10, 1982.

[KKR^{+}86] David A. Kranz, Richard Kelsey, Jonathan A. Rees, Paul Hudak, James Philbin, and Norman I. Adams. Orbit: An optimizing compiler for scheme. In Proceedings SIGPLAN ’86 Symposium on Compiler Construction, 1986. SIGPLAN Notices 21 (7), July, 1986, 219-223.

[Mil77] Robin Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, 4:1–22, 1977.

[Mil90] Robin Milner. Operational and algebraic semantics of concurrent processes. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 1201–1242. MIT Press/Elsevier, 1990.

[MMH96] Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Conf. Rec. 23rd ACM Symposium on Principles of Programming Languages, pages 271–283, 1996.

[Mor68] James H. Morris, Jr. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, Cambridge, MA, 1968.

[MT91] Ian A. Mason and Carolyn L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1:287–327, 1991.

[ORW95] Dino P. Oliva, John D. Ramsdell, and Mitchell Wand. The VLISP verified prescheme compiler. Lisp and Symbolic Computation, 8(1/2):111–182, 1995.

[Par81] David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer Science: 5th GI-Conference, Karlsruhe, volume 104 of Lecture Notes in Computer Science, pages 167–183, Berlin, Heidelberg, and New York, March 1981. Springer-Verlag.

[PJ87] Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall International, 1987.

[Plo75] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[Plo77] Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[Sta94] Ian Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, December 1994. Also published as Technical Report 363, University of Cambridge Computer Laboratory.

[Sul96] Gregory T. Sullivan. Operationally-Based Models of Higher-Order Imperative Programming Languages. PhD thesis, Northeastern University, December 1996.

[TW96] Jerzy Tiuryn and Mitchell Wand. Untyped lambda-calculus with input-output. In H. Kirchner, editor, Trees in Algebra and Programming: CAAP’96, Proc. 21st International Colloquium, volume 1059 of Lecture Notes in Computer Science, pages 317–329, Berlin, Heidelberg, and New York, April 1996. Springer-Verlag.

[WO92] Mitchell Wand and Dino P. Oliva. Proving the correctness of storage representations. In Proc. 1992 ACM Symposium on Lisp and Functional Programming, pages 151–160, 1992.

[WS94] Mitchell Wand and Paul Steckler. Selective, lightweight closure conversion. In Conf. Rec. 21st ACM Symposium on Principles of Programming Languages, pages 435–445, 1994. Revised version submitted for publication.

[WS97] Mitchell Wand and Gregory T. Sullivan. Denotational semantics using an operationallybased term model. In Conf. Rec. 24th ACM Symposium on Principles of Programming Languages, page ??, 1997.