Normalization by Evaluation for the Computational Lambda-Calculus

To appear, Typed Lambda Calculi and Applications 2001

Andrzej Filinski

BRICS^{⋆}, Department of Computer Science, University of Aarhus

                       andrzej@brics.dk

Abstract. We show how a simple semantic characterization of normalization by evaluation for the λ_{βη}-calculus can be extended to a similar construction for normalization of terms in the computational λ-calculus. Specifically, we show that a suitable residualizing interpretation of base types, constants, and computational effects allows us to extract a syntactic normal form from a term’s denotation. The required interpretation can itself be constructed as the meaning of a suitable functional program in an ML-like language, leading directly to a practical normalization algorithm. The results extend easily to product and sum types, and can be seen as a formal basis for call-by-value type-directed partial evaluation.

1 Introduction

The basic idea of normalization by evaluation is to extract the normal form (with respect to some notion of conversion) of a term from its interpretation in a suitably chosen, quasi-syntactic denotational model of the conversion relation [5].

For instance, let us consider the interpretation of a pure, simply typed lambdaterm E in a model where all base types are interpreted as the set Λ of well-formed lambda-terms, and function types are interpreted as full set-theoretic function spaces. Then it is fairly simple to (at least informally) construct for any type τ, a function nf_{τ} ∈ [[τ]] → Λ, such that for any closed term Ẽ : τ in βη-long normal form, nf_{τ} ([[Ẽ]]) =_{α} Ẽ. We proceed as follows:

Let τ = τ_{1} → ⋯ → τ_{n} → b (n ≥ 0), where each τ_{i} = τ_{i1} → ⋯ → τ_{im_{i}} → b_{i}. Then Ẽ : τ must be of the form λx_{1}. · · · . λx_{n}. x_{i} Ẽ_{1} ⋯ Ẽ_{m_{i}} where each Ẽ_{j} : τ_{ij} is again in normal form. We can thus define nf_{τ} inductively as:

nf_{τ} = λf. LAM(v_{1}, …, LAM(v_{n}, f (λa_{1}. · · · . λa_{m_{1}}. APP (···APP (VAR v_{1}, nf_{τ_{11}} a_{1}) ⋯, nf_{τ_{1m_{1}}} a_{m_{1}})) ⋮ (λa_{1}. · · · . λa_{m_{n}}. APP (···APP (VAR v_{n}, nf_{τ_{n1}} a_{1}) ⋯, nf_{τ_{nmn}} a_{m_{n}})) ))

where the v_{i} are “fresh” variable names, and we use VAR, LAM , and APP for constructing elements of Λ, to distinguish them from function abstraction and application in the set-theoretic model.

⋆ Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

Moreover, it is easy to see that nf_{τ} ([[−]]) is in fact a normalization function: since βη-convertibility is sound for equality in all set-theoretic interpretations (and hence also in our chosen one), we have, for all terms E and E′, that E =_{βη} E′ implies [[E]] = [[E′]]. So if Ẽ is the βη-long normal form of E, then nf_{τ} ([[E]]) = nf_{τ} ([[Ẽ]]) =_{α} Ẽ.

Finally, if we can also construct a syntactic term nf_{τ} : τ → Λ such that nf_{τ} [[E]] = [[nf_{τ} E]], then nf_{τ} E is a closed term of base type Λ, and can thus be executed as a functional program. This gives us a very efficient executable algorithm for computing normal forms, and was indeed one of the motivations behind the construction [4, 3]: we are reducing the general problem of term normalization to a special case for which we already have a good solution.

A natural question arises whether this semantic technique for normalization of lambda-terms is inherently tied to βη-conversion. Somewhat surprisingly, it is not: in the following, we show how the same idea can be used to normalize terms with respect to the computational lambda-calculus [16], where it also extends to product and – more notably – sum types. In fact, we can systematically extract the computational normal form of any pure, typed lambda-term from only its observable behavior in an imperative functional language such as ML.

Despite the relative simplicity of the construction, there are still a few technical details to nail down, even in the purely functional case. Accordingly, we will first present in Section 2 the normalization algorithm for a call-by-name setting, then show in Section 3 how it can be refined to call-by-value. In Section 4 we show how to further extend the normalizer with product and sum types, and in Section 5 we consider the relationship between normalization by evaluation and type-directed partial evaluation. Finally, Section 6 concludes and points out some directions for further work.

2 Normalization by evaluation for call by name

The normalization construction sketched above, essentially due to Berger and Schwichtenberg [4], has been studied in many formulations [8], including more syntactic variants [2] as well as category-theoretic ones [1, 6]. In the following, we present it in a call-by-name functional-programming setting [11]; this formulation extends particularly naturally to the call-by-value variant in the next section.

2.1 Language and semantic framework

Syntax. A signature Σ includes, first, a collection of base types b. The set of well-formed Σ-types τ is then given by the grammar

τ ::= b | τ_{1} → τ_{2}

Further, Σ assigns Σ-types to a (possibly infinite) collection of constants c. Let x range over variable names, and Γ be a finite assignment of Σ-types to variables. Then the set of well-typed Σ-terms Γ ⊢_{Σ} E : τ is again given by the usual rules:

\frac{Σ(c) = τ}{Γ ⊢_{Σ} c : τ} \frac{Γ (x) = τ}{Γ ⊢_{Σ} x : τ} \frac{Γ, x: τ_{1} ⊢_{Σ} E : τ_{2}}{Γ ⊢_{Σ} λx^{τ_{1}}.E : τ_{1} → τ_{2}}  \frac{Γ ⊢_{Σ} E_{1} : τ_{1} → τ_{2} Γ ⊢_{Σ} E_{2} : τ_{1}}{Γ ⊢_{Σ} E_{1} E_{2} : τ_{2}}

Finally, a Σ-program is a closed Σ-term of base type.

Semantics. For concreteness, and to accommodate the refinements in Section 5, we consider only a specific, domain-theoretic framework, but the results also adapt easily to a set-theoretic setting, by forgetting the order structure.

