A Denotational Account of Untyped Normalization by Evaluation^{⋆}

Andrzej Filinski^{1} and Henning Korsholm Rohde^{2}

1 DIKU, University of Copenhagen, Denmark; email: andrzej@diku.dk 2 BRICS^{⋆⋆}, University of Aarhus, Denmark; email: hense@brics.dk

Abstract. We show that the standard normalization-by-evaluation construction for the simply-typed λ_{βη}-calculus has a natural counterpart for the untyped λ_{β}-calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computationaladequacy argument for an untyped, call-by-name language to normalization instead of evaluation. In the untyped setting, not all terms have normal forms, so the normalization function is necessarily partial. We establish its correctness in the senses of soundness (the output term, if any, is β-equivalent to the input term); standardization (β-equivalent terms are mapped to the same result); and completeness (the function is defined for all terms that do have normal forms). We also show how the semantic construction enables a simple yet formal correctness proof for the normalization algorithm, expressed as a functional program in an ML-like call-by-value language.

1 Introduction

1.1 Reduction-Based and Reduction-Free Normalization

Traditional accounts of term normalization are based on a directed notion of reduction (such as β-reduction), which can be applied anywhere within a term. A term is said to be a normal form if no reductions can be performed on it. If the reduction relation is confluent, normal forms are uniquely determined, so normalization is a (potentially partial) function on terms. Some terms (such as Ω) may not have normal forms at all; or a particular reduction strategy (such as normal-order reduction) may be required to guarantee arrival at a normal form when one exists; such a strategy is called complete. There is a very large body of work dealing with normalization in reduction-based settings.

However, in recent years, a rather different notion of normalization has emerged, so-called reduction-free normalization. As the name suggests, it is not based on a directed notion of reduction, but rather on an undirected notion of

⋆ A version of this article with detailed proofs is available as a technical report [5].

⋆⋆

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

term equivalence. Equivalence may be defined as simply the reflexive-transitive-symmetric closure of an existing reduction relation, but it does not have to be: any congruence relation on terms may be used. The task of normalization is then to define a normalization function on terms, such that the output of the function is equivalent to the input, and such that any two equivalent terms are mapped to identical outputs [3].

For some notions of equivalence (such as β-convertibility of untyped lambdaterms), it is actually impossible to define a computable, total normalization function with both of these properties; we must thus accept that the normalization function may be partial. However, even in that case, we can impose a completeness constraint: if we have an independent syntactic characterization of acceptable normal forms, we can require that the function both produce terms in this form as output, and that it be defined on all terms equivalent to a normal form.

1.2 Normalization by Evaluation

A particularly natural way of obtaining a reduction-free normalization function is known as normalization by evaluation (NBE), based on the following idea: Suppose we can construct a denotational model of the term syntax (i.e., such that equivalent terms have the same denotation), with the property that a syntactic representation of the term (up to equivalence) can be be extracted from its denotation; such a model is called residualizing. Then the normalization function can be expressed simply as a (compositional) interpretation in the model, followed by extraction.

A priori, such a normalization function is not necessarily effectively computable. It can be given a computational interpretation if the denotational model is constructed in intuitionistic set theory [3], but this gets somewhat complicated for domain-theoretic models, especially those involving reflexive domains. In such cases, it is often easier to establish that the constructions are effective by showing that they can expressed as images of program terms in a language for which the domain-theoretic semantics is already known to be computationally adequate.

(It should be noted that the term NBE is also sometimes used for a related concept, based on reducing – usually in a compositional way – the normalization problem, which may in general involve open terms of higher type, to an evaluation problem, which involves normalization of only closed terms of base type. The required transformation is often syntactically related to the model-based construction above, but the model itself is not made explicit; and in fact, the subsequent evaluation process may still be specified entirely in terms of reductions.)

1.3 The Berger-Schwichtenberg Normalization Algorithm

Perhaps the best-known NBE algorithm is due to Berger and Schwichtenberg [2]. It finds βη-long normal forms of simply-typed λ-terms. We present here its outline, glossing over inessential details.

Types are of the form τ ::= b | τ_{1} → τ_{2}. A natural set-theoretic model interprets each base type b as some set, and the function type as the set of all functions between the interpretations of the types, i.e., [[τ_{1} → τ_{2}]] = [[τ_{1}]] → [[τ_{2}]]. For a type assignment Γ, we also take [[Γ]] = ∏_{x∈dom Γ} [[Γ (x)]].

Let Λ be the set of syntactic λ-terms (written with explicit constructors for emphasis) over a set of variables V. For a well-typed term Γ ⊢ m : τ, we can then express its semantics [[m]] ∈ [[Γ]] → [[τ]] as follows:

[[VAR(x)]] ρ = ρ(x)
[[LAM(x^{τ} , m_{0})]] ρ = λa^{[[τ]]}. [[m_{0}]] ρ[x ↦ a]
[[APP(m_{1}, m_{2})]] ρ = [[m_{1}]] ρ ([[m_{2}]] ρ)

It is easy to check that such a model is sound for conversion, i.e., that when m ↔_{βη} m′, then [[m]] = [[m′]].

Consider now a model where all base types are interpreted as the set of (open) syntactic λ-terms, i.e., [[b]] = Λ for all b. In this model, we can define a pair of type-indexed function families: reification, ↓^{τ} : [[τ]] → Λ, and reflection, ↑^{τ} : Λ → [[τ]], by mutual induction on types:

↓^{b} l = l
↓^{τ_{1}→τ_{2}} f = LAM(x^{τ_{1}}, ↓^{τ_{2}} (f(↑^{τ_{1}} VAR(x)))) (where x is chosen “fresh”)
↑^{b} l = l
↑^{τ_{1}→τ_{2}} l = λa^{[[τ_{1}]]}. ↑^{τ_{2}} (APP(l, ↓^{τ_{1}} a))

For simplicity, let us only consider normal forms of closed terms. Then reification can serve directly as an extraction function: one can check that, for a term ⊢ m : τ in βη-long normal form, ↓^{τ} ([[m]] ∅) ↔_{α} m. Hence, by soundness of the model, for any term m′ with m′ ↔_{βη} m, ↓^{τ} ([[m′]] ∅) = ↓^{τ} ([[m]] ∅) ↔_{α} m ↔_{βη} m′. Alternatively, one can show the latter property directly, for an arbitrary m′. Either way, the typical proof ultimately involves a logical-relations argument, even if this argument is pushed entirely into a standard result about the syntax (namely, that every well-typed term has a βη-long normal form). The latter approach, however, generalizes better, especially to systems where not all terms have normal forms.

1.4 A Tentative Algorithm for Untyped Terms

In an untyped (or, more accurately, unityped) setting, we may hope to get a residualizing model by interpreting the single type of terms as a domain D = Λ + (D → D). (Again, we gloss over domain-theoretic subtleties for expository purposes.) We can then define variants of reification, ↓ : D → Λ, and reflection, ↑ : Λ → D, roughly analogous to the simply-typed case:

↓ d = case d of \begin{cases}in_{1}(l) & → l \\ in_{2}(f) & → LAM(x, ↓ (f(↑ VAR(x)))) (x “fresh”) \end{cases}
↑ l = in_{1}(l)

Note that reification is now defined by general recursion, rather than induction. We can also construct an interpretation, [[m]] ∈ (V → D) → D, by

[[VAR(x)]] ρ = ρ(x)
[[LAM(x, m_{0})]] ρ = in_{2}(λd. [[m_{0}]] ρ[x ↦ d])
[[APP(m_{1}, m_{2})]] ρ = case [[m_{1}]] ρ of \begin{cases}in_{1}(l) & → ↑ (APP(l, ↓ ([[m_{2}]] ρ))) \\ in_{2}(f) & → f ([[m_{2}]] ρ) \end{cases}

Here, reflection is performed “on demand”: when application needs a semantic function, but [[m_{1}]]ρ is a piece of syntax, it is reflected just enough to allow the application to be performed.

Again, it can be checked that β-convertible terms have the same denotation. It is also fairly easy to verify that, for a closed m in β-normal form, ↓ ([[m]] ∅) ↔_{α} m. What is not obvious at all, however, is that when ↓ ([[m′]] ∅) = m for a general m′, then m′ must be syntactically β-convertible to a normal form. Indeed, the problem is a generalization of the usual computational-adequacy problem for a denotational semantics of a functional language: if the denotation of a closed term is not ⊥, must the term then evaluate to a value?

For a simply typed language, PCF, adequacy of the natural domain-theoretic semantics was shown by Plotkin, using a logical-relations argument [8]. Pitts showed that essentially the same argument applies to an untyped language, except that the central relation is no longer constructed by induction on types, but as a solution of a more general “relation equation”; he also showed a general method for solving such equations, yielding invariant relations [6].

In this paper, we first formalize the construction of the normalization function from above, addressing especially the issues of potential divergence and generation of fresh variable names (Section 2). We then show correctness of this function by a generalized computational-adequacy construction (Section 3). Finally, we show how the domain-theoretic analysis directly validates a functional program implementing the construction (Section 4).

1.5 Related Work

The closest related work to ours is probably the NBE-based (in the alternate sense) algorithm for untyped β-normalization proposed by Aehlig and Joachimski [1]. However, while the functional programs ultimately derived from the analyses are quite similar, the correctness arguments are completely different: theirs are based entirely on syntactic concepts and results from higher-order rewriting theory, rather than on the domain-theoretic constructions underlying ours. In particular, their algorithm is very explicitly reduction-based, departing from the original meaning of NBE as term extraction from a denotational model of a conversion relation.

We believe that the domain-theoretic approach enables a more direct and precise correctness proof for the normalizer, as actually implemented. In Aehlig and Joachimski’s work, the abstract algorithm is expressed as a small-step operational semantics for a specialized, two-level λ-calculus with named bound variables; yet the actual normalization program is expressed as a compositional interpreter in Haskell, using de Bruijn indices for bound variables, and a reflexive type for the meanings of higher-typed terms. No connection is made to a formal semantics (operational or otherwise) of the relevant Haskell fragment. While it may well be possible to formally close this gap, it remains as a potentially major undertaking. On the other hand, formally relating the domain-theoretic constructions in the model-based normalizer to the functional terms implementing them is completely straightforward. We expect, but have not formally investigated, that Aehlig and Joachimski’s interesting extensions of the basic algorithm to infinite normal forms (Böhm trees) could also be expressed naturally in the denotational setting, and be used to validate a functional program producing such normal forms lazily.

Many of the constructions in the present paper are inspired by the first author’s work on type-directed partial evaluation [4]. Apart from the obvious differences arising from typed vs. untyped languages, a significant change is also that the TDPE work considered equivalence defined semantically (equality of denotations for all interpretations of “dynamic” constants), while here we consider syntactic β-convertibility. Accordingly, the central invariant relation ties denotations to syntactic terms, rather than to denotations in another semantics.