We work in the setting of (bottomless) cpos and (total) continuous functions. We also use the concept of a monad (more precisely, a Kleisli triple) T = (T, η, ⋆), where T maps cpos to cpos, η_{A} ∈ A → T A is the unit function, and ⋆_{A,B} ∈ T A×(A→T B)→T B is the extension operation written backwards, i.e., with the function last; this makes longer sequences of extensions easier to read. We omit the subscripts on units and extensions where they are clear from the context. A particularly important instance is the lifting monad, T_{l}, where T^{l}A = A_{⊥} = {ιa | a ∈ A} ∪ {⊥} with the usual ordering, η^{l} a = ιa, ⊥ ⋆^{l} f = ⊥, and (ιa) ⋆^{l} f = f a.

An interpretation I of a signature Σ is a pair of functions (B, C). B assigns to every base type b in Σ, a cpo B(b). This assignment determines for any Σ-type τ, a pointed (i.e., containing a least element) cpo [[τ]]^{I} as follows:

[[b]]^{I} = T^{l}B(b) [[τ_{1} → τ_{2}]]^{I} = [[τ_{1}]]^{I} → [[τ_{2}]]^{I}

where A → B denotes the cpo of all continuous functions between A and B. We also give meaning to a type assignment Γ as a finite product:

[[Γ]]^{I} = ∏_{x∈dom Γ} [[Γ (x)]]^{I} = {ρ | ∀x ∈ dom Γ. ρx ∈ [[Γ (x)]]^{I}}

The function C assigns to every Σ-constant c an element C(c) ∈ [[Σ(c)]]^{I}. Again this assignment extends to a full semantics of terms: for any Γ ⊢_{Σ} E : τ, we define a continuous function [[E]]^{I} ∈ [[Γ]]^{I} → [[τ]]^{I} in the usual way:

\begin{aligned}[[c]]^{I} ρ & = & C(c) \\ [[x]]^{I} ρ & = & ρx \end{aligned}  \begin{aligned}[[λx^{τ}.E]]^{I} ρ & = & λa.[[E]]^{I} (ρ[x ↦ a]) \\ [[E_{1} E_{2}]]^{I} ρ & = & [[E_{1}]]^{I} ρ([[E_{2}]]^{I} ρ) \end{aligned}

Equivalence and normal forms. We say that two Σ-terms E and E′ are semantically equivalent, written ⊧ E = E′, if for all interpretations I of Σ, [[E]]^{I} = [[E′]]^{I}. It is easy to see that if E =_{βη} E′ then ⊧ E = E′. More generally, if Int is a subset of all possible interpretations of Σ (e.g., constraining the meanings of some of the constants), we write ⊧^{Int} E = E′ iff for all I ∈ Int, [[E]]^{I} = [[E′]]^{I}; we will return to this notion in Section 5.

Among the well-typed terms Γ ⊢_{Σ} E : τ, we distinguish those in normal and atomic (also known as neutral) form:

\frac{Γ ⊢^{at} E : b}{Γ ⊢^{nf} E : b}  \frac{Γ, x: τ_{1} ⊢^{nf} E : τ_{2}}{Γ ⊢^{nf} λx^{τ_{1}}.E : τ_{1} → τ_{2}}
\frac{Γ (x) = τ}{Γ ⊢^{at} x : τ}  \frac{Σ(c) = τ}{Γ ⊢^{at} c : τ}  \frac{Γ ⊢^{at} E_{1} : τ_{1} → τ_{2} Γ ⊢^{nf} E_{2} : τ_{1}}{Γ ⊢^{at} E_{1} E_{2} : τ_{2}}

A normalization function, in the sense of Coquand and Dybjer [5] (but with a semantic notion of equivalence), then maps any term E to a normal-form term norm(E), such that ⊧ norm(E) = E, and such that for all E′ with ⊧ E′ = E, norm(E′) = norm(E).

2.2 A normalization result

The traditional way of computing norm(E) is by repeated β-reductions, possibly followed by η-expansions. However, we can also compute norm by a subtler, semantic method, reduction-free normalization.

Representing lambda-terms. Let V be a set (= discrete cpo) of explicitly typed variable names, and E a set suitable for representing lambda-terms, i.e., allowing us to define injective functions with mutually disjoint ranges,

CST ∈ dom Σ →E, VAR ∈ V→E, LAM ∈ V×E→E, APP ∈ E×E→E

Then for any term E with variables from V, we define its representation ^{⌜}E^{⌝} ∈ E in the obvious way, e.g., ^{⌜}λx.E^{⌝} = LAM (x,^{⌜}E^{⌝}). Because of the injectivity and disjointness assumptions, for any e ∈ E, there is at most one E such that^{⌜}E^{⌝} = e; we need not require that all elements of E represent well-formed lambda-terms, let alone well-typed ones.

(We deliberately use a very concrete representation of terms, rather than a higher-level notion based on abstract syntax with binding constructs such as [12]. Our ultimate goal is to implement the normalization process as a simple functional program, without assuming potentially expensive operations, such as capture-avoiding substitution, as primitives.)

The task is now to construct an interpretation I_{r} of Σ such that we can recover E’s normal form from [[E]]^{I_{r}}. We want to use the idea from the introduction, but need to account rigorously for “fresh” variable names. Freshness could be captured abstractly in a framework such as Fraenkel-Mostowski sets [14], but this again removes us a level from a direct implementation. Instead, we will explicitly generate non-clashing variable names. Perhaps the simplest scheme for doing so is through de Bruijn levels [2, 11], but we adopt instead a scheme for generating “globally unique”, gensym-style names using a monad, as it scales better to the constructions of the next section.

Auxiliary definitions. We first define the name-generation monad T_{g}. This is just a state-passing monad atop T_{l}; the state is the “next free index”:

T^{g}A = N → T^{l}(A × N)  η^{g} a = λi.η^{l} (a, i)  t ⋆^{g} f = λi.ti ⋆^{l} λ(a, i′).f ai′

With respect to T^{g}, we can define an effectful computation that generates a fresh name, and one that initializes the index within a delimited subcomputation:

new_{τ} ∈ T^{g}V
new_{τ} = λi.η^{l} (g_{i}^{τ} , i + 1)

withct_{A} ∈ T^{g}A → T^{l}A
withct_{A} t = t0 ⋆^{l} λ(a, i′).η^{l} a

where the g_{i}^{τ} ∈ V are assumed distinct for distinct i. Note that the codomain of withct_{A} is simply T^{l}A, i.e., withct t represents a side-effect-free, purely functional computation, for any name-generating computation t.

The residualizing interpretation. We can now define a suitable residualizing interpretation I_{r} = (B_{r}, C_{r}). For B_{r} we take, for all base types b in Σ,

B_{r}(b) = T^{g}E

Formalizing the construction from the introduction, we further define, for any Σ-type τ, a pair of functions commonly called reification and reflection:

↓^{τ} ∈ [[τ]]^{I_{r}} → T^{g}E
↓^{b} = λε.ε
↓^{τ_{1}→τ_{2}} = λf.new_{τ_{1}} ⋆^{g} λv.↓^{τ_{2}} (f (↑_{τ_{1}} (η^{g} (VAR v)))) ⋆^{g} λe.η^{g} (LAM (v, e))
↑_{τ} ∈ T^{g}E → [[τ]]^{I_{r}}
↑_{b} = λε.ε
↑_{τ_{1}→τ_{2}} = λε.λa.↑_{τ_{2}} (ε ⋆^{g} λe.↓^{τ_{1}} a ⋆^{g} λe′.η^{g} (APP (e, e′)))

(It may be helpful, on a first reading, to think of T_{g} as just the identity monad, and new_{τ} as “magically” generating fresh variable names; then the reification function simplifies to precisely the construction of nf sketched in Section 1.) Finally, we define the residualizing interpretation of constants by

C_{r}(c) ∈ [[Σ(c)]]^{I_{r}}, C_{r}(c) = ↑_{Σ(c)} (η^{g} (CST c))

The normalization function. To extract the syntactic normal form from the residualizing meaning of a term, we only need to supply a starting index for name generation. We can thus define an extraction function:

nf_{τ} ∈ [[τ]]^{I_{r}} → T^{l}E, nf_{τ} = λa.withct_{E} (↓^{τ} a)

Finally, we define the (potentially partial) syntax-to-syntax function norm on closed terms ⊢_{Σ} E : τ by

norm(E) = Ẽ iff nf_{τ} ([[E]]^{I_{r}} ∅) = η^{l}^{⌜}Ẽ^{⌝}

(We can find normal forms of open terms by explicitly lambda-abstracting over their free variables. The closed-term formulation leads to a particularly natural implementation, as sketched below.)

Theorem 1 (CBN semantic normalization). Let ⊢_{Σ} E : τ be a closed Σterm. Then (0) Ẽ = norm(E) is defined, (1) ⊢^{nf} Ẽ : τ, (2) ⊧ Ẽ = E, and (3) for all ⊢_{Σ} E′ : τ such that ⊧ E′ = E, norm(E′) = Ẽ.

If we already know that any Σ-term has a unique (up to α-conversion) βηlong normal form, the proof is fairly simple, using the argument sketched in the introduction. However, it is also possible to prove the theorem directly, using a suitable Kripke logical relation between the meanings of terms in the residualizing interpretation I_{r} and in an arbitrary one I, with the base relation taken as the denotational meaning function. The details (for a more general setting, as sketched in Section 5) can be found in [11].

A normalization algorithm. The normalization function described above can be effectively computed as a program in any PCF-like functional language. The key idea is to express the residualizing semantic interpretation as a syntactic realization of all base types and constants in Σ in terms of types and terms of the programming-language signature Σ_{pl}, giving a substitution Φ_{r}, such that [[E{Φ_{r}}]]^{I_{pl}} = [[E]]^{I_{r}}. Likewise, for any Σ-type τ, we construct a term nf_{τ} such that [[nf_{τ}]]^{I_{pl}} ∅ = nf_{τ}. Then for any closed Σ-term ⊢_{Σ} E : τ, we can compute its normal form by evaluating the Σ_{pl}-program “nf_{τ} E{Φ_{r}}”. Again, the details can be found in [11].

3 Normalization by evaluation for call by value with effects

We now refine the normalization result to a language based on Moggi’s computational lambda-calculus λ_{c} [16], which provides a semantic framework for ML-like languages where “functions” may have effects such as mutating the state, performing input/output operations, or raising exceptions.

3.1 Language and semantic framework

Syntax and semantics. The syntax of types is the same as before. For terms, we also add a let-construct, with the usual typing rule:

\frac{Γ ⊢_{Σ} E_{1} : τ_{1} Γ, x: τ_{1} ⊢_{Σ} E_{2} : τ_{2}}{Γ ⊢_{Σ} let x = E_{1} in E_{2} : τ_{2}}

Now an interpretation I of a signature Σ consists a triple (B, T , C). As before, B assigns cpos to base types of Σ. The new component T = (T, η, ⋆) is a monad used to model computational effects. These could be just divergence (modeled with the lifting monad), but also state, exceptions, continuations, etc.; the actual effectful operations are invoked through suitable constants from Σ.

We need to assume that T is layered atop T_{l} [10]; this amounts to requiring that T A is pointed for any A, and that λt. t ⋆ f ∈ T A → T B is strict for any f ∈ A → T B. The CBV semantics of types is then given by:

[[b]]_{v}^{I} = B(b) [[τ_{1} → τ_{2}]]_{v}^{I} = [[τ_{1}]]_{v}^{I} → T [[τ_{2}]]_{v}^{I}

The meaning of a typing environment, [[Γ]]_{v}^{I}, is a (dom Γ)-indexed product of the meanings of the individual types, as before.

For the semantic function C, we again require that for any c ∈ dom Σ, C(c) ∈ [[Σ(c)]]_{v}^{I}. Then we define the meaning of a well-typed term Γ ⊢_{Σ} E : τ as a continuous function [[E]]_{v}^{I} ∈ [[Γ]]_{v}^{I} → T [[τ]]_{v}^{I}, as follows:

\begin{aligned}[[c]]_{v}^{I} ρ & = & η (C(c)) \\ [[x]]_{v}^{I} ρ & = & η (ρx) \end{aligned}  \begin{aligned}[[λx^{τ}.E]]_{v}^{I} ρ & = & η (λa.[[E]]_{v}^{I} (ρ[x ↦ a])) \\ [[E_{1} E_{2}]]_{v}^{I} ρ & = & [[E_{1}]]_{v}^{I} ρ ⋆ λf.[[E_{2}]]_{v}^{I} ρ ⋆ λa.f a \end{aligned}
[[let x = E_{1} in E_{2}]]_{v}^{I} ρ = [[E_{1}]]_{v}^{I} ρ ⋆ λa.[[E_{2}]]_{v}^{I} (ρ[x ↦ a])

Note that the let-construct appears redundant, because [[let x = E_{1} in E_{2}]]_{v}^{I} ρ = [[(λx.E_{2})E_{1}]]_{v}^{I} ρ, but including it enables a nicer syntactic characterization of normal forms.

Equivalence and normal forms. Analogously to the CBN case, we write ⊧_{v} E = E′ if for all I, [[E]]_{v}^{I} = [[E′]]_{v}^{I}. The shape of normal forms is now somewhat different, however: instead of normal and atomic forms, we have normal values and normal computations:

\frac{Σ(c) = b}{Γ ⊢^{nv} c : b}  \frac{Γ (x) = b}{Γ ⊢^{nv} x : b}  \frac{Γ, x: τ_{1} ⊢^{nc} E : τ_{2}}{Γ ⊢^{nv} λx^{τ_{1}}.E : τ_{1} → τ_{2}}
\frac{Γ ⊢^{nv} E : τ}{Γ ⊢^{nc} E : τ}  \frac{Σ(c) = τ_{1} → τ_{2} Γ ⊢^{nv} E : τ_{1} Γ, x: τ_{2} ⊢^{nc} E′ : τ}{Γ ⊢^{nc} let x = cE in E′ : τ}

\frac{Γ (x′) = τ_{1} → τ_{2} Γ ⊢^{nv} E : τ_{1} Γ, x: τ_{2} ⊢^{nc} E′ : τ}{Γ ⊢^{nc} let x = x′ E in E′ : τ}

That is, a normal value is either a base-typed constant or variable, or of the form λx. let x_{1} = f_{1} V_{1} in ⋯ let x_{n} = f_{n} V_{n} in V where all the V s are normal values, and each f_{i} is a function-typed constant or variable.

The set of normal-form terms is similar to Flanagan et al.’s A-normal forms [13]. However, their notion of A-reduction does not include even restricted βconversion, so a term such as (λx. x)y is already A-normal. (Nor does it include η-like let-conversions: both f x and let y = f x in y are A-normal.) A much closer match is Ohori’s language of cut-free A-normal sequent proofs [17], but still with one important difference: since we also care about uniqueness of normal forms, a variable is only a normal value in our sense if it is of base type; function-typed normal values must always be syntactic lambda-abstractions.

3.2 A normalization result

Term representations. Corresponding to the extended source syntax, we also assume given an additional constructor function LET ∈ V×E×E→E, injective and with range disjoint from the others. The representation function for terms is also extended in the obvious way.

Residualizing monad. For constructing the residualizing interpretation, we now also need to pick a residualizing monad T_{r}. It is easy to see that we cannot simply use the lifting monad here, even if we only care about “purely functional” callby-value languages, i.e., interpretations with T taken as lifting. The reason is that the two normal-form terms E_{1} = λf^{b→b}.λx^{b}.let y = f x in x and E_{2} = λf^{b→b}.λx^{b}.x are not semantically equivalent: for any I where T is the lifting monad, we only have [[E_{1}]]_{v}^{I} ⊑ [[E_{2}]]_{v}^{I} ρ (with the strictness of the inequality demonstrated by application of both sides to λa. ⊥). But ^{⌜}E_{1}^{⌝} ⋢ ^{⌜}E_{2}^{⌝}, so there can be no monotone (let alone continuous) function nf : [[(b→b)→b→b]]^{I_{r}} →E_{⊥} such that nf([[E_{1}]]^{I_{r}} ∅) = η^{l}^{⌜}E_{1}^{⌝} and nf([[E_{2}]]^{I_{r}} ∅) = η^{l}^{⌜}E_{2}^{⌝}, if we require I_{r} to use only the lifting monad to interpret computational effects.

Indeed, looking at the shape of normal computations, we see that the residualizing monad most allow us to register exactly where and when a function-typed constant or variable was applied, even if its return value is never used. We will show that it suffices that T_{r} can be equipped with operations

bind_{τ} ∈ E → T^{r}V  and  collect ∈ T^{r}E → T^{g}E

satisfying the equational constraints

collect (η^{r} e) = η^{g} e
collect (bind_{τ} e ⋆^{r} f) = new_{τ} ⋆^{g} λv.collect (f v) ⋆^{g} λe′.η^{g} (LET (v, e, e′))

These equations ensure that a T^{r}E-computation consisting of a sequence of calls to bind followed by returning a term has the effect of wrapping that term in a corresponding sequence of LET s:

collect (bind_{τ_{1}} e_{1} ⋆^{r} λv_{1}.· · · bind_{τ_{n}} (e_{n} v_{1} ⋯ v_{n−1}) ⋆^{r} λv_{n}.η^{r} (e v_{1} ⋯ v_{n})) = new_{τ_{1}} ⋆^{g} λv_{1}.· · · new_{τ_{n}} ⋆^{g} λv_{n}.η^{g} (LET (v_{1}, e_{1}, ⋯ LET (v_{n}, e_{n} v_{1} ⋯ v_{n−1}, e v_{1} ⋯ v_{n})))

To view T^{g}-computations as special cases of T^{r}-computations, we will also need a monad morphism from T_{g} to T_{r}, i.e., a collection of functions γ_{A}^{g,r} ∈ T^{g}A → T^{r}A, such that γ^{g,r} (η^{g} a) = η^{r} a and γ^{g,r} (t ⋆^{g} f) = γ^{g,r} t ⋆^{r} λa.γ^{g,r} (f a). We can construct a monad with these operations in several ways, notably including the following two:

The continuation monad with answer domain T^{g}E. We take:

T^{r}A = (A → T^{g}E) → T^{g}E_{η^{r} a = λκ.κa}_{t ⋆^{r} f = λκ.t(λa.f aκ)} γ^{g,r} t = λκ.t ⋆^{g} κ

bind_{τ} e = λκ.new_{τ} ⋆^{g} λv.κv ⋆^{g} λe′.η^{g} (LET (v, e, e′))
collect t = tη^{g}

This continuation-based wrapping of syntactic bindings was originally used for an “administrative-reduction free” continuation-passing transformation [9], and later adapted for a similar purpose in type-directed partial evaluation [7]. It is notable for also allowing an extension of CBV NBE to sum types (see Section 4).

The accumulation monad over the monoid of (V×E)-lists. Writing [] for the empty list, [−] for a singleton list, and @ for list concatenation, we take:

T^{r}A = T^{g}(A × (V × E)^{∗})
η^{r} a = η^{g} (a, [])
t ⋆^{r} f = t ⋆^{g} λ(a, l).f a ⋆^{g} λ(b, l′).η^{g} (b, l @ l′)

γ^{g,r} t = t ⋆^{g} λa.η^{g} (a, [])
bind_{τ} e = new_{τ} ⋆^{g} λv.η^{g} (v, [(v, e)])
collect t = t ⋆^{g} λ(e, l).η^{g} (wrap l e)

with the auxiliary function wrap : (V × E)^{∗} → E → E defined inductively as

wrap [] e = e wrap ([(v, e′)] @ l) e = LET (v, e′, wrap l e)

This choice is a refinement of state-based TDPE [18]; see the end of this section for a brief account of the relationship between accumulation and state. Other constructions are also possible, such as accumulation with respect to the monoid (E → E, id, ∘).

Residualizing interpretation. For the residualizing interpretation, we again interpret all base types of Σ as syntactic lambda-terms; this time, however, we do not need to involve the name-generation monad yet, but simply take:

B_{r}(b) = E

For any definition of T_{r} satisfying the equational constraints on bind and collect, we can then define new reification and reflection functions:

↓^{τ} ∈ [[τ]]_{v}^{I_{r}} → T^{g}E
↓^{b} = λe.η^{g} e
↓^{τ_{1}→τ_{2}} = λf.new_{τ_{1}} ⋆^{g} λv.collect (↑_{τ_{1}} (VAR v) ⋆^{r} λa.f a ⋆^{r} λb.γ^{g,r} (↓^{τ_{2}} b)) ⋆^{g} λe.
η^{g} (LAM (v, e))
↑_{τ} ∈ E → T^{r}[[τ]]_{v}^{I_{r}}
↑_{b} = λe.η^{r} e
↑_{τ_{1}→τ_{2}} = λe.η^{r} (λa.γ^{g,r} (↓^{τ_{1}} a) ⋆^{r} λe′.bind_{τ_{2}} (APP (e, e′)) ⋆^{r} λv.↑_{τ_{2}} (VAR v))

(The codomain of ↑_{τ} is T^{r}[[τ]]_{v}^{I_{r}}, rather than simply [[τ]]_{v}^{I_{r}}, to accommodate the extensions in Section 4.) Note in particular how every construction of an APPterm is wrapped in a bind.

Finally, as for call by name, we interpret all Σ-constants as reflected CST - constructors:

C_{r}(c) ∈ [[Σ(c)]]_{v}^{I_{r}}, C_{r}(c) = a, where ↑_{Σ(c)} (CST c) = η^{r} a

(C_{r}(c) is well defined, because the reflection function factors through the injective η^{r}.) We also define the extraction function essentially as before:

nf_{τ} ∈ [[τ]]_{v}^{I_{r}} → T^{l}E, nf_{τ} = λa. withct_{E} (↓^{τ} a)

and the CBV normalization function for a closed value (constant or lambdaabstraction) E as

norm_{v}(E) = Ẽ iff nf_{τ} a = η^{l}^{⌜}Ẽ^{⌝}, where [[E]]_{v}^{I_{r}} ∅ = η^{r} a.

(We can find the normal form of a non-value term by wrapping a dummy lambdaabstraction around it.)

Theorem 2 (CBV semantic normalization). Let ⊢_{Σ} E : τ be a value, and take Ẽ = norm_{v}(E). Then (0) Ẽ is defined, (1) ⊢^{nv} Ẽ : τ, (2) ⊧_{v} Ẽ = E, and (3) if ⊧_{v} E′ = E then norm_{v}(E′) = Ẽ.

The proof is similar to the CBN case, but using a pair of mutually inductively defined logical relations, one for values and one for computations. Very roughly, one again establishes that the residualizing and the arbitrary interpretations of all terms are related, and that for a pair of related values (a, a′) ∈ [[τ]]_{v}^{I_{r}} × [[τ]]_{v}^{I} the I-meaning of ↓^{τ} a equals a′.

A normalization algorithm. Phrasing the normalization function as a functional program is a bit more complicated than for the CBN case. A typical CBV host language will have its own notion of effects, modeled by some monad T_{pl}, which is not likely to be exactly our residualizing monad T_{r}. However, much as we can embed the normalization algorithm into a host language with a signature much larger than what we need for the construction, we can realize both the residualizing and the name-generating monad through a uniform effect-embedding into a more general notion of effect in the host language [10].

For example, the accumulation-based choice of T_{r} can be easily (and more efficiently) implemented by passing around the bindings accumulated so far in a mutable state cell, rather than appending the bindings from both subcomputations in ⋆. The current name-generation index is naturally kept in another cell. An analogous, but somewhat more involved, construction also allows us to simulate T_{r} taken as a continuation monad, provided the host language provides both (higher-typed) state and first-class continuations, as found in Scheme or SML/NJ. The resulting implementation forms the basis of the CBV normalization algorithm used in the context of type-directed partial evaluation [7].

4 Structured data types

In this section, we consider normalization for the call-by-value language extended with product and sum types. (Adding products to the call-by-name language is trivial, but it does not appear possible to add even weak sum types, at least in the domain-theoretic semantics.)

Syntax. We extend the set of types by two new type constructors:

τ ::= ⋯ | τ_{1} × τ_{2} | τ_{1} + τ_{2}

(The generalizations to n-ary (n ≥ 0) products and sums are completely straightforward and thus omitted.) The associated new terms are:

\frac{Γ ⊢_{Σ} E_{1} : τ_{1} Γ ⊢_{Σ} E_{2} : τ_{2}}{Γ ⊢_{Σ} (E_{1}, E_{2}) : τ_{1} × τ_{2}}  \frac{Γ ⊢_{Σ} E : τ_{1} × τ_{2} Γ, x_{1}: τ_{1}, x_{2}: τ_{2} ⊢_{Σ} E′ : τ}{Γ ⊢_{Σ} split(E, x_{1}. x_{2}. E′) : τ}
\frac{Γ ⊢_{Σ} E : τ_{1}}{Γ ⊢_{Σ} inl(E) : τ_{1} + τ_{2}}  \frac{Γ ⊢_{Σ} E : τ_{2}}{Γ ⊢_{Σ} inr(E) : τ_{1} + τ_{2}}

\frac{Γ ⊢_{Σ} E : τ_{1} + τ_{2} Γ, x_{1}: τ_{1} ⊢_{Σ} E_{1} : τ Γ, x_{2}: τ_{2} ⊢_{Σ} E_{2} : τ}{Γ ⊢_{Σ} case(E, x_{1}. E_{1}, x_{2}. E_{2}) : τ}

(Instead of split, we could have used explicit projections, but the characterization of normal forms becomes more uniform with split. In practice, the separate split-construct above is usually folded into pattern-matching let- and lambdabindings.)

Semantics. The semantics of the type constructors is standard:

[[τ_{1} × τ_{2}]]_{v}^{I} = [[τ_{1}]]_{v}^{I} × [[τ_{2}]]_{v}^{I} = {(a_{1}, a_{2}) | a_{1} ∈ [[τ_{1}]]_{v}^{I}, a_{2} ∈ [[τ_{1}]]_{v}^{I}}
[[τ_{1} + τ_{2}]]_{v}^{I} = [[τ_{1}]]_{v}^{I} + [[τ_{2}]]_{v}^{I} = {ι_{1} a | a ∈ [[τ_{1}]]_{v}^{I}} ∪ {ι_{2} a | a ∈ [[τ_{2}]]_{v}^{I}}

as is the semantics of the associated terms:

[[(E_{1}, E_{2})]]_{v}^{I} ρ = [[E_{1}]]_{v}^{I} ρ ⋆ λa_{1}.[[E_{2}]]_{v}^{I} ρ ⋆ λa_{2}.η (a_{1}, a_{2})
[[split(E, x_{1}. x_{2}. E′)]]_{v}^{I} ρ = [[E]]_{v}^{I} ρ ⋆ λ(a_{1}, a_{2}).[[E′]]_{v}^{I} (ρ[x_{1} ↦ a_{1}, x_{2} ↦ a_{2}])