Essentially the same program as in Section 4, but expressed in FreshML, can be found in a recent paper by Shinwell et al. [9, Figure 7]. However, the focus there is on a practical application of fresh-name generation, rather than on normalization as such. Indeed, the underlying algorithm is only informally attributed to Coquand, and carries no formal correctness argument. In the present work, generation of fresh names is handled explicitly: since constructed output terms are never subsequently analyzed, using a general framework such as FreshML, or higher-order abstract syntax, is probably overkill. However, we anticipate that a different “back end” for output generation could be used, and have deliberately tried to keep the constructions and proofs modular with respect to the term-generation operations. We thus expect that essentially the same arguments – perhaps even a little simplified – could be used to verify correctness of the FreshML variant of the normalizer as well.

2 A Semantic Normalization Construction

2.1 Syntax and Semantics of the Untyped λ-Calculus

Syntax Let V be a countably infinite set of (object) variables, with x and v ranging over V. Let Λ be the set of λ-terms defined by

m ::= VAR(x) | LAM(x, m_{0}) | APP(m_{1}, m_{2})

The set of free variables of a term, F V (m), is defined in the usual way. For any finite set of variables Δ, we write Λ^{Δ} for the set of λ-terms over Δ, i.e.,

Λ^{Δ} = {m ∈ Λ | F V (m) ⊆ Δ}

Substitutions For technical reasons, we take simultaneous (as opposed to singlevariable), capture-avoiding substitution as the basic concept. Accordingly, we say that a substitution θ is a finite partial function from variables to terms. We take F V (θ) = ⋃_{x∈dom θ} F V (θ(x)), and define the action of θ on a term m in the usual way, by structural induction on m:

VAR(x)[θ] = \{ \begin{matrix}θ(x) & if x ∈ dom θ \\ VAR(x) & otherwise \end{matrix}
LAM(x, m_{0})[θ] = LAM(x′, m_{0}[θ[x ↦ VAR(x′)]])
where x′ ∉ F V (θ) ∪ (F V (m_{0})\{x})
APP(m_{1}, m_{2})[θ] = APP(m_{1}[θ], m_{2}[θ])

As a special case, we use the standard notation m[m′/x] to mean m[ [x ↦ m′] ]. To keep the substitution operation deterministic, we assume that the x′ in the LAM-clause is picked as some fixed but arbitrary function of the (finite) set of variables it needs to avoid.

Conversion and normalization We define convertibility between λ-terms, written m ↔ m′, by the axiom schemas for α- and β-conversion,

LAM(x, m) ↔ LAM(x′, m[x′/x]) (x′ ∉ F V (m)\{x})
APP(LAM(x, m), m′) ↔ m[m′/x]

together with the standard equivalence and compatibility rules, making ↔ into a congruence relation on terms. We further define atomic (also known as neutral) and normal forms, as follows:

\overline{⊢_{at} VAR(x)}  \frac{⊢_{at} m_{1} ⊢_{nf} m_{2}}{⊢_{at} APP(m_{1}, m_{2})}  \frac{⊢_{at} m}{⊢_{nf} m}  \frac{⊢_{nf} m_{0}}{⊢_{nf} LAM(x, m_{0})}

We then expect a normalization function on terms to satisfy that the output, if any, is in normal form and convertible to the input (soundness); convertible terms either give the same output, or neither one does (standardization); and if a term has a normal form at all, the normalization function will return one (completeness).

Semantics A natural way of defining a denotational model of convertibility is in terms of a reflexive pointed cpo D. Reflexivity means that the continuousfunction space [D→D] is a retract of D, i.e., that there exist continuous functions

ϕ : [D → D] → D and ψ : D → [D → D] ,

such that ψ ∘ ϕ = id_{[D→D]}. The induced interpretation, [[m]] ∈ [[V → D] → D], is then:

[[VAR(x)]] ρ = ρ(x)
[[LAM(x, m_{0})]] ρ = ϕ(λd^{D}. [[m_{0}]] ρ[x ↦ d])
[[APP(m_{1}, m_{2})]] ρ = ψ([[m_{1}]] ρ) ([[m_{2}]] ρ)

Lemma 1. The interpretation has two expectable properties:

a. If ∀x ∈ F V (m). ρ(x) = ρ′(x), then [[m]] ρ = [[m]] ρ′. b. Let θ = [x_{1} ↦ m_{1}, …, x_{n} ↦ m_{n}] be a substitution.

Then [[m[θ]]] ρ = [[m]] ρ[x_{1} ↦ [[m_{1}]] ρ, …, x_{n} ↦ [[m_{n}]] ρ].

Proof. Part (a) is a straightforward induction on the structure of m. Part (b) follows by induction on the structure of m, using part (a) in the LAM-case.

Lemma 2 (model soundness). If m ↔ m′ then [[m]] = [[m′]]

Proof. By induction on the derivation of m ↔ m′, using Lemma 1 for α- and β-conversion, and using that ψ ∘ ϕ = id_{[D→D]} for β-conversion.

2.2 Output-Term Generation

We want to account rigorously for the generation of fresh names, and do so in a modular manner. We will therefore construct a set Λ̂ (dependent on the name generation scheme) with elements denoted by l, together with wrapper functions,

{ \atop VAR} : V → Λ̂, { \atop LAM} : [V → Λ̂] → Λ̂, { \atop APP} : Λ̂× Λ̂ → Λ̂

where, in particular, { \atop LAM} provides a fresh name to be used in constructing the body of the λ-abstraction.

Let N be a set (discrete cpo) containing at least the natural numbers, with an operation · + 1 : N → N, agreeing with the successor operation on naturals. Let {g_{0}, g_{1}, ...} be a countably infinite subset of V, such that g_{i} = g_{j} implies i = j, and let gen : N → V be such that gen(n) = g_{n} when n ∈ ℕ.

We write ⌊·⌋ for the inclusion from A to A_{⊥}; and for f : A → B with B pointed, we write · ⋆ f for f’s strict extension to A_{⊥}, i.e., ⊥ ⋆ f = ⊥_{B} and ⌊a⌋ ⋆ f = f a. We then take Λ̂ = [N → Λ_{⊥}] and define wrapper functions for constructing λ-terms using de Bruijn-level (not -index!) naming as follows:

{ \atop VAR}(v) = λn^{N} . ⌊VAR(v)⌋
{ \atop LAM}(f) = λn^{N} . f gen(n) (n + 1) ⋆ λm_{0}^{Λ}. ⌊LAM(gen(n), m_{0})⌋
{ \atop APP}(l_{1}, l_{2}) = λn^{N} . l_{1} n ⋆ λm_{1}^{Λ}. l_{2} n ⋆ λm_{2}^{Λ}. ⌊APP(m_{1}, m_{2})⌋

Note 1. If we took freshness as a primitive concept, like in FreshML, we could simply use Λ̂ = Λ_{⊥}; { \atop VAR}(v) = ⌊VAR(v)⌋; { \atop LAM}(f) = f x ⋆ λm_{0}. ⌊LAM(x, m_{0})⌋,

with x fresh for f; and { \atop APP}(l_{1}, l_{2}) = l_{1} ⋆ λm_{1}. l_{2} ⋆ λm_{2}. ⌊APP(m_{1}, m_{2})⌋.

2.3 A Residualizing Model

From standard domain-theoretic results (e.g., [6]), we know that there exists a pointed cpo D_{r}, together with an isomorphism

i : D_{r} →^{≅} (Λ̂+ [D_{r} → D_{r}])_{⊥}

Moreover, this solution is a so-called minimal invariant, which we will need in the next section.

We first define the reification function ↑ : Λ̂ → D_{r} and reflection function ↓ : D_{r} → Λ̂, as follows:

↓ d = case i(d) of \begin{cases}⌊in_{1}(l)⌋ & → l \\ ⌊in_{2}(f)⌋ & → { \atop LAM}(λx^{V} . ↓ (f(↑ { \atop VAR}(x)))) \\ ⊥ & → ⊥Λ̂ \end{cases}
↑ l = i^{−1}(⌊in_{1}(l)⌋)

where the recursive definition of ↓ is interpreted in the usual least-fixed-point sense. Using these, we construct appropriate functions ϕ_{r} : [D_{r} → D_{r}] → D_{r} and ψ_{r} : D_{r} → [D_{r} → D_{r}]:

ϕ_{r}(f) = i^{−1}(⌊in_{2}(f)⌋)
ψ_{r}(d) = case i(d) of \begin{cases}⌊in_{1}(l)⌋ & → λd^{′D_{r}}. ↑ { \atop APP}(l, ↓ d′) \\ ⌊in_{2}(f)⌋ & → f \\ ⊥ & → ⊥_{[D_{r}→D_{r}]} \end{cases}

Clearly, we have that ψ_{r} ∘ ϕ_{r} = id_{[D_{r}→D_{r}]}, since i was an isomorphism. The induced interpretation is denoted by [[·]]_{r}. We can now define a putative normalization function:

Definition 1. For any Δ, let ♯Δ = max ({n + 1 | g_{n} ∈ Δ} ∪ {0}) (i.e., the least n such that ∀n′ ≥ n. g_{n′} ∉ Δ). We then define the function norm_{Δ} : Λ^{Δ} → Λ_{⊥} by

norm_{Δ}(m) = ↓ ([[m]]_{r} (λx^{V} . ↑ { \atop VAR}(x))) ♯Δ

In particular, when Δ is disjoint from the set of g_{i}-names (so ♯Δ = 0), we write just norm for norm_{Δ}.

3 Correctness of the Construction

3.1 Correctness of the Wrappers

Let s ∈ {at, nf} be a syntactic-form designator. We first define a quaternary relation, l ⪅_{s}^{Δ} m, expressing that if l represents a term at all, then that term only has free variables in Δ, is of the syntactic form s, and is convertible to m:

Definition 2. For l ∈ Λ̂ and m ∈ Λ^{Δ}, we then define the relation ⪅ by

l ⪅_{s}^{Δ} m iff ∀n ≥ ♯Δ, m′ ∈ Λ. l n = ⌊m′⌋ ⇒ m′ ∈ Λ^{Δ} ∧ ⊢_{s} m′ ∧ m′ ↔ m

Lemma 3. For fixed Δ, s, and m, the predicate P = {l | l ⪅_{s}^{Δ} m} is pointed (i.e., ⊥Λ̂ ∈ P) and inclusive (i.e., closed under limits of ω-chains).

Proof. Straightforward, noting that ⪅ is expressed using intersection, inverse image, and a (necessarily inclusive) predicate on the flat domain Λ_{⊥}.

Lemma 4. The representation relation is closed under weakening and conversion:

a. If l ⪅_{s}^{Δ} m and Δ ⊆ Δ′, then also l ⪅_{s}^{Δ′} m. b. If l ⪅_{s}^{Δ} m and m′ ∈ Λ^{Δ} with m ↔ m′, then also l ⪅_{s}^{Δ} m′.

Proof. Both parts are immediate from the definition.

Lemma 5. Representations of terms behave much like the terms themselves:

a. If v ∈ Δ then { \atop VAR}(v) ⪅_{at}^{Δ} VAR(v).

b. If l_{1} ⪅_{at}^{Δ} m_{1} and l_{2} ⪅_{nf}^{Δ} m_{2}, then { \atop APP}(l_{1}, l_{2}) ⪅_{at}^{Δ} APP(m_{1}, m_{2}). c. If l ⪅_{at}^{Δ} m, then also l ⪅_{nf}^{Δ} m.

d. Let f ∈ [V → Λ̂] and m ∈ Λ^{Δ∪{x}}. If ∀v ∉ Δ.fv ⪅_{nf}^{Δ∪{v}} m[VAR(v)/x], then { \atop LAM}(f) ⪅_{nf}^{Δ} LAM(x, m).

Proof. All parts are relatively straightforward. (b) and (d) exploit that ↔ is a congruence relation. For (d), the assumption about m’s free variables is also essential.

3.2 Adequacy of the Residualizing Model

To construct the central relation between denotations and terms, we first state an abstract version of a result due to Pitts [6]:

Theorem 1 (existence of invariant relations). Let A be a cpo, and let i : D →^{≅} (A + [D → D])_{⊥} be a minimal-invariant solution of the domain equation X ≅ (A + [X → X])_{⊥}. Let T be a set, and let predicates P_{1} ⊆ A × T, P_{2} ⊆ T, and P_{3} ⊆ T ×T ×T be given, such that {a | P_{1}(a, t)} is inclusive for every t ∈ T. Then there exists a relation ◁ ⊆ D × T, with {d | d ◁ t} inclusive for every t ∈ T, and such that, for all d ∈ D and t ∈ T:

d ◁ t iff i(d) = ⊥
or ∃a. i(d) = ⌊in_{1}(a)⌋ ∧ P_{1}(a, t)
or ∃f. i(d) = ⌊in_{2}(f)⌋ ∧ P_{2}(t) ∧
∀d′ ∈ D; t′, t′′ ∈ T. P_{3}(t, t′, t′′) ∧ d′ ◁ t′ ⇒ f(d′) ◁ t′′.

Proof. The proof proceeds exactly as in Pitts’s paper, with the following minor refinements: First, the cpo A can be arbitrary (not necessarily discrete), as long as the relation P_{1} is inclusive. Also, when P_{2} is an existential proposition, the witness need not be unique (such as the result of a deterministic evaluation), as long as the choice of witness does not affect P_{3}.

We can then establish the existence of a Kripke-style invariant relation, using sets of variables as worlds:

Lemma 6. There exists a relation ≲ such that for all Δ, d ∈ D_{r} and m ∈ Λ^{Δ},

d ≲^{Δ} m iff i(d) = ⊥
or ∃l. i(d) = ⌊in_{1}(l)⌋ ∧ l ⪅_{at}^{Δ} m

or ∃f. i(d) = ⌊in_{2}(f)⌋ ∧ (∃x ∈ V, m_{0} ∈ Λ^{Δ∪{x}}.LAM(x, m_{0}) ↔ m)

∧ ∀Δ′ ⊇ Δ, d′ ∈ D_{r}, m′ ∈ Λ^{Δ′}, m_{1} ∈ Λ^{Δ′}.
m ↔ m_{1} ∧ d′ ≲^{Δ′} m′ ⇒ f(d′) ≲^{Δ′} APP(m_{1}, m′)

Proof. By Theorem 1, taking A = Λ̂ and T = {(Δ, m) | Δ ⊆_{fin} V ∧ m ∈ Λ^{Δ}}, with the predicates chosen as

P_{1} = {(l, (Δ, m)) | l ⪅_{at}^{Δ} m}
P_{2} = {(Δ, m) | ∃x ∈ V, m_{0} ∈ Λ^{Δ∪{x}}.LAM(x, m_{0}) ↔ m}
P_{3} = {((Δ, m), (Δ′, m′), (Δ′′, m′′)) |
Δ ⊆ Δ′ = Δ′′ ∧ ∃m_{1} ∈ Λ^{Δ′}.m ↔ m_{1} ∧ m′′ = APP(m_{1}, m′)}

using the equivalence [∀x.(∃y.P (x, y)) ⇒ Q(x)] ⇔ [∀x.∀y.P (x, y) ⇒ Q(x)]. P_{1} is inclusive in its first argument by Lemma 3. We write d ≲^{Δ} m instead of d ◁ (Δ, m).

Lemma 7. The relation ≲ shares two key properties with ⪅:

a. If d ≲^{Δ} m and Δ ⊆ Δ′, then also d ≲^{Δ′} m. b. If d ≲^{Δ} m and m′ ∈ Λ^{Δ} with m ↔ m′, then also d ≲^{Δ} m′.

Proof. Both parts are straightforward, given Lemma 4, and noting the transitivity of ⊆ and ↔.

The following two lemmas will combine to establish adequacy of our semantics:

Lemma 8. For all l ∈ Λ̂, d ∈ D_{r}, and m ∈ Λ^{Δ},

a. If l ⪅_{at}^{Δ} m then ↑ l ≲^{Δ} m b. If d ≲^{Δ} m then ↓ d ⪅_{nf}^{Δ} m

Proof. Part (a) follows immediately from the definition of ↑. Part (b) exploits ↓’s definition as a least fixed point and proceeds by fixed-point induction on the pointed and inclusive (by Lemma 3) predicate

R = {φ ∈ [D_{r} → Λ̂] | ∀d, Δ, m ∈ Λ^{Δ}. d ≲^{Δ} m ⇒ φ(d) ⪅_{nf}^{Δ} m}

The verification uses the properties of Λ̂-representations (Lemma 5(a,c,d)), and that both ⪅ and ≲ are closed under conversion (Lemmas 4(b) and 7(b)).

Lemma 9. Let m ∈ Λ^{Γ}, and for all x ∈ Γ, let θ(x) ∈ Λ^{Δ} (in particular, Γ ⊆ dom θ). If ∀x ∈ Γ. ρ(x) ≲^{Δ} θ(x) then [[m]]_{r} ρ ≲^{Δ} m[θ].

Proof. By structural induction on m. The case for variables is immediate. For abstractions, like in a standard Kripke-logical-relations proof, monotonicity of ≲ (Lemma 7(a)) ensures that the environment and substitution remain related in the later world Δ′; also, closure under conversion (Lemma 7(b)) in particular implies closure under β-expansion. Both parts of Lemma 8, as well as Lemma 5(b), are used in the non-standard case for applications.

3.3 Correctness of the Normalization Function

Definition 3. The predicate tot(·) ⊆ Λ̂ is given by tot(l) ⇔ ∀n ∈ ℕ. l n ≠ ⊥.

Lemma 10. The following properties hold of the wrapper functions:

a. For all v ∈ V, tot({ \atop VAR}(v)). b. If for all v ∈ V. tot(f v) then tot({ \atop LAM}(f)). c. If tot(l_{1}) and tot(l_{2}) then tot({ \atop APP}(l_{1}, l_{2})).

Proof. Straightforward verification in each case.

Lemma 11. For all m ∈ Λ and ρ ∈ [V → D_{r}] such that for all x ∈ F V (m), there exists an l with ρ(x) = ↑ l and tot(l),

a. If ⊢_{at} m then ∃l ∈ Λ̂. [[m]]_{r} ρ = ↑ l ∧ tot(l). b. If ⊢_{nf} m then tot(↓ ([[m]]_{r} ρ)).

Proof. By simultaneous rule induction on ⊢_{at} · and ⊢_{nf} ·, relying on Lemma 10 for the totality properties of the wrappers.

Theorem 2 (semantic correctness). norm_{Δ} from Definition 1 is a normalization function on Λ^{Δ}, i.e.,

a. (soundness) If norm_{Δ}(m) = ⌊m′⌋ then m′ ∈ Λ^{Δ}, ⊢_{nf} m′, and m ↔ m′. b. (standardization) If m ↔ m′ then norm_{Δ}(m) = norm_{Δ}(m′). c. (completeness) If m ↔ m′ with ⊢_{nf} m′ then norm_{Δ}(m) ≠ ⊥.

Proof. (Soundness) Let θ_{0} be the substitution mapping every x in Δ to VAR(x), and ρ_{0} = λx^{V} . ↑ { \atop VAR}(x). By Lemma 5(a), for every x ∈ Δ, { \atop VAR}(x) ⪅_{at}^{Δ} VAR(x) = θ_{0}(x), and hence by Lemma 8(a), ρ_{0}(x) ≲^{Δ} θ_{0}(x). By Lemma 9, we then get that [[m]]_{r} ρ_{0} ≲^{Δ} m[θ_{0}] ↔ m, and therefore, by Lemma 8(b), ↓ ([[m]]_{r} ρ_{0}) ⪅_{nf}^{Δ} m. Assume now that norm_{Δ}(m) = ⌊m′⌋. Taking n = ♯Δ in Definition 2, we can then immediately read off that m′ has the required properties.

(Standardization) This follows directly from model soundness (Lemma 2), since the residualizing model is indeed a model.

(Completeness) Using Lemma 10(a), we see that ρ_{0} satisfies the condition on ρ in Lemma 11. Hence, by part (b) of the latter lemma and Definition 3, norm_{Δ}(m′) ≠ ⊥. The desired result then follows from (standardization).

4 An Implementation of the Construction

4.1 Syntax and Semantics of an ML-like Call-by-Value Language

The language is a small fragment of Standard ML where, to sidestep inessential bookkeeping, we have hard-coded the inductive representation of λ-terms,

  datatype term = VAR of string | LAM of string*term | APP of term*term

as an additional base type of the language, and simply taken the value sets underlying string and term to be the sets V and Λ, respectively.

Syntax The fragment is restricted to a single recursive datatype declaration,

             datatype dt = In_{1} of τ^{1} | · · · | In_{k} of τ^{k}

where types are given by the grammar

           τ ::= unit | int | bool | string | term | τ_{1} -> τ_{2} | dt

The syntax of ML expressions is then

e ::= x | \underline{n} | "v" | () | e_{1} + e_{2} | e_{1} = e_{2} | "g"^Int.toString e |

      fn () => e | fn x => e | e_{1} e_{2} | VAR(e) | LAM(e_{1},e_{2}) | APP(e_{1},e_{2}) |

      case e of VAR x_{1} => e_{1} | LAM(x_{2},x′_{2}) => e_{2} | APP(x_{3},x′_{3}) => e_{3} |

      In_{i}(e) | case e of In_{1} x_{1} => e_{1}| · · · | In_{k} x_{k} => e_{k} |
      if e_{1} then e_{2} else e_{3} | let fun f (x:τ_{1}):τ_{2} = e_{1} in e_{2} end

where x and f range over ML variable names.

Typing We only consider well-typed ML expressions, as captured by the judgement x_{1}: τ_{1}, ..., x_{n}: τ_{n} ⊢ e : τ, asserting that e is of type τ, with free variables x_{1}, ..., x_{n} of types τ_{1}, ..., τ_{n}. It is defined in the usual way by inference rules.

Operational semantics A complete program is a closed expression of type τ_{1}->τ_{2}, where τ_{1} and τ_{2} are ground types (i.e., not containing -> or dt). For such types, let C_{τ} denote the set of canonical values underlying τ, e.g., Cint = ℤ.

For a complete program e : τ_{1} -> τ_{2}, we can construct a computable partial function run_{e} : C_{τ_{1}} ⇀ C_{τ_{2}}, e.g., by

run_{e}(c_{1}) = c_{2} iff (e \underline{c_{1}}) ⇓ \underline{c_{2}}.

where ⇓ is the usual big-step operational semantics of expressions, and \underline{c} denotes the syntactic representation of the value c.

Denotational Semantics For the meaning of ML types, we take

[[unit]]^{ml} = 1 = {∗}  [[int]]^{ml} = ℤ  [[bool]]^{ml} = 𝔹  [[string]]^{ml} = V
[[term]]^{ml} = Λ  [[τ_{1} -> τ_{2}]]^{ml} = [[[τ_{1}]]^{ml} → [[τ_{2}]]_{⊥}^{ml}]  [[dt]]^{ml} = S

where i_{S} : S →^{≅} [[τ^{1}]]^{ml} + ⋯ + [[τ^{k}]]^{ml} is a minimal-invariant solution to the evident predomain equation. We write in_{i} : [[τ^{i}]]^{ml} → [[τ^{1}]]^{ml} + ⋯ + [[τ^{k}]]^{ml} for the injection functions.

The meaning of ML terms is defined by induction on the typing derivation; for conciseness we write only the terms. The semantics is structured such that if Γ ⊢ e : τ and for all (x : τ′) ∈ Γ, ξ(x) ∈ [[τ′]]^{ml}, then [[e]]^{ml}ξ ∈ [[τ]]_{⊥}^{ml}. In particular, the semantics of dt-constructors and recursive function definitions are given by:

[[In_{i}(e)]]^{ml} ξ = [[e]]^{ml} ξ ⋆ λa^{[[τ^{i}]]^{ml}}. ⌊i_{S}^{−1}(in_{i}(a))⌋
[[let fun f (x:τ_{1}):τ_{2} = e_{1} in e_{2} end]]^{ml} ξ =
[[e_{2}]]^{ml} ξ[f ↦ fix(λθ^{[[[τ_{1}]]^{ml}→[[τ_{2}]]_{⊥}^{ml}]}.λa^{[[τ_{1}]]^{ml}}.[[e_{1}]]^{ml} ξ[f ↦ θ, x ↦ a])]

For notational convenience in the following, we will assume that all function names f in the program are distinct. We can then unambiguously use Θ_{f} to refer to the semantic function whose fixed point f is mapped to in the environment of the let-body, and θ_{f} = fix(Θ_{f}).

Theorem 3 (computational adequacy for ML). For a complete ML program e, run_{e}(c_{1}) = c_{2} iff [[e]]^{ml} ∅ ⋆ λf. f(c_{1}) = ⌊c_{2}⌋.

Proof. Modulo trivial syntactic differences, and an equivalent formulation of the semantics in terms of strict functions between pointed cpos, rather than general ones between cpos, this is shown in, e.g., [7, Section 5]. The primary difficulty is, of course, the definition of the logical relation at type dt, which is again achieved by exploiting the minimal-invariant property of S.

4.2 The Normalization Algorithm

The concrete representation of the normalization algorithm, with many of the auxiliary definitions inlined, is shown in Fig. 1. We have instantiated dt as the type sem, with two constructors In_{1} = TM and In_{2} = FUN. It is easy to check that the top-level expression, NORM : term -> term, is a well-typed complete program in our sense.

Since ML is a call-by-value language, we must simulate the implicit callby-name nature of the residualizing semantics using thunking. We have defined sem so that [[sem]]_{⊥}^{ml} ≅ D_{r}; then semantic functions with codomain D_{r} can be represented directly as ML functions into sem, while functions with domain D_{r} are represented with source type unit -> sem. As a further optimization, the strict function ↓ : D_{r} → Λ̂ is represented as simply a function from sem.

Let us now properly relate the abstract and concrete constructions. To get a perfect isomorphism between term families and their implementation, we choose N = ℤ, with gen(n) = "g\underline{n}", e.g., gen(13) = "g13". Let i_{D} denote the isomorphism i : D_{r} →^{≅} ([ℤ → Λ_{⊥}] + [D_{r} → D_{r}])_{⊥} from before. We now also have

i_{S} : S →^{≅} [ℤ → Λ_{⊥}] + [[1 → S_{⊥}] → S_{⊥}].

Lemma 12. There exists an isomorphism i_{DS} : D_{r} →^{≅} S_{⊥}, satisfying

a. For all l ∈ Λ̂, i_{DS}(i_{D}^{−1}(⌊in_{1}(l)⌋)) = ⌊i_{S}^{−1}(in_{1}(l))⌋. b. For all f ∈ [D_{r} → D_{r}],

i_{DS}(i_{D}^{−1}(⌊in_{2}(f)⌋)) = ⌊i_{S}^{−1}(in_{2}(λt^{1→S_{⊥}}. i_{DS}(f(i_{DS}^{−1}(t ∗)))))⌋. c. i_{DS}(i_{D}^{−1}(⊥_{D_{r}})) = ⊥_{S_{⊥}}

Proof. The strict functions (i_{DS}, i_{DS}^{−1}) are constructed in the natural way by mutual recursion. That they are actually inverses, and satisfy equations (a) and (b), follows from the minimal-invariant properties of D_{r} and S.

We can also state three lemmas, relating the central domain-theoretic functions to the denotations of their syntactic counterparts:

Lemma 13. For all d ∈ D_{r} and n ∈ ℤ, ↓ d n = i_{DS}(d) ⋆ λs^{S}. θ_{down} s ⋆ λlΛ̂. l n.

datatype term = VAR of string | LAM of string*term | APP of term*term
datatype sem = TM of int -> term | FUN of (unit -> sem) -> sem;
let fun down (s:sem):int->term = fn n =>
     (case s of
        TM l => l n
      | FUN f => LAM("g"^Int.toString n,
          down (f (fn () => TM(fn n' => VAR("g"^Int.toString n)))) (n+1)))
in let fun eval (m:term):(string->sem)->sem = fn p =>
        (case m of
           VAR x => p x
         | LAM(x,m0) => FUN(fn d => eval m0
                              (fn x' => if x = x' then d () else p x'))
         | APP(m1,m2) => (case (eval m1 p) of
                            TM l => TM(fn n => APP(l n,down (eval m2 p) n))
                          | FUN f => f (fn () => eval m2 p)))
   in let fun norm (m:term):term =
            down (eval m (fn x => TM(fn n => VAR(x)))) 0
      in norm end end end

Fig. 1. The normalization algorithm, NORM , in a fragment of ML

Proof. By simultaneous fixed-point induction wrt. the relation R = {(φ, θ) ∈ [D_{r} → Λ̂] × [S → Λ̂_{⊥}] | ∀d ∈ D_{r}, n ∈ ℤ. φ d n = i_{DS}(d) ⋆ λs^{S}.θ s ⋆ λlΛ̂.l n}. The inductive step proceeds by analysis of the cases for i_{D}(d); they all follow straightforwardly, using Lemma 12.

Lemma 14. For all m ∈ Λ, ρ ∈ [V → D_{r}], and ζ ∈ [V → S_{⊥}], such that ∀x ∈ F V (m). i_{DS}(ρ(x)) = ζ(x), i_{DS}([[m]]_{r} ρ) = θ_{eval} m ⋆ λg. g ζ.

Proof. By structural induction on m, using the fixed-point equation for fix(Θ_{eval}) in the inductive steps, Lemma 12 throughout, and Lemma 13 in one of the subcases for application.

Lemma 15. For all m ∈ Λ, norm(m) = θ_{norm} m.

Proof. Follows easily from the definition of θ_{norm}, using Lemmas 12, 13 and 14.

Theorem 4 (implementation correctness). The program NORM satisfies that run_{NORM} (m) = m′ ⇔ norm(m) = ⌊m′⌋. That is, NORM computes the normalization function for all λ-terms without free occurrences of g\underline{n}-variables (including, in particular, all closed terms).

Proof. A direct consequence of Lemma 15 and Theorem 3.

5 Conclusions and Perspectives

We have presented a domain-theoretic analysis of a normalization-by-evaluation construction for untyped λ-terms. Compared to the typed case, the main difference is a change from induction on types to general recursion, both for function definitions and for the domains and relations on them. That the correctness proof has a generalized computational-adequacy result at its core, further strengthens the connection between normalization and evaluation. Moreover, the algorithmic content of the construction corresponds very directly to a simple functional program, enabling a precise verification of the normalizer as actually implemented.

There are several possible directions in which to extend the present work. Some were already mentioned in Section 1.5, such as generalizations of the algorithm to Böhm trees. It should also be possible to extend the language and notion of normalization with interpreted constants in a suitable sense. But already the current results indicate that the fundamental ideas of NBE are not incompatible with general recursive types. Thus, reduction-free normalization may provide a complementary view of other equational systems that are currently analyzed using exclusively reduction-based methods. It might even be possible to find unified formulations of rewriting-theoretic and model-theoretic normalization results about particular such systems.

Acknowledgment The authors wish to thank Olivier Danvy and the FOSSACS’04 reviewers for their insightful comments.

References

1. Klaus Aehlig and Felix Joachimski. Operational aspects of untyped normalization by evaluation. Mathematical Structures in Computer Science, 2004(?). To appear; avail-

able from http://www.mathematik.uni-muenchen.de/~aehlig/pub/03-nbe.ps.

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

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

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

5. Andrzej Filinski and Henning Korsholm Rohde. A denotational account of untyped normalization by evaluation (extended version). BRICS Report RS-03-40, University of Aarhus, Denmark, December 2003. Available from http://www.brics.dk/

RS/03/40/.

6. Andrew M. Pitts. Computational adequacy via ‘mixed’ inductive definitions. In Mathematical Foundations of Programming Semantics, volume 802 of Lecture Notes in Computer Science, pages 72–82. Springer-Verlag, April 1993.

7. Andrew M. Pitts. Relational properties of domains. Information and Computation, 127(2):66–90, June 1996.

8. Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223–255, December 1977.

9. Mark R. Shinwell, Andrew M. Pitts, and Murdoch J. Gabbay. FreshML: Programming with binders made simple. In Eighth ACM SIGPLAN International Conference on Functional Programming, pages 263–274. ACM Press, Uppsala, Sweden, August