[[inl(E)]]_{v}^{I} ρ = [[E]]_{v}^{I} ρ ⋆ λa.η (ι_{1} a)
[[inr(E)]]_{v}^{I} ρ = [[E]]_{v}^{I} ρ ⋆ λa.η (ι_{2} a)
[[case(E, x_{1}. E_{1}, x_{2}. E_{2})]]_{v}^{I} ρ = [[E]]_{v}^{I} ρ ⋆ λs.\{ \begin{matrix}[[E_{1}]]_{v}^{I} (ρ[x_{1} ↦ a_{1}]) & if s = ι_{1} a_{1} \\ [[E_{2}]]_{v}^{I} (ρ[x_{2} ↦ a_{2}]) & if s = ι_{2} a_{2} \end{matrix}

Normal forms. With the addition of product and sum types, CBV normal forms exhibit a striking similarity with cut-free proofs in Gentzen-style intuitionistic sequent calculus, as also noted by Ohori [17]. In fact, we also get the usual sequent-calculus inconvenience of having to make arbitrary choices about the order in which we apply left-rules to decompose the types of variables. To keep normal forms unique, we choose to eliminate structured-type variables immediately as they are introduced, in a stack-like manner. (Immediate elimination leads to a slight anomaly for constants introduced by the signature: we can only allow Σ to declare constants of base and top-level-functional types. In the rare cases where we need, e.g., a sum-typed constant c : τ_{1} + τ_{2} in Σ, it can be provided as a function c′ : 1 → τ_{1} + τ_{2} where 1 is the zero-ary product type.)

We now have three mutually recursive notions of normality: normal values Γ ⊢^{nv} E : τ, normal computations Γ ⊢^{nc} E : τ, and normal bodies Γ | Θ ⊢^{nb} E : τ, where Θ is an ordered list of typing assumptions:

\frac{Σ(c) = b}{Γ ⊢^{nv} c : b}  \frac{Γ (x) = b}{Γ ⊢^{nv} x : b}  \frac{Γ | x: τ_{1} ⊢^{nb} E : τ_{2}}{Γ ⊢^{nv} λx^{τ_{1}}.E : τ_{1} → τ_{2}}

\frac{Γ ⊢^{nv} E_{1} : τ_{1} Γ ⊢^{nv} E_{2} : τ_{2}}{Γ ⊢^{nv} (E_{1}, E_{2}) : τ_{1} × τ_{2}}  \frac{Γ ⊢^{nv} E : τ_{1}}{Γ ⊢^{nv} inl(E) : τ_{1} + τ_{2}}  \frac{Γ ⊢^{nv} E : τ_{2}}{Γ ⊢^{nv} inr(E) : τ_{1} + τ_{2}}
\frac{Γ ⊢^{nv} E : τ}{Γ ⊢^{nc} E : τ}  \frac{Σ(c) = τ_{1} → τ_{2} Γ ⊢^{nv} E : τ_{1} Γ | x: τ_{2} ⊢^{nb} E′ : τ}{Γ ⊢^{nc} let x = cE in E′ : τ}

\frac{Γ (x′) = τ_{1} → τ_{2} Γ ⊢^{nv} E : τ_{1} Γ | x: τ_{2} ⊢^{nb} E′ : τ}{Γ ⊢^{nc} let x = x′ E in E′ : τ}

\frac{Γ ⊢^{nc} E : τ}{Γ | ⊢^{nb} E : τ}  \frac{Γ, x: b | Θ ⊢^{nb} E : τ}{Γ | Θ, x: b ⊢^{nb} E : τ}  \frac{Γ, x: τ_{1} → τ_{2} | Θ ⊢^{nb} E : τ}{Γ | Θ, x: τ_{1} → τ_{2} ⊢^{nb} E : τ}
\frac{Γ | Θ, x_{1}: τ_{1}, x_{2}: τ_{2} ⊢^{nb} E : τ}{Γ | Θ, x: τ_{1}×τ_{2} ⊢^{nb} split(x, x_{1}. x_{2}. E) : τ} \frac{Γ | Θ, x_{1}: τ_{1} ⊢^{nb} E_{1} : τ Γ | Θ, x_{2}: τ_{2} ⊢^{nb} E_{2} : τ}{Γ | Θ, x: τ_{1}+τ_{2} ⊢^{nb} case(x, x_{1}. E_{1}, x_{2}. E_{2}) : τ}

Note how newly-introduced variables are put into the quarantined context Θ, where their types are decomposed and the pieces migrate back into the ordinary context Γ. In particular, without the rules for product and sum types, the new definitions of normal values and computations agree exactly with the original ones.

Normalization by evaluation. We show only how the continuation-based residualizing interpretation can be extended. Products could be added to an accumulationbased interpretation without too much trouble, but sums apparently require the full power of applying a single continuation multiple times.

We assume the syntax-constructor functions for E are extended with functions PAIR, SPLIT , INL, INR, and CASE with the obvious types. Then we can define additional helper functions analogous to bind_{τ} from before:

bindp_{τ_{1},τ_{2}} ∈ E → T^{r}(V × V)

= λe.λκ.new_{τ_{1}} ⋆^{g} λv_{1}.new_{τ_{2}} ⋆^{g} λv_{2}.κ(v_{1}, v_{2}) ⋆^{g} λe′.η^{g} (SPLIT (e, v_{1}, v_{2}, e′))

binds_{τ_{1},τ_{2}} ∈ E → T^{r}(V + V)
= λe.λκ.new_{τ_{1}} ⋆^{g} λv_{1}.new_{τ_{2}} ⋆^{g} λv_{2}.κ(ι_{1} v_{1}) ⋆^{g} λe_{1}.κ(ι_{2} v_{2}) ⋆^{g} λe_{2}.
η^{g} (CASE (e, v_{1}, e_{1}, v_{2}, e_{2}))

and the corresponding cases for the reification and reflection functions, extending the ones from Section 2.2:

↓^{τ_{1}×τ_{2}} = λ(a_{1}, a_{2}).↓^{τ_{1}} a_{1} ⋆^{g} λe_{1}.↓^{τ_{2}} a_{2} ⋆^{g} λe_{2}.η^{g} (PAIR (e_{1}, e_{2}))
↓^{τ_{1}+τ_{2}} = λs.\{ \begin{matrix}↓^{τ_{1}} a_{1} ⋆^{g} λe_{1}.η^{g} (INLe_{1}) & if s = ι_{1} a_{1} \\ ↓^{τ_{2}} a_{2} ⋆^{g} λe_{2}.η^{g} (INR e_{2}) & if s = ι_{2} a_{2} \end{matrix}
↑_{τ_{1}×τ_{2}} = λe.bindp_{τ_{1},τ_{2}} e ⋆^{r} λ(v_{1}, v_{2}).↑_{τ_{1}} (VAR v_{1}) ⋆^{r} λa_{1}.↑_{τ_{2}} (VAR v_{2}) ⋆^{r} λa_{2}.η^{r} (a_{1}, a_{2})
↑_{τ_{1}+τ_{2}} = λe.binds_{τ_{1},τ_{2}} e ⋆^{r} λs.\{ \begin{matrix}↑_{τ_{1}} (VAR v_{1}) & if s = ι_{1} v_{1} \\ ↑_{τ_{2}} (VAR v_{2}) & if s = ι_{2} v_{2} \end{matrix}

The residualizing interpretation is as before. (Note that we cannot give a residualizing interpretation to constants of top-level product or sum type, since the reflection function does not factor through η^{r} in these cases.) The normalization function and Theorem 2 remain the same. For the implementation, the realizations of bindp, binds, and the new clauses for reification and reflection in terms of continuation-manipulating primitives are straightforward.

5 Type-directed partial evaluation

A primary application of normalization by evaluation is for type-directed partial evaluation (TDPE) [7]. The goal is to simplify a partially applied function of multiple arguments by propagating the values of the known arguments throughout the body of the function. Here, in addition to eliminating β-redexes, we also want to simplify occurrences of constants, such as arithmetic operations, when they are applied to literal values. In other words, we now want to normalize terms with interpreted base types and constants. There are in fact two natural ways to achieve this, both expressible in terms of the notion of constrained interpretations:

Offline TDPE. For offline TDPE [7, Section 3], we say that a program is bindingtime separated if it is expressed over a signature Σ partitioned into a static and a dynamic part, Σ_{s} and Σ_{d}, each containing some type and term constants. The interpretation is likewise partitioned into I_{s} and I_{d}. We then constrain the allowable interpretations so that I_{s} is always the standard interpretation (i.e., int as Z, + as addition, fix as the domain-theoretic least fixed point, etc.), while the dynamic part remains completely unconstrained. That is, we consider the notion of static equivalence, ⊧^{Int^{s}} E = E′ where Int_{s} = {I | I|_{Σ_{s}} = I_{s}}. When the static normal form Ẽ of a term E exists, it is then equivalent to E with respect to all interpretations of Σ_{d}. The residualizing interpretation of Σ, like any interpretation in Int_{s}, also uses the standard interpretation of Σ_{s}, and the syntax-reconstructing interpretation from Section 3.2 for I_{d}.

The separation allows us to realize the static part of the signature completely natively in terms of the corresponding construct of the programming language, and in fact we can use syntactic conveniences of the host language, such as pattern matching or letrec-forms directly for the static computations. It also becomes possible to self-apply the partial evaluator (the so-called second Futamura projection) [15].

Online TDPE. In the online variant [7, Section 4], like in general online partial evaluation, we do not annotate types, nor most occurrences of constants, with their binding times. Instead, the partial evaluator “opportunistically” propagates statically known data and performs reductions such as 2 + 3 → 5.

This corresponds to normalizing with respect to the set Int_{c} of interpretations (B, C) that satisfy constraints such as C(+) (C(2), C(3)) = C(5), and possibly also additional ones, such as C(+) (x, C(0)) = x for all x in B(int). Again, the standard interpretation of C(+) satisfies these constraints automatically. The residualizing one includes explicit checks for the reducible cases, to avoid constructing the corresponding redexes in the generated code. This formulation is similar to recent work on merging the reduction-free normalization of function abstraction and application with explicit reduction rules for constants [3].

The advantage of the online approach is that we do not have to explicitly separate the binding times in the source program, but correspondingly it becomes less predictable how much of the source program can be simplified at partialevaluation time. An online normalizer also requires all primitive operations to explicitly check whether their arguments are literals (so the operation can be eliminated) or more general expressions (so the operation must remain in the normal form), slowing down the specialization process somewhat. Finally, fixedpoint operators must still either be explicitly classified as static or dynamic, or need some ad hoc mechanism for deciding whether their unfolding equation should be applied.

In both cases, the normalization function may be partial, i.e., without part (0) of Theorems 1 and 2. This is unavoidable, since in the presence of recursion, some terms simply have no normal form. However, for the CBN case, one can still show that when it is defined, Ẽ satisfies parts (1-3), and also that whenever a Ẽ satisfying (1-3) exists, norm(E) is defined [11]. The situation for CBV TDPE has not been fully analyzed yet, although it seems reasonable to conjecture an analogous result.

In any case, the semantic treatment of TDPE allows us to uniformly analyze the construction and state its correctness criterion independently of the details of its implementation. That is, we can think about partial evaluation in terms of normalization with respect to a class of interpretations, without worrying about whether the normalization is achieved through repeated reductions, or through reduction-less normalization by evaluation.

6 Conclusions and future work

We have seen that the same basic idea that allows us to compute normal forms of lambda-terms with respect to purely functional interpretations also allows us to compute such normal forms with respect to general computational interpretations. In both cases, we chose a “quasi-syntactic” interpretation of the types and constants, and in the latter, also a binding-accumulating monad as the interpretation of computational effects. Both variants of semantic normalization can be phrased as functional-program evaluation, although the construction is significantly more involved in the computational case.

An important application of the normalization construction is type-directed partial evaluation, which seeks to compute normal forms not with respect to all interpretations of a signature, but only with respect to a subset of those; different choices of such subsets lead to offline and online partial evaluation. The offline, call-by-name case is analyzed in isolation in an earlier paper [11], but the more general constrained-interpretation formulation presented here seems worth investigating further, especially since it also leads to natural TDPE formulations of other partial-evaluation concepts, such as polyvariant program-point specialization expressed as suitable constraints on the recursion operator.

Additionally, it should be possible to obtain a syntactic analog of the CBV normalization result, showing that the computed normal form is not only equivalent to the original term with respect to arbitrary set-, or domain-theoretic interpretations, but is provably equal to it using the axioms of the computational lambda-calculus [16]. However, it seems that the semantic characterization may be ultimately more convenient for reasoning about programs, since it seems to scale more directly to partially constrained interpretations, and especially static recursion.

Acknowledgments

The author wishes to thank Olivier Danvy and Peter Dybjer for many fruitful discussions of the topics presented here, and the anonymous TLCA’01 reviewers for numerous helpful suggestions (of which regrettably not all could be followed here, due to space constraints.)

References

1. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science, 6th International Conference, number 953 in Lecture Notes in Computer Science, 1995.

2. Ulrich Berger. Program extraction from normalization proofs. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pages 91–106, Utrecht, The Netherlands, March 1993.

3. Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. In Prospects for Hardware Foundations (NADA), number 1546 in Lecture Notes in Computer Science, pages 117–137, 1998.

4. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203–211, Amsterdam, The Netherlands, July 1991.

5. Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:75–94, 1997.

6. Djordje Čubrić, Peter Dybjer, and Philip Scott. Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8:153–192, 1998.

7. Olivier Danvy. Type-directed partial evaluation. In J. Hatcliff, T. Æ. Mogensen, and P. Thieman, editors, Partial Evaluation – Practice and Theory; Proceedings of the 1998 DIKU Summer School, number 1706 in Lecture Notes in Computer Science, pages 367–411. Springer-Verlag, Copenhagen, Denmark, July 1998.

8. Olivier Danvy and Peter Dybjer, editors. Preliminary Proceedings of the APPSEM Workshop on Normalization by Evaluation. Department of Computer Science, University of Aarhus, May 1998. BRICS Note NS-98-1.

9. Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

10. Andrzej Filinski. Representing layered monads. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 175–188, San Antonio, Texas, January 1999.

11. Andrzej Filinski. A semantic account of type-directed partial evaluation. In G. Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, number 1702 in Lecture Notes in Computer Science, pages 378–395, Paris, France, September 1999.

12. Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, pages 193–202, Trento, Italy, July 1999.

13. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the SIGPLAN ’93 Conference on Programming Language Design and Implementation, pages 237–247, Albuquerque, New Mexico, June 1993.

14. Murdoch Gabbay and Andrew Pitts. A new approach to abstract syntax involving binders. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, pages 214–224, Trento, Italy, July 1999.

15. Bernd Grobauer and Zhe Yang. The second Futamura projection for type-directed partial evaluation. In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 22–32. ACM Press, January 2000.

16. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 14–23, Pacific Grove, California, June 1989. IEEE.

17. Atsushi Ohori. A Curry-Howard isomorphism for compilation and program execution. In J.-Y. Girard, editor, Typed Lambda-Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, L’Aquila, Italy, April 1999.

18. Eijiro Sumii and Naoki Kobayashi. Online-and-offline partial evaluation: A mixed approach. In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 12–21. ACM Press, January 2000.