BRICS

Basic Research in Computer Science

Denotational Aspects of Untyped Normalization by Evaluation

Andrzej Filinski Henning Korsholm Rohde BRICS Report Series RS-05-4 ISSN 0909-0878 February 2005 BRICS RS-05-4 Filinski & Rohde: Denotational Aspects of Untyped Normalization by Evaluation Copyright \begin{matrix}c \\ ◯ \end{matrix} 2005, Andrzej Filinski & Henning Korsholm Rohde.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/05/4/

Denotational Aspects of Untyped Normalization by Evaluation^{∗}

(Extended version, with detailed proofs)

Andrzej Filinski DIKU, University of Copenhagen, Denmark

                  andrzej@diku.dk

Henning Korsholm Rohde BRICS^{†}, University of Aarhus, Denmark

                   hense@brics.dk

February 2005

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 computational-adequacy 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 in normal form and β-equivalent to the input term); identification (β-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.

Finally, we generalize the construction to produce an infinitary variant of normal forms, namely Böhm trees. We show that the three-part characterization of correctness, as well as the proofs, extend naturally to this generalization.

∗Extended version of an article to appear in RAIRO – Theoretical Informatics and Applications.

An earlier version appeared in the proceedings of FOSSACS 2004 [FR04, FR03].

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

Contents

1 Introduction 3 1.1 Reduction-based and reduction-free normalization . . . . . . . . . . . 3 1.2 Normalization by evaluation . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 The Berger-Schwichtenberg normalization algorithm . . . . . . . . . . 4 1.4 A tentative algorithm for untyped terms . . . . . . . . . . . . . . . . . 4 1.5 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2 A semantic normalization construction 7 2.1 Syntax and semantics of the untyped λ-calculus . . . . . . . . . . . . . 7 2.2 Output-term generation . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3 A residualizing model . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3 Correctness of the construction 10 3.1 Correctness of the wrappers . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 Adequacy of the residualizing model . . . . . . . . . . . . . . . . . . . 11 3.3 Correctness of the normalization function . . . . . . . . . . . . . . . . 15

4 An implementation of the construction 16 4.1 Syntax and semantics of an ML-like call-by-value language . . . . . . . 16 4.2 The normalization algorithm . . . . . . . . . . . . . . . . . . . . . . . 19

5 A generalization to Böhm trees 25 5.1 From λ-terms to λ-trees . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.2 A semantic Böhm-tree construction . . . . . . . . . . . . . . . . . . . . 28 5.3 Correctness of the construction . . . . . . . . . . . . . . . . . . . . . . 29 5.4 An implementation of the construction . . . . . . . . . . . . . . . . . . 36 5.5 Observing Böhm trees . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

5.5.1 Computations with infinite results . . . . . . . . . . . . . . . . 40 5.5.2 Observing λ-trees . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5.5.3 Implementing tree-observations in ML . . . . . . . . . . . . . . 42

6 Conclusions and perspectives 43

A Existence of invariant relations 45

B Existence of isomorphisms 47 B.1 Isomorphisms for the redualizing model . . . . . . . . . . . . . . . . . 47 B.2 Isomorphisms for Böhm trees . . . . . . . . . . . . . . . . . . . . . . . 49

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 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 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 [CD97].

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 any normal-form term can 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 [CD97], but this gets somewhat complicated for domaintheoretic 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 [BS91]. 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 typeindexed function families – reification, ↓^{τ} : [[τ]] → Λ, and reflection, ↑^{τ} : Λ → [[τ]] – by mutual induction on the type index τ:

↓^{b} l = l  ↓^{τ_{1}→τ_{2}} f = LAM(x^{τ_{1}}, ↓^{τ_{2}} (f(↑^{τ_{1}} VAR(x)))) (x “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 the 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 ⊥ (undefined), 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 [Plo77]. 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 [Pit93].

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) and how the domain-theoretic analysis directly validates a functional program implementing the construction (Section 4). Finally, we show how the construction can be generalized naturally to Böhm trees (Section 5).

1.5 Related work

The closest related work to ours is probably the NBE-based (in the alternate, reductionoriented sense) algorithm for untyped β-normalization proposed by Aehlig and Joachimski [AJ04]. However, while the functional programs ultimately derived from the analyses are quite similar, the correctness arguments are completely different: theirs are based on syntactic concepts and results from higher-order rewriting theory, rather than on the domain-theoretic constructions underlying ours.

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; whereas the actual normalization program is formulated as a compositional interpreter in Haskell, using de Bruijn indices for bound variables, and a reflexive type for the meanings of highertyped terms. It thus remains a potentially significant task to verify that the concrete Haskell program correctly implements the abstract algorithm. On the other hand, formally relating the domain-theoretic constructions in the model-based normalizer to the functional terms implementing them, is completely straightforward.

An untyped, reduction-based NBE-like algorithm can also be found in disguise in Grégoire and Leroy’s work [GL02], whose focus is on compilation. Their concrete algorithm of strong reduction (i.e., β-normalization) by iterated symbolic weak reduction (akin to ↑ and [[·]]) and readback (akin to ↓) is ultimately quite similar to ours. Their algorithm also handles several language extensions, such as inductive datatypes and guarded fixpoints. However, as they consider only a strongly-normalizing fragment of the λ-calculus, establishing correctness becomes significantly simpler. Their implementation takes the form of an abstract machine, whose (5000-line) correctness proof is mechanically checked using a proof assistant. They do not mention how the abstract machine is actually implemented.

Many of the constructions in the present paper are inspired by the first author’s work on type-directed partial evaluation [Fil99]. 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, under 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, appears in a recent paper by Shinwell et al. [SPG03, 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 (informally attributed to Coquand) is not supported by a formal correctness argument. In our variant, generation of fresh names is handled explicitly: since constructed output terms are never subsequently analyzed by pattern-matching, 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 = {x, y, …} be a countably infinite set of (object) variables, with x and v ranging over V. The set of λ-terms m is then the least set Λ such that

Λ = {VAR(x) | x ∈ V} ∪ {LAM(x, m_{0}) | x ∈ V, m_{0} ∈ Λ} ∪ {APP(m_{1}, m_{2}) | m_{1} ∈ Λ, m_{2} ∈ Λ} .

Note that we do not identify α-equivalent terms at the level of syntax. 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}[θ])

where f[a ↦ b] is function extension: f[a ↦ b](a′) = b if a′ = a, and f(a′) otherwise. To keep the substitution operation deterministic, we assume that the x′ in the LAMclause is picked as some arbitrary but fixed function of the (finite) set of variables it needs to avoid. As a special case, we use the standard notation m[m′/x] to mean m[ ∅[x ↦ m′] ].

Convertibility 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})} .

For s ∈ {nf, at}, we take N_{s} = {m | ⊢_{s} m}, i.e., the set of terms that can be shown to be of syntactic form s by a finite number of rule applications.

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 (identification); 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 continuous-function space [D → D] is a retract of D, i.e., that there exist continuous functions

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

with ψ ∘ ϕ = 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 pointed cpo Λ̂ (dependent on the name generation scheme) with elements denoted by l, together with continuous 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 = {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). (As is conventional in functional-programming syntax, function application by juxtaposition binds tighter than all explicit infix operators, including ⋆.)

Definition 1 We 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., Pitts [Pit93]), we know that there exists a pointed cpo D_{r}, together with an isomorphism

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

We write

tm(l) = i_{D}^{−1}(⌊in_{1}(l)⌋)  fun(f) = i_{D}^{−1}(⌊in_{2}(f)⌋)  ⊥_{D_{r}} = i_{D}^{−1}(⊥) .

Then any element of D_{r} can be uniquely written as one of tm(l), fun(f), or ⊥_{D_{r}}.

Moreover, the standard domain-theoretic solution is in fact a so-called minimal invariant [Pit93], which we will exploit in the correctness proof. (In the specific case of D_{r}, the minimal-invariant condition says that the following “copy function” e : D_{r} → D_{r}, recursively defined in the least-fixed-point sense,

e(d) = case d of \begin{cases}tm(l) & → tm(l) \\ fun(f) & → fun(e ∘ f ∘ e) \\ ⊥_{D_{r}} & → ⊥_{D_{r}} \end{cases}

is in fact the identity function on D_{r}.)

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

↓ d = case d of \begin{cases}tm(l) & → l \\ fun(f) & → { \atop LAM}(λx^{V}. ↓ (f(↑ ({ \atop VAR}(x))))) \\ ⊥_{D_{r}} & → ⊥Λ̂ \end{cases}
↑ l = tm(l) ,

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

ϕ_{r}(f) = fun(f)
ψ_{r}(d) = case d of \begin{cases}tm(l) & → λd^{′D_{r}}. ↑ { \atop APP}(l, ↓ d′) \\ fun(f) & → f \\ ⊥_{D_{r}} & → ⊥_{[D_{r}→D_{r}]} . \end{cases}

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

Definition 2 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)))) ♯Δ .

We also define the general function norm : Λ → Λ_{⊥} like above, but with ♯Δ replaced by 0. Then for any Δ such that Δ ∩ G = ∅, and m ∈ Λ^{Δ}, norm(m) = norm_{Δ}(m).

3 Correctness of the construction

3.1 Correctness of the wrappers

We first define what it means for an element of Λ̂ to represent a λ-term with some additional properties:

Definition 3 For l ∈ Λ̂, Δ ⊆_{fin} V, s ∈ {at, nf}, and m ∈ Λ^{Δ}, we define the representation relation ⪅ by

l ⪅_{s}^{Δ} m iff ∀n ≥ ♯Δ. l n = ⊥ ∨ ∃m′ ∈ Λ^{Δ}. l n = ⌊m′⌋ ∧ m′ ↔ m ∧ m′ ∈ N_{s} .

That is, as long as we avoid clashes with generated bound-variable names, any concrete term generated from l has only free variables in Δ, is convertible to m, and is of syntactic form s. Note, however, that we only capture a notion of partial correctness here: if l does not generate a term at all, the conditions are vacuously satisfied.

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 as an intersection of inverse images by a continuous function (application to n) of 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. For part (a), assume l ⪅_{s}^{Δ} m and Δ ⊆ Δ′, and consider an n ≥ ♯Δ′. Then also n ≥ ♯Δ, and thus, by the assumption on l, if l n ≠ ⊥, there exists an m′ ∈ Λ^{Δ} ⊆ Λ^{Δ′}, satisfying the conditions in l ⪅_{s}^{Δ′} m.

For part (b), assume l ⪅_{s}^{Δ} m, and let m′ ∈ Λ^{Δ} with m ↔ m′ be given. Then, when n ≥ ♯Δ and l n ≠ ⊥, there exists an m′′ ∈ Λ^{Δ} such that l n = ⌊m′′⌋, m′′ ↔ m, and m′′ ∈ N_{s}. By transitivity of ↔, we must also have m′′ ↔ m′, so l ⪅_{s}^{Δ} m′ as required. □

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: Parts (a), (b), and (c) are straightforward, where (b) uses that convertibility is a congruence wrt. APP. We will now prove (d).

Let f, x, and m, satisfy the condition of the lemma, and let n ≥ ♯Δ and m′ with { \atop LAM}(f) n = ⌊m′⌋ be given; we must show that m′ ∈ Λ^{Δ}, m′ ↔ LAM(x, m), and m′ ∈ N_{nf}.

From the definition of { \atop LAM}(f), we must have that, for some m_{0}, f g_{n} (n + 1) = ⌊m_{0}⌋ and m′ = LAM(g_{n}, m_{0}). By definition of ♯, g_{n} ∉ Δ, so by assumption on f, f g_{n} ⪅_{nf}^{Δ∪{g_{n}}} m[VAR(g_{n})/x]. Further, since n + 1 ≥ ♯(Δ ∪ {g_{n}}), the definition of ⪅ gives us that m_{0} ∈ Λ^{Δ∪{g_{n}}}, m_{0} ↔ m[VAR(g_{n})/x], and m_{0} ∈ N_{nf},. But then clearly LAM(g_{n}, m_{0}) ∈ Λ^{Δ}, LAM(g_{n}, m_{0}) ∈ N_{nf}, and

LAM(g_{n}, m_{0}) ↔ LAM(g_{n}, m[VAR(g_{n})/x]) ↔ LAM(x, m) ,

where the first conversion is by congruence wrt. LAM and the second is a valid αconversion, since g_{n} ∉ Δ ensures that g_{n} ∉ F V (m) \ {x}. □

The constructions and results in the next section rely only on those properties of the wrappers from Definition 1 and the relation ⪅ from Definition 3 that were established in Lemmas 3–5, not on the definitions themselves.

3.2 Adequacy of the residualizing model

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

Theorem 1 (existence of invariant relations) Let A be a cpo, and let i : D →^{≅} (A+[D→D])_{⊥} be a minimal invariant. 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, such that, for all d ∈ D and t ∈ T,

d ◁ t iff ( \begin{matrix}d = ⊥_{D} ∨ \\ ∃a. d = i^{−1}(⌊in_{1}(a)⌋) ∧ P_{1}(a, t) ∨ \\ ∃f. d = i^{−1}(⌊in_{2}(f)⌋) ∧ P_{2}(t) ∧ \\ ∀d′ ∈ D; t′, t′′ ∈ T. P_{3}(t, t′, t′′) ∧ d′ ◁ t′ ⇒ f(d′) ◁ t′′ \end{matrix} ) .

Proof: See Appendix A □

We can recover Pitts’s original result as follows. Let Λ_{ℤ} be an extension of Λ with PCF-style integer arithmetic, and let ⇓ be the usual big-step, call-by-name evaluation relation on Λ_{ℤ}^{∅}. We then take A as ℤ, T as Λ_{ℤ}^{∅}, P_{1}(n, m) as m ⇓ \underline{n}, P_{2}(m) as ∃x, m_{0}. m ⇓ LAM(x, m_{0}), and P_{3}(m, m′, m′′) as ∀x, m_{0}. m ⇓ LAM(x, m_{0}) ⇒ m′′ = m_{0}[m′/x]. Note that, by determinacy of ⇓, the x and m_{0} are uniquely determined when they exist, so P_{2} and P_{3} would naturally be joined into a single condition.

The computational-adequacy proof for evaluation then shows, by a straightforward structural induction on m, that if ρ : V → D and θ : V ⇀ Λ_{ℤ}^{∅} are such that ∀x ∈ F V (m). ρ(x) ◁ θ(x), then [[m]]ρ ◁ m[θ]. For the special case when m is itself a closed term, we then immediately read off that if [[m]]∅ ≠ ⊥_{D} then m must evaluate to a value.

When generalizing to normalization, there are two complications. First, we consider symmetric equivalence, not directed evaluation, so the relation d ◁ − must be closed under arbitrary β-conversions, not just head-β-expansions as before. Second, since we also normalize under lambdas, we must in general consider substitutions that replace variables with open terms. Accordingly, we replace the fixed set of closed terms, Λ^{∅}, with a Kripke-style family of term sets, indexed by their allowed free variables, Λ^{Δ}. Somewhat surprisingly, Pitts’s result – although in the generalized formulation – accounts directly for these adaptations:

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

d ≲^{Δ} m iff ( \begin{matrix}d = ⊥_{D_{r}} ∨ \\ ∃l. d = tm(l) ∧ l ⪅_{at}^{Δ} m ∨ \\ ∃f. d = fun(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′) \end{matrix} ) .

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

□

Note how, in the function case, we require that f and m can also be meaningfully applied to arguments from later worlds Δ′, much like in a conventional, type-indexed Kripke logical relation [Mit96, p.590].

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: We proceed according to the cases for d ≲^{Δ} m in Lemma 6:

Case d = ⊥_{D_{r}}: Both parts are immediate.

Case d = tm(l): Both parts follow directly from the corresponding parts of Lemma 4, taking s = at.

Case d = fun(f): For (a), if m_{0} ∈ Λ^{Δ∪{x}}, then also m_{0} ∈ Λ^{Δ′∪{x}}. Likewise, any Δ′′ with Δ′′ ⊇ Δ′ in the universal quantification also satisfies Δ′′ ⊇ Δ.

For (b), any m_{0} satisfying LAM(x, m_{0}) ↔ m also satisfies LAM(x, m_{0}) ↔ m′ by transitivity. Similarly, the terms m_{1} satisfying m ↔ m_{1} are the same as those that satisfy m′ ↔ m_{1}.

□

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 Lemma 6(⇐) and the definition of ↑.

For part (b), recall that reification was conceptually defined in terms of the continuous function Φ : [D_{r} → Λ̂] → [D_{r} → Λ̂],

Φ(φ) = λd^{D_{r}}. case d of \begin{cases}tm(l) & → l \\ fun(f) & → { \atop LAM}(λx^{V}. φ(f(↑ ({ \atop VAR}(x))))) \\ ⊥_{D_{r}} & → ⊥Λ̂ \end{cases}

with ↓ = fix(Φ). Consider therefore the predicate

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

It is straightforward to verify that R is pointed and inclusive, using the corresponding properties of ⪅ (Lemma 3). To show that fix(Φ) ∈ R by fixed-point induction, it therefore suffices to show that for all φ ∈ R, Φ(φ) ∈ R.

Accordingly, assume that φ ∈ R and d ≲^{Δ} m; we aim to prove that Φ(φ)(d) ⪅_{nf}^{Δ} m. We divide the argument into cases over d:

Case d = ⊥_{D_{r}}: Then Φ(φ)(d) = ⊥Λ̂, and thus ⊥Λ̂ ⪅_{nf}^{Δ} m, by Lemma 3.

Case d = tm(l): Then Φ(φ)(d) = l, and by Lemma 6(⇒) and Lemma 5(c), l ⪅_{nf}^{Δ} m.

Case d = fun(f): Then Φ(φ)(d) = { \atop LAM}(λx^{V}. φ(f(↑ ({ \atop VAR}(x))))). Let v ∉ Δ be arbitrary. By Lemma 5(a), { \atop VAR}(v) ⪅_{at}^{Δ∪\{v\}} VAR(v), and so by part (a) above,

↑ ({ \atop VAR}(v)) ≲^{Δ∪\{v\}} VAR(v) .

By assumption on m and Lemma 6(⇒), there exist x and m_{0} ∈ Λ^{Δ∪{x}} such that LAM(x, m_{0}) ↔ m.

Take Δ′ = Δ ∪ \{v\}, d′ = ↑ ({ \atop VAR}(v)), m′ = VAR(v), and m_{1} = LAM(x, m_{0}). By assumption on f, we then get that

f(↑ ({ \atop VAR}(v))) ≲^{Δ∪\{v\}} APP(LAM(x, m_{0}), VAR(v)) .

Since APP(LAM(x, m_{0}), VAR(v)) ↔ m_{0}[VAR(v)/x], and ≲ is closed under conversion (Lemma 7(b)), we also have

f(↑ ({ \atop VAR}(v))) ≲^{Δ∪\{v\}} m_{0}[VAR(v)/x] .

Hence, by assumption on φ,

(λx^{V}.φ(f(↑ ({ \atop VAR}(x))))) v ⪅_{nf}^{Δ∪\{v\}} m_{0}[VAR(v)/x] .

And thus, by Lemma 5(d),

{ \atop LAM}(λx^{V}.φ(f(↑ ({ \atop VAR}(x))))) ⪅_{nf}^{Δ} LAM(x, m_{0}) .

Finally, since ⪅ is closed under conversion (Lemma 4(b)), we get Φ(φ)(d) ⪅_{nf}^{Δ} m, as required.

□

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.

Case m = VAR(x): This follows immediately from the assumption on ρ and θ, since [[VAR(x)]]_{r} ρ = ρ(x).

Case m = LAM(x, m_{0}): Take f = λd.[[m_{0}]]_{r} ρ[x ↦ d]. Then i_{D}([[m]]_{r} ρ) = ⌊in_{2}(f)⌋, so to use Lemma 6(⇐), we must establish that f and m[θ] satisfy the requirements for the third alternative. First, from the definition of substitution, we get that LAM(x, m_{0})[θ] = LAM(x′, m′_{0}) for some x′ and m′_{0} = m_{0}[θ[x↦VAR(x′)]]. Clearly m′_{0} ∈ Λ^{Δ∪{x′}}, and LAM(x′, m′_{0}) ↔ m[θ] by reflexivity of ↔ .

Second, let Δ′ ⊇ Δ, d′, m_{1} ∈ Λ^{Δ′} and m′ ∈ Λ^{Δ′} be given, with m[θ] ↔ m_{1} and d′ ≲^{Δ′} m′; we must show that f(d′) ≲^{Δ′} APP(m_{1}, m′). Take ρ′ = ρ[x ↦ d′] and θ′ = θ[x ↦ m′]. Using the assumption on d′ and m′ for x, and monotonicity of ≲ (Lemma 7(a)) for the remaining variables in Γ, we get that for all x′′ ∈ Γ ∪ {x}, ρ′(x′′) ≲^{Δ′} θ′(x′′). Hence, by IH on m_{0}, f(d′) = [[m_{0}]]_{r} ρ′ ≲^{Δ′} m_{0}[θ′]. And finally, since

m_{0}[θ′]
↔ APP(LAM(x, m_{0}), VAR(x))[θ′] = APP(LAM(x, m_{0})[θ′], VAR(x)[θ′])
↔ APP(LAM(x, m_{0})[θ], m′) = APP(m[θ], m′)
↔ APP(m_{1}, m′) ,

and ≲ is closed under conversion (Lemma 7(b)), we get f(d′) ≲^{Δ′} APP(m_{1}, m′), as required.

Case m = APP(m_{1}, m_{2}): Here, [[APP(m_{1}, m_{2})]]_{r} ρ = ψ_{r}([[m_{1}]]_{r} ρ) ([[m_{2}]]_{r} ρ). We divide the argument into subcases over [[m_{1}]]_{r} ρ:

Case [[m_{1}]]_{r} ρ = ⊥_{D_{r}}: Then ψ_{r}([[m_{1}]]_{r} ρ)([[m_{2}]]_{r} ρ) = ⊥ ≲^{Δ} APP(m_{1}, m_{2})[θ].

Case [[m_{1}]]_{r} ρ = tm(l): Then ψ_{r}([[m_{1}]]_{r} ρ)([[m_{2}]]_{r} ρ) = ↑ ({ \atop APP}(l, ↓ ([[m_{2}]]_{r} ρ))). By IH on m_{1} and Lemma 6(⇒), l ⪅_{at}^{Δ} m_{1}[θ], and by IH on m_{2} and Lemma 8(b), ↓ ([[m_{2}]]_{r} ρ) ⪅_{nf}^{Δ} m_{2}[θ]. Hence by Lemma 5(b),

{ \atop APP}(l, ↓ ([[m_{2}]]_{r} ρ)) ⪅_{at}^{Δ} APP(m_{1}[θ], m_{2}[θ]) = APP(m_{1}, m_{2})[θ] = m[θ] .

And thus, by Lemma 8(a), ↑ ({ \atop APP}(l, ↓ [[m_{2}]]_{r} ρ)) ≲^{Δ} m[θ]. Case [[m_{1}]]_{r} ρ = fun(f): Then ψ_{r}([[m_{1}]]_{r} ρ)([[m_{2}]]_{r} ρ) = f([[m_{2}]]_{r} ρ). By IH on m_{1}

and Lemma 6(⇒), we have, in particular, that if d′ ≲^{Δ} m′ then f(d′) ≲^{Δ} APP(m_{1}[θ], m′). Take d′ = [[m_{2}]]_{r} ρ and m′ = m_{2}[θ]. Then, using IH on m_{2},

f([[m_{2}]]_{r} ρ) ≲^{Δ} APP(m_{1}[θ], m_{2}[θ]) = m[θ]. □

3.3 Correctness of the normalization function

For showing completeness of the normalizer, we first establish that, for a term already in normal form, reifying its residualizing denotation gives an always-defined term generator.

Definition 4 For any l ∈ Λ̂, we define the uniform definedness predicate def(l) by def(l) ⇔ ∀n ∈ ω. l n ≠ ⊥.

Lemma 10 The wrapper functions preserve definedness:

a. For all v ∈ V, def({ \atop VAR}(v)).

b. If for all v ∈ V, def(f v), then def({ \atop LAM}(f)).

c. If def(l_{1}) and def(l_{2}), then def({ \atop APP}(l_{1}, l_{2})).

Proof: Straightforward verification in each case. □

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

a. If m ∈ N_{at}, then ∃l ∈ Λ̂. [[m]]_{r} ρ = ↑ l ∧ def(l).

b. If m ∈ N_{nf}, then def(↓ ([[m]]_{r} ρ)).

Proof: By simultaneous rule induction on ⊢_{at} · and ⊢_{nf} ·. The relevant cases are:

Case ⊢_{at} VAR(x): Then [[m]]_{r} ρ = ρ(x), and x ∈ F V (m), so the result follows directly from the assumption on ρ.

Case ⊢_{at} APP(m_{1}, m_{2}) because ⊢_{at} m_{1} and ⊢_{nf} m_{2}: By IH(a) on the first premise, there exists an l_{1} such that [[m_{1}]]_{r} ρ = ↑ l_{1} and def(l_{1}). Therefore, [[m]]_{r} ρ = ↑ ({ \atop APP}(l_{1}, ↓ ([[m_{2}]]_{r} ρ))). Take l_{2} = ↓ ([[m_{2}]]_{r} ρ) and l = { \atop APP}(l_{1}, l_{2}). By IH(b) on the second premise, def(l_{2}), so by Lemma 10(c), def(l), as required.

Case ⊢_{nf} m because ⊢_{at} m: By IH(a) on the premise, [[m]]_{r} ρ = ↑ l, with def(l). But ↓ (↑ l) = l, so also def(↓ [[m]]_{r} ρ).

Case ⊢_{nf} LAM(x, m_{0}) because ⊢_{nf} m_{0}: Expanding the definition of ↓ for the functional case, we have to show that def({ \atop LAM}(λx.↓ ([[m_{0}]]_{r} ρ[x ↦ ↑ ({ \atop VAR}(x))]))). By Lemma 10(b), it suffices to show that, for every v ∈ V, def(↓ ([[m_{0}]]_{r} ρ′)), where ρ′ = ρ[x ↦ ↑ ({ \atop VAR}(v))]. This follows from IH(b) on the premise, if for every x′ ∈ F V (m_{0}), there exists an l, such that ρ′(x′) = ↑ l and def(l). But for x′ ≠ x, we must have x′ ∈ F V (m), so this follows from the assumption on ρ; and for x′ = x, it follows from Lemma 10(a).

□

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

a. (soundness) If norm_{Δ}(m) = ⌊m′⌋, then m′ ∈ Λ^{Δ}, m′ ↔ m, and m′ ∈ N_{nf}. b. (identification) If m ↔ m′, then norm_{Δ}(m) = norm_{Δ}(m′).

c. (completeness) If for some m′ ∈ N_{nf}, m′ ↔ m, then norm_{Δ}(m) ≠ ⊥.

Proof: (Soundness) Let ρ_{0} = λx^{V}. ↑ ({ \atop VAR}(x)), and let θ_{0} be the substitution mapping every x in Δ to 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 thus, by Lemma 8(b), ↓ ([[m]]_{r} ρ_{0}) ⪅_{nf}^{Δ} m. Assume now that norm_{Δ}(m) = ↓ ([[m]]_{r} ρ_{0}) ♯Δ = ⌊m′⌋. Taking n = ♯Δ in Definition 3, we can then immediately read off that m′ has the required properties.

(Identification) 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 4, ↓ ([[m′]]_{r} ρ_{0}) ♯Δ ≠ ⊥. And thus, again by model soundness, also norm_{Δ}(m) = ↓ ([[m]]_{r} ρ_{0}) ♯Δ ≠ ⊥. □

Note that the correctness theorem does not completely pin down the behavior of the normalizer: the soundness specification allows it to return any valid αvariant of the normal form, such as normalizing the term LAM(x, LAM(y, VAR(y))) to LAM(g_{0}, LAM(g_{0}, VAR(g_{0}))). Conversely, completeness says only that if a term has a β-normal form, the normalizer will also find one, though not necessarily the same one.

It would also be possible to adopt a “tight” specification of normal forms, requiring them to also be α-normal, such as the current de Bruijn-level naming. Then, a term can have at most one normal form, and the normalizer will in fact find exactly that one when it exists – which would allow us to combine soundness and completeness into a single statement.

4 An implementation of the construction

4.1 Syntax and semantics of an ML-like call-by-value language

As our implementation language, we take a small fragment of Standard ML [MTHM97]. We deliberately choose an eager language, whose finer control over lifting allows us to mirror all the semantic constructions almost exactly (i.e., up to isomorphism). Any necessary laziness can be easily added by explicit thunking. On the other hand, working in an inherently lazy language, such as Haskell, would make it harder to work with, e.g., the set of λ-terms as a datatype, without also including spurious infinite and partially-defined elements.

Syntax The fragment is parameterized by a sequence of recursive datatype declarations, each of the form

datatype dt^{i} = In_{1}^{i} of τ_{11}^{i} * ⋯ * τ_{1n_{1}}^{i} | ⋯ | In_{k}^{i} of τ_{k1}^{i} * ⋯ * τ_{kn_{k}}^{i} ,

where ML types τ are given by the grammar,

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

\overline{Γ, x : τ ⊢ x : τ} \overline{Γ ⊢ \underline{n} : int}  \overline{Γ ⊢ "v" : string}  \overline{Γ ⊢ () : unit}
\frac{Γ ⊢ e_{1} : int Γ ⊢ e_{2} : int}{Γ ⊢ e_{1} + e_{2} : int} \frac{Γ ⊢ e_{1} : τ Γ ⊢ e_{2} : τ}{Γ ⊢ e_{1} = e_{2} : bool} (τ ground)

                     \frac{Γ ⊢ e : int}{Γ ⊢ "g"^Int.toString e : string}

\frac{Γ ⊢ e : τ}{Γ ⊢ fn () => e : unit->τ} \frac{Γ, x : τ_{1} ⊢ e : τ_{2}}{Γ ⊢ fn x => e : τ_{1}->τ_{2}} \frac{Γ ⊢ e_{1} : τ_{1}->τ_{2} Γ ⊢ e_{2} : τ_{1}}{Γ ⊢ e_{1} e_{2} : τ_{2}}

\frac{Γ ⊢ e_{1} : τ_{j1}^{i} ⋯ Γ ⊢ e_{n} : τ_{jn_{j}}^{i}}{Γ ⊢ In_{j}^{i}(e_{1},…,e_{n_{j}}) : dt^{i}}

\frac{\begin{matrix}Γ ⊢ e : dt^{i} \\ Γ, x_{11} : τ_{11}^{i}, …, x_{1n_{1}} : τ_{1n_{1}}^{i} ⊢ e_{1} : τ ⋯ Γ, x_{k1} : τ_{k1}^{i}, …, x_{kn_{k}} : τ_{kn_{k}}^{i} ⊢ e_{k} : τ \end{matrix}}{Γ ⊢ case e of In_{1}^{i}(x_{11},…,x_{1n_{1}}) => e_{1} | ⋯ | In_{k}^{i}(x_{k1},…,x_{kn_{k}}) => e_{k} : τ}

\frac{Γ ⊢ e_{1} : bool Γ ⊢ e_{2} : τ Γ ⊢ e_{3} : τ}{Γ ⊢ if e_{1} then e_{2} else e_{3} : τ}

\frac{Γ, f : τ_{1}->τ_{2}, x : τ_{1} ⊢ e_{1} : τ_{2} Γ, f : τ_{1}->τ_{2} ⊢ e_{2} : τ}{Γ ⊢ let fun f (x:τ_{1}):τ_{2} = e in e_{2} end : τ}

Figure 1: Typing rules for the ML fragment

The datatypes cannot be mutually recursive, but may be cumulative, i.e., later declarations may refer to earlier ones. We say that a type is ground if it does not contain – directly, or indirectly (through a datatype declaration) – any function spaces. For notational simplicity, we assume that the set of λ-term variable names, V, is identified with the set of ML character strings.

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} | In_{j}^{i}(e_{1},…,e_{n}) |

case e of In_{1}^{i}(x_{11},…,x_{1n_{1}}) => e_{1} | ⋯ | In_{k}^{i}(x_{k1},…,x_{kn_{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}. The typing rules are shown in Figure 1

Denotational semantics For the meaning of ML types, we take

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

[[x]]^{ml} ξ = ⌊ξ(x)⌋  [[\underline{n}]]^{ml} ξ = ⌊n⌋  [["v"]]^{ml} ξ = ⌊v⌋  [[()]]^{ml} ξ = ⌊∗⌋
[[e_{1} + e_{2}]]^{ml} ξ = [[e_{1}]]^{ml} ξ ⋆ λn_{1}^{ℤ}. [[e_{2}]]^{ml} ξ ⋆ λn_{2}^{ℤ}. ⌊n_{1} + n_{2}⌋
[[e_{1} = e_{2}]]^{ml} ξ = [[e_{1}]]^{ml} ξ ⋆ λa_{1}^{[[τ]]^{ml}}. [[e_{2}]]^{ml} ξ ⋆ λa_{2}^{[[τ]]^{ml}}. ⌊a_{1} = a_{2}⌋
[["g"^Int.toString e]]^{ml} ξ = [[e]]^{ml} ξ ⋆ λn^{ℤ}. ⌊g\underline{n}⌋

[[fn () => e]]^{ml} ξ = ⌊λu^{1}.[[e]]^{ml} ξ⌋ [[fn x => e]]^{ml} ξ = ⌊λa^{[[τ_{1}]]^{ml}}.[[e]]^{ml} ξ[x ↦ a]⌋

[[e_{1} e_{2}]]^{ml} ξ = [[e_{1}]]^{ml} ξ ⋆ λf^{[[[τ_{1}]]^{ml}→[[τ_{2}]]_{⊥}^{ml}]}. [[e_{2}]]^{ml} ξ ⋆ λa^{[[τ_{1}]]^{ml}}. f a
[[In_{j}^{i}(e_{1},…,e_{n})]]^{ml} ξ =
[[e_{1}]]^{ml} ξ ⋆ λa_{1}^{[[τ_{j1}^{i}]]^{ml}}. · · · .[[e_{n}]]^{ml} ξ ⋆ λa_{n}^{[[τ_{jn}^{i}]]^{ml}}. ⌊ιIni_{j}(a_{1}, …, a_{n})⌋

[[case e of In_{1}^{i}(x_{11},…,x_{1n_{1}}) => e_{1} | ⋯ | In_{k}^{i}(x_{k1},…,x_{kn_{k}}) => e_{k}]]^{ml} ξ =

[[e]]^{ml} ξ ⋆ λs^{S^{i}}. case s of {ιIni_{1}(a_{1}, …, a_{n_{1}}) → [[e_{1}]]^{ml} ξ[x_{11} ↦ a_{1}, …, x_{1n_{1}} ↦ a_{n_{1}}] ⋮ ιIni_{k}(a_{1}, …, a_{n_{k}}) → [[e_{k}]]^{ml} ξ[x_{k1} ↦ a_{1}, …, x_{kn_{k}} ↦ a_{n_{k}}]

[[if e_{1} then e_{2} else e_{3}]]^{ml} ξ = [[e_{1}]]^{ml} ξ ⋆ λb^{𝔹}. case b of \begin{cases}tt & → [[e_{2}]]^{ml} ξ \\ ff & → [[e_{3}]]^{ml} ξ \end{cases}
[[let fun f (x:τ_{1}):τ_{2} = e_{1} in e_{2} end]]^{ml} ξ =

[[e_{2}]]^{ml} ξ[f ↦ fix(\underbrace{λθ^{[[[τ_{1}]]^{ml}→[[τ_{2}]]_{⊥}^{ml}]}.λa^{[[τ_{1}]]^{ml}}.[[e_{1}]]^{ml} ξ[f ↦ θ, x ↦ a]}_{Θ_{f}})]

Figure 2: Denotational semantics of the ML fragment.

where, for each dt^{i},

idt^{i} : S^{i} →^{≅} ([[τ_{11}^{i}]]^{ml} × ⋯ × [[τ_{1n_{1}}^{i}]]^{ml}) + ⋯ + ([[τ_{k1}^{i}]]^{ml} × ⋯ × [[τ_{kn_{k}}^{i}]]^{ml})

is a minimal-invariant solution to the evident predomain equation. We write

ιIni_{j}(a_{1}, …, a_{n}) = idt^{i}^{−1}(in_{j}(a_{1}, …, a_{n}))

for the constructor functions. Any element of S^{i} can thus be uniquely written as the image of a constructor function.

When all the τ_{··}^{i} (and hence also dt^{i}) are ground, the least solution S^{i} will again be a set (discrete cpo), and could be constructed using standard set-theoretic methods. In the general case, one must use, e.g., the domain-theoretic inverse-limit construction, straightforwardly adapted to predomains.

The meaning of ML expressions is defined by induction on the typing derivation; for conciseness we write only the expressions themselves. The semantics is structured such that if Γ ⊢ e : τ and for all (x_{i} : τ_{i}) ∈ Γ, ξ(x_{i}) ∈ [[τ_{i}]]^{ml}, then [[e]]^{ml} ξ ∈ [[τ]]_{⊥}^{ml}. The full semantics is shown in Figure 2

For notational convenience in the following, we will assume that all function names

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

Figure 3: The normalization algorithm, NORM.

f in a program are distinct. For a fixed program, we can then unambiguously use θ_{f} = fix(Θ_{f}) to refer to the denotation of f in the let fun-construct.

Evaluation semantics We say that a complete program is a closed expression of type τ_{1} -> τ_{2} -> ⋯ -> τ_{n} -> τ_{0} (n ≥ 0), where each τ_{i} is a ground type. For such types, let C_{τ} = [[τ]]^{ml} denote the set of values underlying τ, e.g., Cint = ℤ. A complete program e : τ_{1} -> τ_{2} -> ⋯ -> τ_{n} -> τ_{0} then determines a computable partial function e • (·) : C_{τ_{1}} × ⋯ × C_{τ_{n}} ⇀ C_{τ_{0}}, given, e.g., by

e • (c_{1}, …, c_{n}) = c_{0} iff (e \underline{c_{1}} ⋯ \underline{c_{n}}) ⇓^{ml} \underline{c_{0}} ,

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

Theorem 3 (computational adequacy of denotational semantics) For a complete ML program e, e • (c_{1}, …, c_{n}) = c_{0} iff [[e]]^{ml}∅ ⋆ λf_{1}. f_{1} c_{1} ⋆ ⋯ ⋆ λf_{n}.f_{n} c_{n} = ⌊c_{0}⌋.

Proof: Modulo trivial syntactic differences, an equivalent formulation of the semantics in terms of strict functions between pointed cpos, rather than general ones between cpos, and the obvious generalization to multiple (non-mutually recursive) datatypes, this is shown in, e.g., [Pit96, Section 5]. The primary difficulty is, of course, the definition of the logical relation at types dt^{i}, which is again achieved by exploiting the minimal-invariant properties of the (S^{i}, idt^{i}). □

4.2 The normalization algorithm

The concrete representation of the normalization algorithm, with many of the auxiliary definitions inlined, is shown in Figure 3. We have taken dt^{1} = term with three constructors In_{1}^{1} = VAR, In_{2}^{1} = LAM, and In_{3}^{1} = APP. Note that term is a ground type. To keep the notation concise, we assume that the chosen predomain-equation solution coincides exactly with our representation of terms, i.e., [[term]]^{ml} = Λ, ι_{LAM}(v, m) = LAM(v, m), etc. Similarly, we have instantiated dt^{2} as the type sem, with constructors TM and FUN. We write S = [[sem]]^{ml}, but here we do not a priori require that S_{⊥} = D_{r}.

Since ML is a call-by-value language, we must simulate the implicit call-by-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 as ML functions with source type unit -> sem. As an optimization, however, the strict function ↓ : D_{r} → Λ̂ is represented as simply an ML function on sem.

It is easy to check that the top-level expression, NORM : term -> term, is a welltyped complete program in our sense.

Examples The following examples illustrate how the program behaves. Let SA ≡ LAM(x, APP(VAR(x), VAR(x))) and Omega ≡ APP(SA, SA).

a. NORM • (Omega) diverges.

b. NORM • (APP(LAM(x, LAM(x, VAR(x))), Omega)) = LAM(g_{0}, VAR(g_{0})).

c. NORM • (LAM(y, LAM(g_{4}, VAR(z)))) = LAM(g_{0}, LAM(g_{1}, VAR(z))).

Let us now formally relate the abstract and concrete constructions. To obtain a perfect correspondence between semantic term generators and their implementation, we choose N = ℤ, with gen(n) = g\underline{n} = g_{n} when n ≥ 0, e.g., gen(13) = g13; then [[int->term]]^{ml} = Λ̂. Recall that we had D_{r} ≅ (Λ̂ + [D_{r} → D_{r}])_{⊥}, while [[sem]]^{ml} = S ≅ Λ̂ + [[1 → S_{⊥}] → S_{⊥}]. We can then show:

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

a. For all l ∈ Λ̂, i_{DS}(tm(l)) = ⌊ι_{TM}(l)⌋.

b. For all f ∈ [D_{r} → D_{r}], i_{DS}(fun(f)) = ⌊ι_{FUN}(λt^{[1→S_{⊥}]}. i_{DS}(f(i_{DS}^{−1}(t ∗))))⌋.

c. i_{DS}(⊥_{D_{r}}) = ⊥_{S_{⊥}}.

Proof: See Appendix B.1. □

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.

Proof: By fixed-point induction on Φ×Θ_{down} (where Φ is as in the proof of Lemma 8), using the predicate R ⊆ [D_{r} → Λ̂] × [S → Λ̂_{⊥}] defined by

R = {(φ, θ) | ∀d ∈ D_{r}, n ∈ ℤ. φ d n = i_{DS}(d) ⋆ λs^{S}.θ s ⋆ λlΛ̂.l n}.

We aim to establish that (fix(Φ), fix(Θ_{down})) ∈ R. It is straightforward to verify that R is pointed and inclusive. Assume that (φ, θ) ∈ R; we then must show that (Φ(φ), Θ_{down}(θ)) ∈ R. Accordingly, let arbitrary d and n be given, and consider d:

Case d = ⊥_{D_{r}}: By Lemma 12(c), i_{DS}(d) = ⊥_{S_{⊥}}, and so i_{DS}(d) ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λlΛ̂.l n = ⊥_{Λ_{⊥}}.

Similarly, Φ(φ) d n = ⊥Λ̂ n = ⊥_{Λ_{⊥}}.

Case d = tm(l): Let ξ = ∅[down ↦ θ, s ↦ ι_{TM}(l)]; we calculate:

i_{DS}(d) ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λlΛ̂.l n = i_{DS}(tm(l)) ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λlΛ̂.l n = ⌊ι_{TM}(l)⌋ ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λlΛ̂.l n (by Lemma 12(a)) = Θ_{down}(θ) (ι_{TM}(l)) ⋆ λlΛ̂.l n

= [[fn n => (case s of TM l => l n | ...)]]^{ml} ξ ⋆ λlΛ̂.l n

= [[l n]]^{ml} ξ[n ↦ n, l ↦ l] = l n

Similarly, Φ(φ) d n = Φ(φ)(tm(l)) n = l n.

Case d = fun(f): Let ξ = ∅[down ↦ θ, s ↦ ι_{FUN}(λt. i_{DS}(f(i_{DS}^{−1}(t ∗))))] and let ξ′ =

ξ[n ↦ n, f ↦ (λt. i_{DS}(f(i_{DS}^{−1}(t ∗))))]; again, i_{DS}(d) ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λlΛ̂.l n = i_{DS}(fun(f)) ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λlΛ̂.l n = ⌊ι_{FUN}(λt. i_{DS}(f(i_{DS}^{−1}(t ∗))))⌋ ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λlΛ̂.l n (by Lemma 12(b))

= [[fn n => (case s of ...| FUN f => LAM ...)]]^{ml} ξ ⋆ λlΛ̂.l n
= [[LAM("g"^Int.toString(n), down (f (fn () => ...)) (n+1))]]^{ml} ξ′

= [[down (f (fn () => ...)) (n+1)]]^{ml} ξ′ ⋆ λm^{Λ}.⌊LAM(g_{n}, m)⌋

= \underbrace{[[f (fn () => ...)]]^{ml} ξ′}_{s′} ⋆ λs^{S}.θ s ⋆ λlΛ̂.l(n + 1) ⋆ λm^{Λ}.⌊LAM(g_{n}, m)⌋

Now, s′

= [[f (fn () => TM(fn n' => VAR("g"^Int.toString(n))))]]^{ml} ξ′

= ⌊(λt. i_{DS}(f(i_{DS}^{−1}(t ∗))))⌋ ⋆ λg.⌊λu.[[TM(fn ...)]]^{ml} ξ′⌋ ⋆ λa.g a = i_{DS}(f(i_{DS}^{−1}(⌊ι_{TM}(λn^{′ℤ}.⌊VAR(g_{n})⌋)⌋))) = i_{DS}(f(tm(λn^{′ℤ}.⌊VAR(g_{n})⌋))) (by Lemma 12(a)) = i_{DS}(f(↑ ({ \atop VAR}(g_{n})))) (by Def. of { \atop VAR} and ↑)

Now, the IH that (φ, θ) ∈ R says that ∀d′, n′. φ d′ n′ = i_{DS}(d′) ⋆ λs^{S}.θ s⋆λlΛ̂.l n′. Taking d′ = f(↑ ({ \atop VAR}(g_{n}))) and n′ = n + 1, we continue the original calculation:

[[f (fn () => ...)]]^{ml} ξ′ ⋆ λs^{S}.θ s ⋆ λlΛ̂.l(n + 1) ⋆ λm^{Λ}.⌊LAM(g_{n}, m)⌋ = i_{DS}(f(↑ ({ \atop VAR}(g_{n})))) ⋆ λs^{S}.θ s ⋆ λlΛ̂.l(n + 1) ⋆ λm^{Λ}.⌊LAM(g_{n}, m)⌋ = φ(f(↑ ({ \atop VAR}(g_{n})))) (n + 1) ⋆ λm^{Λ}.⌊LAM(g_{n}, m)⌋ (by IH)

Similarly, Φ(φ) d n = Φ(φ)(fun(f)) n

= { \atop LAM}(λx^{V}. φ(f(↑ ({ \atop VAR}(x))))) n

= φ(f(↑ ({ \atop VAR}(g_{n})))) (n + 1) ⋆ λm^{Λ}. ⌊LAM(g_{n}, m)⌋ (by Def. of { \atop LAM}) □

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

Proof: By structural induction on m. Let m, ρ and ϱ be given such that ∀x ∈ F V (m).i_{DS}(ρ(x)) = ϱ(x). Let ξ = ∅[down ↦ θ_{down}]. By the fixed-point equation, since

θ_{eval} = fix(Θ_{eval}),

θ_{eval} m ⋆ λg.g ϱ = Θ_{eval}(θ_{eval}) m ⋆ λg.g ϱ

= [[fn p => (case m of ...)]]^{ml} ξ[eval ↦ θ_{eval}, m ↦ m] ⋆ λg.g ϱ
= [[case m of ...]]^{ml} ξ[eval ↦ θ_{eval}, m ↦ m, p ↦ ϱ]

Let ξ′ = ξ[eval ↦ θ_{eval}, m ↦ m, p ↦ ϱ]. Consider m:

Case m = VAR(x): Then, θ_{eval} m ⋆ λg.g ϱ

= [[case m of VAR x => p x | ...]]^{ml} ξ′

= [[p x]]^{ml} ξ′[x ↦ x] = ϱ(x)

Since clearly x ∈ F V (m), we have i_{DS}(ρ(x)) = ϱ(x) by assumption on ρ and ϱ. Thus similarly,

i_{DS}([[m]]_{r} ρ) = i_{DS}([[VAR(x)]]_{r} ρ) = i_{DS}(ρ(x)) = ϱ(x)

Case m = LAM(x, m_{0}): Let ξ′′ = ξ′[x ↦ x, m0 ↦ m_{0}]. Then, θ_{eval} m ⋆ λg.g ϱ

= [[case m of ... | LAM(x,m0) => FUN(...) | ...]]^{ml} ξ′
= [[FUN(fn d => eval m0 (...))]]^{ml} ξ′′

= ⌊ι_{FUN}(λt^{1→S_{⊥}}.[[eval m0 (fn x' => if ...)]]^{ml} ξ′′[d ↦ t])⌋

= ⌊ι_{FUN}(\underbrace{λt.θ_{eval} m_{0} ⋆ λg.g (λx^{′V}.[[if ...]]^{ml} ξ′′[d ↦ t, x' ↦ x′])}_{f})⌋

Similarly, i_{DS}([[m]]_{r} ρ) = i_{DS}([[LAM(x, m_{0})]]_{r} ρ) = i_{DS}(ϕ_{r}(λd^{D_{r}}.[[m_{0}]]_{r} ρ[x ↦ d])) = i_{DS}(fun(λd^{D_{r}}.[[m_{0}]]_{r} ρ[x ↦ d])) = ⌊ι_{FUN}(λt.i_{DS}((λd^{D_{r}}.[[m_{0}]]_{r} ρ[x ↦ d]) (i_{DS}^{−1}(t ∗))))⌋ (by Lemma 12(b))

= ⌊ι_{FUN}(\underbrace{λt.i_{DS}([[m_{0}]]_{r} ρ[x ↦ i_{DS}^{−1}(t ∗)])}_{f′})⌋

It remains now to prove that f = f′. Let any t′ : 1 → S_{⊥} be given.

Let ρ_{0} = ρ[x ↦ i_{DS}^{−1}(t′ ∗)] and ϱ_{0} = (λx^{′V}.[[if ...]]^{ml} ξ′′[d ↦ t′, x' ↦ x′]). First we verify that ρ_{0} and ϱ_{0} satisfy the requirements of the IH for m_{0}, namely that for all x′ ∈ F V (m_{0}) ⊆ {x} ∪ F V (m), i_{DS}(ρ_{0}(x′)) = ϱ_{0}(x′). This is straightforward; first for x′ = x:

ϱ_{0}(x)

= [[if x=x' then d () else p x']]^{ml} ξ′′[d ↦ t′, x' ↦ x]

= t′ ∗ = i_{DS}(i_{DS}^{−1}(t′ ∗)) = i_{DS}(ρ_{0}(x))

Then for any x′′ ∈ F V (m_{0}) \ {x}:

ϱ_{0}(x′′)

= [[if x=x' then d () else p x']]^{ml} ξ′′[d ↦ t′, x' ↦ x′′]

= ϱ(x′′) = i_{DS}(ρ(x′′)) (by assumption on ρ and ϱ) = i_{DS}(ρ_{0}(x′′))

Hence, f t′ = θ_{eval} m_{0} ⋆ λg.g ϱ_{0} = i_{DS}([[m_{0}]]_{r} ρ_{0}) (by IH on m_{0}) = f′ t′

Since t′ was arbitrary, f = f′.

Case m = APP(m_{1}, m_{2}): Let ξ′′ = ξ′[m1 ↦ m_{1}, m2 ↦ m_{2}]. Then, θ_{eval} m ⋆ λg.g ϱ

= [[case m of ... | APP(m1,m2) => (case ...)]]^{ml} ξ′
= [[case (eval m1 p) of ...]]^{ml} ξ′′

Now, [[eval m1 p]]^{ml} ξ′′ = θ_{eval} m_{1} ⋆ λg.g ϱ = i_{DS}([[m_{1}]]_{r} ρ) (by IH on m_{1})

Consider [[m_{1}]]_{r} ρ:

Case [[m_{1}]]_{r} ρ = ⊥_{D_{r}}: Then by Lemma 12(c) also i_{DS}([[m_{1}]]_{r} ρ) = ⊥, and so θ_{eval} m⋆ λg.g ϱ = ⊥_{S_{⊥}}. Similarly,

i_{DS}([[m]]_{r} ρ)

= i_{DS}([[APP(m_{1}, m_{2})]]_{r} ρ)

= i_{DS}(ψ_{r}(⊥_{D_{r}})([[m_{2}]]_{r} ρ))

= i_{DS}(⊥_{[D_{r}→D_{r}]} ([[m_{2}]]_{r} ρ))

= i_{DS}(⊥_{D_{r}})

= ⊥_{S_{⊥}}

Case [[m_{1}]]_{r} ρ = tm(l_{1}): Then, θ_{eval} m ⋆ λg.g ϱ

= [[case (eval m1 p) of TM l => TM(fn n ...) | ...]]^{ml} ξ′′
= [[TM(fn n => APP (...))]]^{ml} ξ′′[l ↦ l_{1}]

= ⌊ι_{TM}(\underbrace{λn^{ℤ}.[[APP(l n, down (eval m2 p) n)]]^{ml} ξ′′[l ↦ l_{1}, n ↦ n]}_{l})⌋

Similarly, i_{DS}([[m]]_{r} ρ) = i_{DS}([[APP(m_{1}, m_{2})]]_{r} ρ) = i_{DS}(ψ_{r} (tm(l_{1})) ([[m_{2}]]_{r} ρ))

= i_{DS}(↑ { \atop APP}(l_{1}, ↓ ([[m_{2}]]_{r} ρ)))

= i_{DS}(tm({ \atop APP}(l_{1}, ↓ ([[m_{2}]]_{r} ρ)))) (by Def. of ↑) = ⌊ι_{TM}({ \atop APP}(l_{1}, ↓ ([[m_{2}]]_{r} ρ)))⌋ (by Lemma 12(a))

= ⌊ι_{TM}(\underbrace{λn^{ℤ}.l_{1} n ⋆ λm′_{1}.↓ ([[m_{2}]]_{r} ρ) n ⋆ λm′_{2}.⌊APP(m′_{1}, m′_{2})⌋}_{l′})⌋

Again, it remains to show that l = l′. Let any n ∈ ℤ be given. Let ξ′′′ = ξ′′[l ↦ l_{1}, n ↦ n]; we calculate:

l n

= [[APP(l n, down (eval m2 p) n)]]^{ml} ξ′′′

= l_{1} n ⋆ λm′_{1}. [[down (eval m2 p)]]^{ml} ξ′′′ ⋆ λl_{2}. l_{2} n ⋆ λm′_{2}. ⌊APP(m′_{1}, m′_{2})⌋ = l_{1} n ⋆ λm′_{1}. θ_{eval} m_{2} ⋆ λg. g ϱ ⋆ λs. θ_{down} s ⋆ λl_{2}. l_{2} n ⋆ λm′_{2}. ⌊APP(m′_{1}, m′_{2})⌋ = l_{1} n ⋆ λm′_{1}. i_{DS}([[m_{2}]]_{r} ρ) ⋆ λs. θ_{down} s ⋆ λl_{2}. l_{2} n ⋆ λm′_{2}. ⌊APP(m′_{1}, m′_{2})⌋

(by IH on m_{2})

= l_{1} n ⋆ λm′_{1}. ↓ ([[m_{2}]]_{r} ρ) n ⋆ λm′_{2}. ⌊APP(m′_{1}, m′_{2})⌋ (by Lemma 13) = l′ n

Since n was arbitrary, l = l′. Case [[m_{1}]]_{r} ρ = fun(f): Then by Lemma 12(b), we have i_{DS}([[m_{1}]]_{r} ρ) =

⌊ι_{FUN}(λt^{1→S_{⊥}}. i_{DS}(f(i_{DS}^{−1}(t ∗))))⌋. Thus,

θ_{eval} m ⋆ λg.g ϱ

= [[case (eval m1 p) of ... | FUN f => f (fn ...)]]^{ml} ξ′′

= [[f (fn () => eval m2 p)]]^{ml} ξ′′[f ↦ (λt.i_{DS}(f(i_{DS}^{−1}(t ∗))))]) = (λt.i_{DS}(f(i_{DS}^{−1}(t ∗)))) (λu.θ_{eval} m_{1} ⋆ λg. g ϱ) = (λt.i_{DS}(f(i_{DS}^{−1}(t ∗)))) (λu.i_{DS}([[m_{2}]]_{r} ρ)) (By IH on m_{2}) = i_{DS}(f ([[m_{2}]]_{r} ρ))

Similarly, i_{DS}([[m]]_{r} ρ) = i_{DS}([[APP(m_{1}, m_{2})]]_{r} ρ) = i_{DS}(ψ_{r}(fun(f)) ([[m_{2}]]_{r} ρ)) = i_{DS}(f ([[m_{2}]]_{r} ρ))

□

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

Proof: Let m be given, and let ξ = ∅[down ↦ θ_{down}, eval ↦ θ_{eval}, norm ↦ θ_{norm}, m ↦ m]. Let further ⌊ϱ⌋ = [[fn x => TM(fn n => VAR(x))]]^{ml} ξ and ρ = (λx^{V}.↑ ({ \atop VAR}(x))).

We first verify that ϱ and ρ satisfy the requirements of Lemma 14, namely that for all x′ ∈ V ⊃ F V (m),

ϱ(x′)

   = [[fn x => TM(fn n => VAR(x))]]^{ml} ξ ⋆ λf.f(x′)
   = [[TM(fn n => VAR(x))]]^{ml} ξ[x ↦ x′]

= ⌊ι_{TM}(λn^{ℤ}.⌊VAR(x′)⌋)⌋

= ⌊ι_{TM}({ \atop VAR}(x′))⌋ (by Def. of { \atop VAR}) = i_{DS}(tm({ \atop VAR}(x′))) (by Lemma 12(a)) = i_{DS}(↑ ({ \atop VAR}(x′))) (by Def. of ↑) = i_{DS}(ρ(x′))

Hence, by a single unrolling of the fixed-point equation θ_{norm} = Θ_{norm}(θ_{norm}),

   θ_{norm} m
   = [[down (eval m (fn x => TM(fn n => VAR(x)))) 0]]^{ml} ξ
   = [[eval m (fn x => TM(fn n => VAR(x)))]]^{ml} ξ ⋆ λs.θ_{down} s ⋆ λl.l 0

= θ_{eval} m ⋆ λg.g ϱ ⋆ λs.θ_{down} s ⋆ λl.l 0

= i_{DS}([[m]]_{r} ρ) ⋆ λs.θ_{down} s ⋆ λl.l 0 (by Lemma 14) = ↓ ([[m]]_{r} ρ) 0 (by Lemma 13) = norm(m) (by Def. of norm)

□

Theorem 4 (implementation correctness) The program NORM satisfies that for all m, m′ ∈ Λ, NORM • (m) = m′ ⇔ norm(m) = ⌊m′⌋.

Proof: A direct consequence of Lemma 15 and Theorem 3, since [[NORM]]^{ml} ∅ = ⌊θ_{norm}⌋. □

Together with semantic correctness (Theorem 2) and Definition 2 of norm, this tells us that NORM correctly computes the normal form of all λ-terms without free occurrences of g\underline{i}-variables (including, in particular, all closed terms).

5 A generalization to Böhm trees

Recall that the correctness of our normalization algorithm was expressed in terms of simple conditionals. Soundness was, essentially, “if the algorithm returns a result, that result is correct”; and completeness, “if a correct result exists, the algorithm will find one”. We now set out to extend these statements to a more general notion of normal forms, effectively replacing “if” with “to the extent that”.

5.1 From λ-terms to λ-trees

We adopt a new view of normalization results, generalizing the flat domain Λ_{⊥} of lifted λ-terms to a more elaborate domain of lazy λ-trees, which will allow us to talk formally about partial and infinite terms. The intended reading of a λ-tree result is that the finitely reachable, defined parts of the tree represent committed output from the normalizer.

Syntax Let \underline{Λ} be the cpo of λ-trees M, defined as a minimal-invariant solution to the recursive domain equation

i\underline{Λ} : \underline{Λ} →^{≅} (V + V × \underline{Λ} + \underline{Λ} × \underline{Λ})_{⊥} ,

with the constructors for \underline{Λ}-elements given by:

□ = i−1 ; \underline{Λ}(⊥)_{\underline{VAR}(x) = i−1 ; \underline{Λ}(⌊in_{1}(x)⌋)} \underline{LAM}(x, M_{0}) = i−1 ; \underline{Λ}(⌊in_{2}(x, M_{0})⌋)

\underline{APP}(M_{1}, M_{2}) = i−1 ; \underline{Λ}(⌊in_{3}(M_{1}, M_{2})⌋)

Again, any element of \underline{Λ} can be uniquely written as one of these four forms.

We also have a natural interpretation of the domain-theoretic ordering on \underline{Λ}: M ⊑ M′ precisely when M′ can be obtained by replacing some occurrences of □ in M with suitable subtrees. Note that, since \underline{Λ} is a cpo, it necessarily also contains infinite trees, such as ⨆_{n∈ω} \underline{LAM}(x_{1}, ⋯ \underline{LAM}(x_{n}, □)) = \underline{LAM}(x_{1}, \underline{LAM}(x_{2}, ⋯)).

We define the cut function |·|^{·} : \underline{Λ} × ω → \underline{Λ} by induction on k:

|M|^{0} = □  |□|^{k+1} = □  |\underline{VAR}(x)|^{k+1} = \underline{VAR}(x)

|\underline{LAM}(x, M_{0})|^{k+1} = \underline{LAM}(x, |M_{0}|^{k}) |\underline{APP}(M_{1}, M_{2})|^{k+1} = \underline{APP}(|M_{1}|^{k}, |M_{2}|^{k})

That is, |M|^{k} replaces all parts of the tree M above height k with □. As we would expect, every tree is the limit of its finite cuts:

Lemma 16 For any M ∈ \underline{Λ}, M = ⨆_{k∈ω} |M|^{k}.

Proof: The function δ : [\underline{Λ} → \underline{Λ}] → [\underline{Λ} → \underline{Λ}] associated to the domain equation is given by

δ(e)(M) = case M of \begin{cases}\underline{VAR}(v) & → \underline{VAR}(v) \\ \underline{LAM}(v, M_{0}) & → \underline{LAM}(v, e M_{0}) \\ \underline{APP}(M_{1}, M_{2}) & → \underline{APP}(e M_{1}, e M_{2}) \\ □ & → □ \end{cases}

It is easy to check, by induction on k, that |M|^{k} = δ^{k}(⊥_{[\underline{Λ}→\underline{Λ}]})(M). Hence, by the minimal-invariant property, ⨆_{k∈ω} |M|^{k} = ⨆_{k∈ω} δ^{k}(⊥) M = (⨆_{k∈ω} δ^{k}(⊥)) M = fix(δ)(M) = id\underline{Λ} M = M. □

A tree is called finite if it is equal to one of its cuts, and total if it contains no □. Thus, finite, total λ-trees are in one-to-one correspondence with ordinary λ-terms, as previously defined. We also have a natural inclusion of ordinary λ-terms into λ-trees, ⟨·⟩ : Λ → \underline{Λ}, defined inductively in the obvious way.

Compatibility We can extend any predicate on λ-terms, P ⊆ Λ, to a corresponding predicate on λ-trees, P^{†} ⊆ \underline{Λ}, by

P^{†} = \{M ∈ \underline{Λ} | ∀k ∈ ω. ∃m ∈ P. |M|^{k} ⊑ ⟨m⟩\} .

That is, M ∈ P^{†} if every finite cut of M can be increased to a total tree, satisfying the original predicate. When a tree already represents a proper term, the extension has no effect: ⟨m⟩ ∈ P^{†} iff m ∈ P. We also note that P^{†} is downward closed: if M ∈ P^{†} and M′ ⊑ M, then also M′ ∈ P^{†}; and that extension is monotone: if P ⊆ P′, then P^{†} ⊆ P^{′†}.

Definition 5 For M ∈ \underline{Λ} and m ∈ Λ^{Δ}, we define the compatibility relations ↔^{†} and ↔_{Δ}^{†} by

M ↔^{†} m ⇔ M ∈ {m′ ∈ Λ | m′ ↔ m}^{†}
M ↔_{Δ}^{†} m ⇔ M ∈ {m′ ∈ Λ^{Δ} | m′ ↔ m}^{†}

Note that, like convertibility, compatibility is defined with respect to concrete terms, not α-equivalence classes. Thus,

\underline{LAM}(g_{0}, \underline{LAM}(g_{0}, □)) ↔^{†} LAM(x, LAM(y, VAR(y)))

(because the □ can still be increased to \underline{VAR}(g_{0}), making the two sides convertible), but we do not have

\underline{LAM}(g_{0}, \underline{LAM}(g_{0}, □)) ↔^{†} LAM(x, LAM(y, VAR(x))) .

Böhm trees We can view Böhm trees [Bar84, Chapter 10] as a particular kind of λ-trees. Informally, a Böhm tree is either □, or a generalized head normal form,

\underline{LAM}(x_{1}, ⋯ \underline{LAM}(x_{n}, \underline{APP}(\underline{APP}(\underline{VAR}(x), M_{1}), ⋯ M_{m}))) ,

where n, m ≥ 0, and each M_{i} is itself a Böhm tree. However, we need to make precise how this evidently circular definition is to be interpreted.

Formally, we define Böhm trees in terms of the following rules:

\overline{⊢_{bt} □} (BT-□)

\frac{⊢_{nf} M}{⊢_{bt} M} (BT-nf)

\frac{⊢_{at} M}{⊢_{nf} M} (NF-at)

\frac{⊢_{nf} M_{0}}{⊢_{nf} \underline{LAM}(x, M_{0})} (NF-lam)

\overline{⊢_{at} \underline{VAR}(x)} (AT-var)

\frac{⊢_{at} M_{1} ⊢_{bt} M_{2}}{⊢_{at} \underline{APP}(M_{1}, M_{2})} (AT-app)

These rules determine an operator F on subsets of B = \{bt, nf, at\} × \underline{Λ}, where F (X) is the set of conclusions occurring in rule instances with premises from X:

F (X) = \{(bt, □)\} ∪ ⋯ ∪ \{(at, \underline{APP}(M_{1}, M_{2})) | (at, M_{1}) ∈ X ∧ (bt, M_{2}) ∈ X\} .

F is clearly monotone, i.e., X ⊆ X′ ⇒ F (X) ⊆ F (X′). We say that a set X ⊆ B is F -closed if F (X) ⊆ X, i.e., if everything derivable by the rule instances with premises from X, is already in X.

When X is inclusive, so is F (X), because inclusiveness is preserved by finite unions, and the constructor functions (as well as pairing with constants) are order-monics, i.e., also reflect ⊑, so their direct images preserve inclusiveness.

Since both subsets of B and inclusive subsets of B are closed under arbitrary intersections, they each form complete lattices. Thus, by the Knaster-Tarski fixedpoint theorem, we get the least F -closed set B^{fin} ⊆ B by taking the intersection over all F -closed subsets of B, and the least F -closed inclusive set B^{inf} ⊆ B as the intersection of all F -closed inclusive subsets of B.

The associated rule induction principles are: if a predicate P on B is F -closed, then B^{fin} ⊆ P (since B^{fin} was the least F -closed set). Analogously, if P is both F - closed and inclusive, then B^{inf} ⊆ P. As special cases we get inversion principles:

B^{fin} = F (B^{fin}) and B^{inf} = F (B^{inf}), i.e., every element of either set can be written as the conclusion of a rule with premises in the corresponding set. Naturally, B^{fin} ⊆ B^{inf}, because B^{fin} is the least of all fixed points of F.

We write B_{s}^{fin} for {M | (s, M) ∈ B^{fin}}, and analogously for B_{s}^{inf}. The set of Böhm trees is then defined to be B_{bt}^{inf}; the finite Böhm trees are B_{bt}^{fin}.

(Note, incidentally, that Böhm trees are not simply the uniform extension of finite normal forms to λ-trees, N_{nf}^{†}. The latter (which could be called infinitary normal forms) are merely the λ-trees that do not contain any evident β-redexes. We thus have B_{bt}^{inf} ⊆ N_{nf}^{†}, but the opposite inclusion does not hold: infinitary normal forms include non-Böhm trees, such as \underline{LAM}(x, □) or \underline{APP}(\underline{APP}(⋯, x), x).

Nor should B_{bt}^{inf} be confused with the set of trees determined by a coinductive reading of the above rules, i.e., the greatest fixed point of F. That set still contains, e.g., the tree \underline{LAM}(x_{0}, \underline{LAM}(x_{1}, ⋯)). Even though we allow Böhm trees to be infinite, each run of curried abstractions or applications must be finite, like in the inductive reading of the rules.)

Again, we expect that a reduction-free Böhm normalizer will output Böhm trees that are compatible with the input term (soundness); that convertible inputs are mapped to the same Böhm tree (identification); and that the output tree is as large as possible (completeness).

5.2 A semantic Böhm-tree construction

The modularity of output-term generation, originally motivated by flexible generation of fresh names, also allows us to “locally” re-target the existing normalization construction to Böhm trees.

Output-tree generation For any f : A → B, where A and B are pointed cpos, we define its smashed strict extension, · ⊙ ⋆ f : A → B, by ⊥_{A} ⊙ ⋆ f = ⊥_{B}, and a ⊙ ⋆ f = f(a) otherwise.

We first define tree-based analogs of the wrapper functions from Section 2.2, again using de Bruijn-level naming:

Definition 6 (cf. Definition 1) Let Λ̂ = [N → \underline{Λ}], and define

{ \atop VAR}(v) = λn^{N}. \underline{VAR}(v)
{ \atop LAM}(f) = λn^{N}. f (gen(n)) (n + 1) ⊙ ⋆ λM\underline{Λ} 0. \underline{LAM}(gen(n), M_{0})
{ \atop APP}(l_{1}, l_{2}) = λn^{N}. l_{1} n ⊙ ⋆ λM\underline{Λ} 1. \underline{APP}(M_{1}, l_{2} n)

Note that { \atop APP} is strict in its first argument only. Making it strict in both, would revert the normalizer to always produce either □ or a finite, total λ-tree as the result, just like the original version. Strictness in the first argument does not actually matter, since the function will never be applied to a □-representative; however, from an operational viewpoint, it is convenient to know that it is safe to evaluate the argument eagerly. Making { \atop LAM} non-strict would not affect correctness with respect to compatibility, but the output would no longer necessarily be a Böhm tree.

The residualizing model The construction of the residualizing model from Section 2.3 can be reused verbatim, since it only relies on Λ̂ being a pointed cpo with continuous wrapper functions. Only the codomain of the putative Böhm normalizer changes:

Definition 7 (cf. Definition 2) For any Δ, we define the function bt_{Δ} : Λ^{Δ} → \underline{Λ} by

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

Again, we write just bt : Λ → \underline{Λ} for the variant where ♯Δ is replaced with 0, noting that it agrees with bt_{Δ} whenever Δ ∩ G = ∅.

5.3 Correctness of the construction

The proof proceeds very much like in the original, finitary case.

Basic results about compatibility

Lemma 17 P^{†} is inclusive for any P.

Proof: We need to show that ∀k ∈ ω. ∃m ∈ P. |M|^{k} ⊑ ⟨m⟩ is an inclusive predicate in M. By closure under intersections, it is enough to consider a fixed k. But, for any chain (M_{i})_{i∈ω}, there must be an i_{0} such that ∀i ≥ i_{0}.|M_{i}|^{k} = |M_{i_{0}}|^{k}. Hence, if M_{i_{0}} ∈ P^{†}, the m ∈ P such that |M_{i_{0}}|^{k} ⊑ ⟨m⟩ will also work for all subsequent i, and thus also for ⨆_{i∈ω} M_{i}. □

Lemma 18 The constructor functions preserve compatibility:

a. For all m and Δ, □ ↔_{Δ}^{†} m.

b. If v ∈ Δ, then \underline{VAR}(v) ↔_{Δ}^{†} VAR(v).

c. If M ↔_{Δ∪\{v\}}^{†} m, then \underline{LAM}(v, M) ↔_{Δ}^{†} LAM(v, m).

d. If M_{1} ↔_{Δ}^{†} m_{1} and M_{2} ↔_{Δ}^{†} m_{2}, then \underline{APP}(M_{1}, M_{2}) ↔_{Δ}^{†} APP(m_{1}, m_{2}).

Proof: Straightforward. Part (a) uses that □ is the least element in \underline{Λ} and that ↔ is reflexive; part (b) uses that both ⊑ and ↔ are reflexive; parts (c) and (d) use that \underline{LAM}(v, ·) and \underline{APP}(·, ·) are monotonic and that ↔ is a congruence wrt. LAM and APP, respectively. □

Correctness of the wrappers

Definition 8 (cf. Definition 3) For l ∈ Λ̂, m ∈ Λ^{Δ}, and s ∈ {nf, at}, we define the representation relation ⪅ by

l ⪅_{s}^{Δ} m iff ∀n ≥ ♯Δ. l n ↔_{Δ}^{†} m ∧ (l n = □ ∨ l n ∈ B_{s}^{inf}) .

The correctness of the wrappers will need to be established with respect to the new definition of ⪅. The original “interface” lemmas of ⪅ (Lemmas 3, 4, and 5) can actually be restated verbatim – this considerably simplifies establishing soundness. Of course, the underlying meanings, and hence the proofs, of the Lemmas do change, according to the new definitions for the Böhm-tree construction.

Lemma 19 (cf. Lemma 3) For fixed Δ, s, and m, the predicate P = {l | l ⪅_{s}^{Δ} m} is pointed and inclusive.

Proof: Pointedness is immediate. Inclusiveness also follows directly, since the relation is defined in terms of universal quantification, conjunction, finite disjunction, and inverse image by the (continuous) application function from the inclusive predicates ↔_{Δ}^{†} (by Definition 5 and Lemma 17) and B_{s}^{inf} (by construction). □

Lemma 20 (cf. 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: The proof is analogous to that of Lemma 4, with part (a) now exploiting monotonicity of predicate extension: when n ≥ ♯Δ′ ≥ ♯Δ, l n ∈ {m′ ∈ Λ^{Δ} | m′ ↔ m}^{†} ⊆ {m′ ∈ Λ^{Δ′} | m′ ↔ m}^{†}. Part (b) just uses transitivity of ↔, like in the original proof. □

Lemma 21 (cf. 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: In each case, assume that an arbitrary n ≥ ♯Δ is given. Then the proofs for each case proceed as follows:

a. Let arbitrary v ∈ Δ be given. Then { \atop VAR}(v) n = \underline{VAR}(v). The first conjunct in ⪅ then follows from Lemma 18(b), and the second by Rule AT-var.

b. Assume that l_{1} ⪅_{at}^{Δ} m_{1} and l_{2} ⪅_{nf}^{Δ} m_{2}. Let further M_{1} = l_{1} n and M_{2} = l_{2} n. Consider M_{1}. If M_{1} = □, then { \atop APP}(l_{1}, l_{2}) n = □; thus, the first conjunct holds by Lemma 18(a), and the second by its left disjunct.

If M_{1} ≠ □, then { \atop APP}(l_{1}, l_{2}) n = \underline{APP}(M_{1}, M_{2}). By definition of ⪅ for l_{1}, M_{1} ↔_{Δ}^{†} m_{1} and M_{1} ∈ B_{at}^{inf}. Analogously, M_{2} ↔_{Δ}^{†} m_{2} and M_{2} = □ ∨ M_{2} ∈ B_{nf}^{inf}. Since these two possibilities correspond to Rules BT-□ and BT-nf, we have M_{2} ∈ B_{bt}^{inf}. And thus, \underline{APP}(M_{1}, M_{2}) ↔_{Δ}^{†} APP(m_{1}, m_{2}) follows from Lemma 18(d), and \underline{APP}(M_{1}, M_{2}) ∈ B_{at}^{inf} by Rule AT-app.

c. Immediate, by Rule NF-at. d. Let f, x, and m, satisfy the condition of the lemma, and let M_{0} = f g_{n} (n +

1). Consider M_{0}. If M_{0} = □, then { \atop LAM}(f) n = □, so the first conjunct of { \atop LAM}(f) ⪅_{nf}^{Δ} LAM(x, m) holds by Lemma 18(a), and the second by its left disjunct.

If M_{0} ≠ □, then { \atop LAM}(f) n = \underline{LAM}(g_{n}, M_{0}). By definition of ♯Δ, g_{n} ∉ Δ, and so by assumption on f, f g_{n} ⪅_{nf}^{Δ∪{g_{n}}} m[VAR(g_{n})/x]. Thus, since n + 1 ≥ ♯(Δ ∪ {g_{n}}), the definition of ⪅ gives us that

M_{0} ↔_{Δ∪{g_{n}}}^{†} m[VAR(g_{n})/x] ∧ M_{0} ∈ B_{nf}^{inf}.

By Lemma 18(c), \underline{LAM}(g_{n}, M_{0}) ↔_{Δ}^{†} LAM(g_{n}, m[VAR(g_{n})/x]). Now, since g_{n} ∉ Δ ensures that g_{n} ∉ F V (m) \ {x}, LAM(g_{n}, m[VAR(g_{n})/x]) ↔ LAM(x, m) is a valid α-conversion. By construction of ↔_{Δ}^{†} (Definition 5) and transitivity of ↔, also \underline{LAM}(g_{n}, M_{0}) ↔_{Δ}^{†} LAM(x, m). Finally, from M_{0} ∈ B_{nf}^{inf}, we get \underline{LAM}(g_{n}, M_{0}) ∈ B_{nf}^{inf} by Rule NF-lam.

□

Adequacy of the residualizing model By virtue of the above “interface” lemmas, the verbatim insertion of Lemmas 6, 7, 8, and 9 and their proofs remain correct with the Böhm tree definitions, modulo a simple substitution of references to Lemmas 3–5 with references to Lemmas 19–21, respectively.

Correctness of the Böhm-tree normalization function The key technical property of Böhm trees we will need for the completeness result, is that any finite cut of a Böhm tree can be extended to a finite Böhm tree, still approximating the original one. Thus, it will suffice to consider only approximants of the output term that are themselves Böhm trees.

Definition 9 For any Böhm tree M ∈ B_{bt}^{inf}, and k ∈ ω, we define the Böhm cut ∥M∥^{k} by induction on k, as follows:

∥M∥^{0} = □  ∥□∥^{k+1} = □  ∥\underline{VAR}(x)∥^{k+1} = \underline{VAR}(x)
∥\underline{LAM}(x, M_{0})∥^{k+1} = ∥M_{0}∥^{k} ⊙ ⋆ λM′_{0}. \underline{LAM}(x, M′_{0})
∥\underline{APP}(M_{1}, M_{2})∥^{k+1} = ∥M_{1}∥^{k} ⊙ ⋆ λM′_{1}. \underline{APP}(M′_{1}, ∥M_{2}∥^{k})

Intuitively, ∥M∥^{k} is the largest (necessarily finite) Böhm tree such that ∥M∥^{k} ⊑ |M|^{k}. It is constructed by cutting off branches early, if they do not reach a complete Böhmsubtree within the remaining height limit.

Lemma 22 Böhm cuts satisfy:

a. ∀k. ∥M∥^{k} ∈ B_{bt}^{fin}.

b. ∀k. ∥M∥^{k} ⊑ |M|^{k}.

c. ∀k. ∃k′. |M|^{k} ⊑ ∥M∥^{k′}.

(These are the only properties of ∥M∥^{k} that we will subsequently use.)

Proof: We prove (a) and (b) together by, induction on k. (They could also have been proven separately). The strengthened induction hypothesis is

P (k) ⇔ ∀(s, M) ∈ B^{inf}. (∥M∥^{k} ∈ B_{s}^{fin} ∨ ∥M∥^{k} = □) ∧ ∥M∥^{k} ⊑ |M|^{k}.

All parts of P (0) are immediate. For the inductive step, we assume P (k) and aim to show P (k + 1). Let M ∈ B_{s}^{inf}; we distinguish cases on M:

Case M = □: All parts are trivial.

Case M = \underline{VAR}(x): Then ∥M∥^{k+1} = \underline{VAR}(x), which belongs to all of B_{at}^{fin}, B_{nf}^{fin}, and B_{bt}^{fin}; and \underline{VAR}(x) = |\underline{VAR}(x)|^{k+1}.

Case M = \underline{LAM}(x, M_{0}): By the inversion principle for B^{inf}, M ∈ B_{bt}^{inf} must be because M ∈ B_{nf}^{inf}; and that again must be because M_{0} ∈ B_{nf}^{inf}. Now consider ∥M_{0}∥^{k}. If ∥M_{0}∥^{k} = □, then also ∥M∥^{k+1} = □, and all requirements are trivially satisfied. Otherwise, ∥M∥^{k+1} = \underline{LAM}(x, ∥M_{0}∥^{k}). By the IH, we get that ∥M_{0}∥^{k} ∈ B_{nf}^{fin} and ∥M_{0}∥^{k} ⊑ |M_{0}|^{k}, from which we immediately conclude that also \underline{LAM}(x, ∥M_{0}∥^{k}) ∈ B_{nf}^{fin} and \underline{LAM}(x, ∥M_{0}∥^{k}) ⊑ \underline{LAM}(x, |M_{0}|^{k}) = |M|^{k+1}.

Case M = \underline{APP}(M_{1}, M_{2}): Like above, we must have \underline{APP}(M_{1}, M_{2}) ∈ B_{at}^{inf} ⊆ B_{nf}^{inf} ⊆ B_{bt}^{inf}, hence M_{1} ∈ B_{at}^{inf} and M_{2} ∈ B_{bt}^{inf}. If ∥M_{1}∥^{k} = □, then also ∥M∥^{k+1} = □, and we are done. Otherwise, ∥M∥^{k+1} = \underline{APP}(∥M_{1}∥^{k}, ∥M_{2}∥^{k}). By IH on M_{1}, we get that ∥M_{1}∥^{k} ∈ B_{at}^{fin} and ∥M_{1}∥^{k} ⊑ |M_{1}|^{k}. By IH on M_{2}, ∥M_{2}∥^{k} ∈ B_{bt}^{fin} (which holds even if ∥M_{2}∥^{k} = □), and ∥M_{2}∥^{k} ⊑ |M_{2}|^{k}. Hence, \underline{APP}(∥M_{1}∥^{k}, ∥M_{2}∥^{k}) ∈ B_{at}^{fin}, and ∥M∥^{k+1} ⊑ \underline{APP}(|M_{1}|^{k}, |M_{2}|^{k}) = |M|^{k+1}.

For (c), the proof is by the inclusive variant of rule induction. We strengthen the induction hypothesis to

P (s, M) ⇔ ∀k.∃k′.|M|^{k} ⊑ ∥M∥^{k′} ∧ (s ≠ bt ⇒ ∥M∥^{k′} ≠ □) .

And we want to show that for all (s, M) ∈ B^{inf}, P (s, M). First, we must establish that P is inclusive. By closedness under intersection, and inverse image by projections, it suffices to show that, for every fixed s and k,

P_{s,k}(M) ⇔ ∃k′.|M|^{k} ⊑ ∥M∥^{k′} ∧ (s ≠ bt ⇒ ∥M∥^{k′} ≠ □)

is inclusive. So, consider a chain M_{1} ⊑ M_{2} ⊑ ⋯ such that there exist k′_{1}, k′_{2}, ... with

∀i.|M_{i}|^{k} ⊑ ∥M_{i}∥^{k′_{i}} ∧ (s ≠ bt ⇒ ∥M_{i}∥^{k′_{i}} ≠ □) ;

we must show that there also exists a k′ such that |⨆_{i} M_{i}|^{k} ⊑ ∥ ⨆_{i} M_{i}∥^{k′} and (s ≠ bt ⇒ ∥ ⨆_{i} M_{i}∥^{k′} ≠ □).

But since there can be no infinite ascending chain of λ-trees of height at most k, there must exist an i_{0} such that ∀i ≥ i_{0}, |M_{i}|^{k} = |M_{i_{0}}|^{k}, and so |⨆_{i} M_{i}|^{k} = |M_{i_{0}}|^{k}. Take k′ = k′_{i_{0}}. Then, by monotonicity of ∥ − ∥^{k′}, we conclude,

|⨆_{i} M_{i}|^{k} = |M_{i_{0}}|^{k} ⊑ ∥M_{i_{0}}∥^{k′} ⊑ ∥ ⨆_{i} M_{i}∥^{k′}

as required. Moreover, when s ≠ bt, we have ∥M_{i}∥^{k′} ≠ □, so also ∥ ⨆_{i} M_{i}∥^{k′} ≠ □.

Now, we need to show that P is closed under the rules defining B^{inf}. There are 6 cases to consider:

Case (BT-□). To show: P (bt, □). For any k, |□|^{k} = □, so we can just take k′ = 0. The second conjunct is vacuously true.

Case (BT-nf. To show: P (bt, M), assuming P (nf, M). The result follows immediately from the assumption (forgetting the extra guarantee that ∥M∥^{k′} ≠ □).

Case (NF-at). To show: P (nf, M), assuming P (at, M). The result follows immediately from the assumption.

Case (NF-lam). To show: P (nf, \underline{LAM}(x, M_{0})), assuming P (nf, M_{0}). Let k be given; we must find a k′ such that |\underline{LAM}(x, M_{0})|^{k} ⊑ ∥\underline{LAM}(x, M_{0})∥^{k′}, and ∥\underline{LAM}(x, M_{0})∥^{k′} ≠ □.

By the assumption, there exists a k′_{0} such that |M_{0}|^{k} ⊑ ∥M_{0}∥^{k′_{0}} and ∥M_{0}∥^{k′_{0}} ≠ □. Take k′ = k′_{0} + 1. Then

|\underline{LAM}(x, M_{0})|^{k} ⊑ |\underline{LAM}(x, M_{0})|^{k+1} = \underline{LAM}(x, |M_{0}|^{k}) ⊑ \underline{LAM}(x, ∥M_{0}∥^{k′_{0}}) = ∥M_{0}∥^{k′_{0}} ⊙ ⋆ λM′_{0}. \underline{LAM}(x, M′_{0}) = ∥\underline{LAM}(x, M_{0})∥^{k′_{0}+1} = ∥\underline{LAM}(x, M_{0})∥^{k′} .

Case (AT-var). To show: P (at, \underline{VAR}(x)). For any k, |\underline{VAR}(x)|^{k} ⊑ \underline{VAR}(x) = ∥\underline{VAR}(x)∥^{1}, so we can take k′ = 1.

Case (AT-app). To show: P (at, \underline{APP}(M_{1}, M_{2}), assuming P (at, M_{1}) and P (bt, M_{2}). Let k be given; we must find a k′ such that |\underline{APP}(M_{1}, M_{2})|^{k} ⊑ ∥\underline{APP}(M_{1}, M_{2})∥^{k′} and ∥\underline{APP}(M_{1}, M_{2})∥^{k′} ≠ □.

By the assumptions, there exists a k′_{1} such that |M_{1}|^{k} ⊑ ∥M_{1}∥^{k_{1}} and ∥M_{1}∥^{k′_{1}} ≠ □, and a k′_{2} such that |M_{2}|^{k} ⊑ ∥M_{2}∥^{k′_{2}}. Take k′ = max(k′_{1}, k′_{2}) + 1. Then, noting that for any M and k′ ≤ k′′, ∥M∥^{k′} ⊑ ∥M∥^{k′′}, we get:

|\underline{APP}(M_{1}, M_{2})|^{k} ⊑ |\underline{APP}(M_{1}, M_{2})|^{k+1} = \underline{APP}(|M_{1}|^{k}, |M_{2}|^{k}) ⊑ \underline{APP}(∥M_{1}∥^{k′_{1}}, ∥M_{2}∥^{k′_{2}}) ⊑ \underline{APP}(∥M_{1}∥^{max(k′_{1},k′_{2})}, ∥M_{2}∥^{max(k′_{1},k′_{2})}) = ∥M_{1}∥^{max(k′_{1},k′_{2})} ⊙ ⋆ λM′_{1}. \underline{APP}(M′_{1}, ∥M_{2}∥^{max(k′_{1},k′_{2})}) = ∥\underline{APP}(M_{1}, M_{2})∥^{max(k′_{1},k′_{2})+1} = ∥\underline{APP}(M_{1}, M_{2})∥^{k′} .

□

For showing completeness, it will also be convenient to disregard the exact variable names occurring in the output tree. Accordingly, we define the (evidently continuous) shape function $ : \underline{Λ} → \underline{Λ}, by

$ □ = □ $ \underline{VAR}(x) = \underline{VAR}(x_{$})
$ \underline{LAM}(x, M_{0}) = \underline{LAM}(x_{$}, $ M_{0}) $ \underline{APP}(M_{1}, M_{2}) = \underline{APP}($ M_{1}, $ M_{2})

where x_{$} is some arbitrary but fixed variable. From the definition of the ordering relation on \underline{Λ}, it is easy to see that if M ⊑ M′ but $ M′ ⊑ $ M, then M = M′.

We can now refine the previous characterization of the wrapper functions, to state that they produce representatives that are at least as defined as some given finite tree:

Definition 10 (cf. Definition 4) For any finite M, and l ∈ Λ̂, we define the bounded uniform definedness predicate def_{M}(l) by def_{M}(l) ⇔ ∀n ∈ ω. $ M ⊑ $ (l n). We also write def_{M}^{+}(l) for M ≠ □ ∧ def_{M}(l).

Lemma 23 (cf. Lemma 10) The wrapper functions preserve bounded definedness:

a. For all v ∈ V, def_{\underline{VAR}(x)}^{+}({ \atop VAR}(v)).

b. If for all v ∈ V, def_{M_{0}}^{+}(f v), then def_{\underline{LAM}(x,M_{0})}^{+}({ \atop LAM}(f)).

c. If def_{M_{1}}^{+}(l_{1}) and def_{M_{2}}(l_{2}), then def_{\underline{APP}(M_{1},M_{2})}^{+}({ \atop APP}(l_{1}, l_{2})).

Proof: In each case, let an arbitrary n ∈ ω be given. Then,

a. We have to show that $ \underline{VAR}(x) ⊑ $ \underline{VAR}(v). But by the definition of $ ·, both sides are simply \underline{VAR}(x_{$}), so the inequality holds.

b. We have to show that $ \underline{LAM}(x, M_{0}) ⊑ $ (f g_{n} (n + 1) ⊙ ⋆ λM′_{0}. \underline{LAM}(g_{n}, M′_{0})). Let M′_{0} = f g_{n} (n + 1). By the assumption on f, def_{M_{0}}^{+}(f g_{n}), so M_{0} ≠ □ and $ M_{0} ⊑ $ M′_{0}. Hence also M′_{0} ≠ □, and it only remains to show that $ \underline{LAM}(x, M_{0}) ⊑ $ \underline{LAM}(g_{n}, M′_{0}), which follows immediately from the definition of $ .

c. We have to show that $ \underline{APP}(M_{1}, M_{2}) ⊑ $ (l_{1} n ⊙ ⋆ λM′_{1}. \underline{APP}(M′_{1}, l_{2} n)). Let M′_{1} = l_{1} n and M′_{2} = l_{2} n. By assumptions on l_{1} and l_{2}, we then get that M_{1} ≠ □, $ M_{1} ⊑ $ M′_{1}, and $ M_{2} ⊑ $ M′_{2}. So, again, we get M′_{1} ≠ □, and then $ \underline{APP}(M_{1}, M_{2}) ⊑ $ \underline{APP}(M′_{1}, M′_{2}) by the definition of $ .

□

Lemma 24 (cf. Lemma 11) Let m ∈ Λ and ρ ∈ [V → D_{r}] be such that ∀x ∈ F V (m). ∃l ∈ Λ̂. ρ(x) = ↑ l ∧ def_{\underline{VAR}(x)}^{+}(l). Then, for any M ∈ \underline{Λ} with M ⊑ ⟨m⟩,

a. If M ∈ B_{at}^{fin}, then ∃l.[[m]]_{r} ρ = ↑ l ∧ def_{M}^{+}(l).

b. If M ∈ B_{nf}^{fin}, then def_{M}^{+}(↓ [[m]]_{r} ρ).

c. If M ∈ B_{bt}^{fin}, then def_{M}(↓ [[m]]_{r} ρ).

Proof: By rule induction for B^{fin}, with respect to the evident combined predicate, giving two cases for each part of the lemma:

a. For Rule (AT-var), we have M = \underline{VAR}(x), so we must have m = VAR(x). Then [[m]]_{r} ρ = ρ(x), and since x ∈ F V (m), the result follows directly from the assumption on ρ. For Rule (AT-app), we have M = \underline{APP}(M_{1}, M_{2}), with M_{1} ∈ B_{at}^{fin} and M_{2} ∈ B_{bt}^{fin}, so we must have m = APP(m_{1}, m_{2}), with M_{1} ⊑ ⟨m_{1}⟩ and M_{2} ⊑ ⟨m_{2}⟩. By IH(a) on the first premise, there exists an l_{1} such that [[m_{1}]]_{r} ρ = ↑ l_{1} and def_{M_{1}}^{+}(l_{1}). Therefore, [[m]]_{r} ρ = ψ_{r}(tm(l_{1})) ([[m_{2}]]_{r} ρ) = ↑ ({ \atop APP}(l_{1}, ↓ ([[m_{2}]]_{r} ρ))). Take l_{2} = ↓ ([[m_{2}]]_{r} ρ) and l = { \atop APP}(l_{1}, l_{2}). By IH(c) on the second premise, def_{M_{2}}(l_{2}), so by Lemma 23(c), def_{M}^{+}(l), as required.

b. For Rule (NF-at), we have M ∈ B_{at}^{fin}. By IH(a) on the premise, [[m]]_{r} ρ = ↑ l, for some l with def_{M}^{+}(l). But ↓ (↑ l) = l, so also def_{M}^{+}(↓ ([[m]]_{r} ρ)). For Rule (NF-lam), we have M = \underline{LAM}(x, M_{0}), with M_{0} ∈ B_{nf}^{fin}, so we must have m = LAM(x, m_{0}) with M_{0} ⊑ ⟨m_{0}⟩, and thus [[m]]_{r} ρ = fun(λd.[[m_{0}]]_{r} ρ[x ↦ d]). Expanding the definition of ↓ for the functional case, we have to show that

def_{\underline{LAM}(x,M_{0})}^{+}({ \atop LAM}(λx.↓ ([[m_{0}]]_{r} ρ[x ↦ ↑ ({ \atop VAR}(x))]))) .

By Lemma 23(b), it suffices to show, for every v ∈ V, def_{M_{0}}^{+}(↓ ([[m_{0}]]_{r} ρ′)), where ρ′ = ρ[x ↦ ↑ ({ \atop VAR}(v))]. This follows from IH(b) on the premise, if for every x′ ∈ F V (m_{0}), there exists an l, such that ρ′(x′) = ↑ l and def_{\underline{VAR}(x′)}^{+}(l). But for x′ ≠ x, we must have x′ ∈ F V (m), so this follows from the assumption on ρ; and for x′ = x, it follows from Lemma 23(a).

c. For Rule (BT-□), we have M = □, so the result follows trivially, since any m satisfies def_{□}(↓ ([[m]]_{r} ρ)).

For Rule (BT-nf), we have M ∈ B_{nf}^{fin}, so by IH(b) on the premise, we get def_{M}^{+}(↓ ([[m]]_{r} ρ)), from which also def_{M}(↓ ([[m]]_{r} ρ)).

□

We can now show the main completeness lemma:

Lemma 25 Let m ∈ Λ^{Δ}. If M ↔^{†} m and M ∈ B_{bt}^{inf} then $ M ⊑ $ bt_{Δ}(m).

Proof: Since for any λ-tree M, M = ⨆_{k} |M|^{k} (Lemma 16), by continuity of $ , we get the desired result from ⨆_{k} $ |M|^{k} ⊑ $ bt_{Δ}(m). By the definition of ⨆, it thus suffices to show, for all k, that $ |M|^{k} ⊑ $ bt_{Δ}(m).

Let k be given. By Lemma 22(c), there exists a k′ such that |M|^{k} ⊑ ∥M∥^{k′}. From the definition of M ↔^{†} m, we get that, for this k′, there exists an m′ ∈ Λ, such that |M|^{k′} ⊑ ⟨m′⟩ and m ↔ m′. Since ∥M∥^{k′} ⊑ |M|^{k′} (Lemma 22(b)), we must also have ∥M∥^{k′} ⊑ ⟨m′⟩.

Let ρ_{0} = λx.↑ ({ \atop VAR}(x)); by Lemma 23(a), this clearly satisfies the condition on ρ in Lemma 24. Since ∥M∥^{k′} ∈ B_{bt}^{fin} (Lemma 22(a)), Lemma 24(c) gives us that def_{∥M∥^{k′}} (↓ ([[m′]]_{r} ρ_{0})), so in particular $ ∥M∥^{k′} ⊑ $ (↓ ([[m′]]_{r} ρ_{0}) ♯Δ). Thus, using model soundness, $ ∥M∥^{k′} ⊑ $ (↓ ([[m]]_{r} ρ_{0}) ♯Δ) = $ bt_{Δ}(m). Finally, from |M|^{k} ⊑ ∥M∥^{k′}, we get $ |M|^{k} ⊑ $ ∥M∥^{k′}, and thus $ |M|^{k} ⊑ $ bt_{Δ}(m), as required. □

Theorem 5 (cf. Theorem 2) bt_{Δ} from Definition 7 is a Böhm-tree normalization function on Λ^{Δ}, i.e., for all m, m′ ∈ Λ^{Δ},

a. (soundness) bt_{Δ}(m) ↔_{Δ}^{†} m and bt_{Δ}(m) ∈ B_{bt}^{inf}.

b. (identification) If m ↔ m′, then bt_{Δ}(m) = bt_{Δ}(m′).

c. (completeness) bt_{Δ}(m) is maximal among M ∈ B_{bt}^{inf} such that M ↔^{†} m.

Proof: (Soundness) and (identification) are shown verbatim as in Theorem 2 (using Lemma 21(a) instead of Lemma 5(a)), with the unsurprising exception that unfolding the new definition for ⪅ (using Definition 8 instead of Definition 3), again taking n = ♯Δ, yields bt_{Δ}(m) = □∨bt_{Δ}(m) ∈ B_{nf}^{inf}, from which we get the desired bt_{Δ}(m) ∈ B_{bt}^{inf} by Rule BT-□ or Rule BT-nf, respectively.

(Completeness) Let M ∈ B_{bt}^{inf} with M ↔^{†} m be given; we must show that M cannot be strictly greater than bt_{Δ}(m). So assume that bt_{Δ}(m) ⊑ M. By Lemma 25, $ M ⊑ $ bt_{Δ}(m), so we must actually have bt_{Δ}(m) = M. □

From downwards closure of ↔^{†}, we get a simple, intuitive characterization of soundness: in any finite approximation (not necessarily a level-uniform cut) of bt_{Δ}(m), we can replace all holes □ with proper terms, to obtain a term convertible to the original m. (In particular, if bt_{Δ}(m) ≠ □, by the inversion principle for B_{bt}^{inf}, we see

datatype term = VAR of string | LAM of string*term | APP of term*term
datatype tree = LVAR of string | LLAM of string*(unit->tree)
              | LAPP of (unit->tree)*(unit->tree)
datatype sem = TM of int -> tree | FUN of (unit -> sem) -> sem;
let fun down (s:sem):int->tree = fn n =>
     (case s of
        TM l => l n
      | FUN f => LLAM("g"^Int.toString n, (fn v => fn () => v)
          (down (f (fn () => TM(fn n' => LVAR("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 =>
                              LAPP((fn v => fn () => v) (l n),
                                   fn () => down (eval m2 p) n))
                          | FUN f => f (fn () => eval m2 p)))
   in let fun bt (m:term):tree =
            down (eval m (fn x => TM(fn n => LVAR(x)))) 0
      in bt end end end

Figure 4: The Böhm normalization algorithm, BT.

that the original term must have at least a head normal form.) On the other hand, completeness says that no such replacement for a hole already present in bt_{Δ}(m) can have even a head normal form, since this would contradict that the result tree was maximal.

Like in the finitary case, the characterization of normal forms for soundness and completeness is based on β-normalization only. If we restricted our definition of Böhm trees to only α-normal ones (i.e., using a fixed naming convention for bound variables), instead of saying that the output was a maximal Böhm tree compatible with the input, we would have that it was the largest.

5.4 An implementation of the construction

As before, the development of an actual algorithm and its proof of correctness is straightforward, given the domain-theoretic construction. Unsurprisingly, we shall need to identify □ with divergence, to obtain a computable algorithm (shown in Figure 4), returning so-called effective Böhm trees.

As before, we assume [[term]]^{ml} = Λ, and take T = [[tree]]^{ml} and S = [[sem]]^{ml}. Note that tree is overly lazy when representing Böhm trees and we therefore need to strictify the representations of { \atop LAM} and { \atop APP} explicitly, using the idiom (fn v => fn () => v). As remarked in Section 5.2, the latter strictification is in fact optional, but advantageous from an efficiency perspective.

Lemma 26 There exists an isomorphism i_{\underline{Λ}T} : \underline{Λ} →^{≅} T_{⊥}, satisfying:

a. i_{\underline{Λ}T} (□) = ⊥_{T_{⊥}}.

b. For all x, i_{\underline{Λ}T} (\underline{VAR}(x)) = ⌊ι_{LVAR}(x)⌋.

c. For all x and M_{0}, i_{\underline{Λ}T} (\underline{LAM}(x, M_{0})) = ⌊ι_{LLAM}(x, λu^{1}.i_{\underline{Λ}T} (M_{0}))⌋.

d. For all M_{1} and M_{2}, i_{\underline{Λ}T} (\underline{APP}(M_{1}, M_{2})) = ⌊ι_{LAPP}(λu^{1}.i_{\underline{Λ}T} (M_{1}), λu^{1}.i_{\underline{Λ}T} (M_{2}))⌋.

Proof: See Appendix B.2 □

We can also relate the our two variants of strict extension:

Lemma 27 For M ∈ \underline{Λ} and f : \underline{Λ}→\underline{Λ}, i_{\underline{Λ}T} (M ⊙ ⋆ f) = i_{\underline{Λ}T} (M)⋆λt^{T} . i_{\underline{Λ}T} (f(i_{\underline{Λ}T}^{−1} (⌊t⌋))).

Proof: By cases on M: if M = □, then i_{\underline{Λ}T} (M) = ⊥, and hence

\begin{matrix}i_{\underline{Λ}T} (M ⊙ ⋆ f) = i_{\underline{Λ}T} (□) = ⊥ = ⊥ ⋆ λt. i_{\underline{Λ}T} (f(i_{\underline{Λ}T}^{−1} (⌊t⌋))) \\ = i_{\underline{Λ}T} (M) ⋆ λt. i_{\underline{Λ}T} (f(i_{\underline{Λ}T}^{−1} (⌊t⌋))) . \end{matrix}

On the other hand, if M ≠ □, then i_{\underline{Λ}T} (M) = ⌊t⌋ for some t ∈ T, and thus

i_{\underline{Λ}T} (M ⊙ ⋆ f) = i_{\underline{Λ}T} (f M) = i_{\underline{Λ}T} (f (i_{\underline{Λ}T}^{−1} (i_{\underline{Λ}T} (M)))) = i_{\underline{Λ}T} (f (i_{\underline{Λ}T}^{−1} (⌊t⌋)))

= ⌊t⌋ ⋆ λt. i_{\underline{Λ}T} (f (i_{\underline{Λ}T}^{−1} (⌊t⌋))) = i_{\underline{Λ}T} (M) ⋆ λt. i_{\underline{Λ}T} (f (i_{\underline{Λ}T}^{−1} (⌊t⌋))) . □

Like in the finitary case, we have chosen N = ℤ, so that Λ̂ = [ℤ → \underline{Λ}] is the base domain in the definition of D_{r}, whereas in S, we use the isomorphic [ℤ → T_{⊥}]. Therefore, we get a slightly more complicated characterization of the relationship between the two residualizing models:

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

a. For all l ∈ Λ̂, i_{DS}(tm(l)) = ⌊ι_{TM}(λn^{ℤ}.i_{\underline{Λ}T} (l n))⌋.

b. For all f ∈ [D_{r} → D_{r}], i_{DS}(fun(f)) = ⌊ι_{FUN}(λt^{1→S_{⊥}}. i_{DS}(f(i_{DS}^{−1}(t ∗))))⌋.

c. i_{DS}(⊥_{D_{r}}) = ⊥_{S_{⊥}}

Proof: See Appendix B.1. □

We are now in position to relate the central domain-theoretic functions to the denotations of their syntactic counterparts:

Lemma 29 (cf. Lemma 13) For all d ∈ D_{r} and n ∈ ℤ,

i_{\underline{Λ}T} (↓ d n) = i_{DS}(d) ⋆ λs^{S}. θ_{down} s ⋆ λl^{[ℤ→T_{⊥}]}. l n

Proof: By fixed-point induction on Φ×Θ_{down} (where Φ is as in the proof of Lemma 8, but with the Böhm-tree definitions), using the predicate R ⊆ [D_{r} → Λ̂] × [S → Λ̂_{⊥}] defined by

R = \{(φ, θ) | ∀d ∈ D_{r}, n ∈ ℤ. i_{\underline{Λ}T} (φ d n) = i_{DS}(d) ⋆ λs^{S}.θ s ⋆ λl^{[ℤ→T_{⊥}]}.l n\}

The proof proceeds similarly to the proof of Lemma 13, expect that the isomorphism i_{\underline{Λ}T} must now also be accounted for. Assume that (φ, θ) ∈ R, and let arbitrary d and n be given. The cases d = ⊥_{D_{r}} and d = tm(l) are essentially unchanged, but now using Lemmas 26(a) and 28(a), respectively.

Case d = fun(f): Let ξ = ∅[down ↦ θ, s ↦ ι_{FUN}(λt. i_{DS}(f(i_{DS}^{−1}(t ∗))))] and let ξ′ = ξ[n ↦ n, f ↦ (λt. i_{DS}(f(i_{DS}^{−1}(t ∗))))]. Then,

i_{DS}(d) ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λl^{[ℤ→T_{⊥}]}.l n = i_{DS}(fun(f)) ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λl^{[ℤ→T_{⊥}]}.l n = ⌊ι_{FUN}(λt. i_{DS}(f(i_{DS}^{−1}(t ∗))))⌋ ⋆ λs^{S}.Θ_{down}(θ) s ⋆ λl^{[ℤ→T_{⊥}]}.l n

(by Lemma 28(b))

= [[fn n => (case s of ...| FUN f => LLAM ...)]]^{ml} ξ ⋆ λl^{[ℤ→T_{⊥}]}.l n
= [[LLAM("g"^Int.toString(n), (fn v => fn () => v) (...)]]^{ml} ξ′

= [[down (f ...) ...]]^{ml} ξ′ ⋆ λt^{T} .⌊λu.⌊t⌋⌋ ⋆ λt^{[1→T_{⊥}]}.⌊ι_{LLAM}(g_{n}, t)⌋ = [[down (f (fn () => ...)) (n+1)]]^{ml} ξ′ ⋆ λt^{T} .⌊ι_{LLAM}(g_{n}, λu.⌊t⌋)⌋

= \underbrace{[[f (...)]]^{ml} ξ′}_{s′} ⋆ λs^{S}.θ s ⋆ λl^{[ℤ→T_{⊥}]}.l(n + 1) ⋆ λt^{T} .⌊ι_{LLAM}(g_{n}, λu.⌊t⌋)⌋

Now, s′

= [[f (fn () => TM(fn n' => LVAR("g"^Int.toString(n))))]]^{ml} ξ′

= ⌊(λt. i_{DS}(f(i_{DS}^{−1}(t ∗))))⌋ ⋆ λg.⌊λu.[[TM(fn ...)]]^{ml} ξ′⌋ ⋆ λa.g a = i_{DS}(f(i_{DS}^{−1}(⌊ι_{TM}(λn^{′ℤ}.⌊ι_{LVAR}(g_{n})⌋)⌋))) = i_{DS}(f(i_{DS}^{−1}(⌊ι_{TM}(λn^{′ℤ}.i_{\underline{Λ}T} (\underline{VAR}(g_{n})))⌋))) (by Lemma 26(b)) = i_{DS}(f(tm(λn^{′ℤ}.\underline{VAR}(g_{n})))) (by Lemma 28(a)) = i_{DS}(f(↑ ({ \atop VAR}(g_{n})))) (by Def. of { \atop VAR} and ↑)

The fixed point assumption on φ and θ says that for all d′ ∈ D_{r} and n′ ∈ ℤ,

i_{\underline{Λ}T} (φ d′ n′) = i_{DS}(d′) ⋆ λs^{S}.θ s ⋆ λl^{[ℤ→T_{⊥}]}.l n′. Taking d′ = f(↑ ({ \atop VAR}(g_{n}))) and

n′ = n + 1, we continue:

[[f (...)]]^{ml} ξ′ ⋆ λs^{S}.θ s ⋆ λl^{[ℤ→T_{⊥}]}.l(n + 1) ⋆ λt^{T} .⌊ι_{LLAM}(g_{n}, λu.⌊t⌋)⌋ = i_{\underline{Λ}T} (φ (f(↑ ({ \atop VAR}(g_{n})))) (n + 1)) ⋆ λt^{T} .⌊ι_{LLAM}(g_{n}, λu.⌊t⌋)⌋ (by IH)

Similarly, i_{\underline{Λ}T} (Φ(φ) d n) = i_{\underline{Λ}T} (Φ(φ)(fun(f)) n) = i_{\underline{Λ}T} ({ \atop LAM}(λx^{V}. φ(f(↑ ({ \atop VAR}(x))))) n) = i_{\underline{Λ}T} (φ(f(↑ ({ \atop VAR}(g_{n})))) (n + 1) ⊙ ⋆ λM\underline{Λ}. \underline{LAM}(g_{n}, M)) (by Def. of { \atop LAM}) = i_{\underline{Λ}T} (φ(f(↑ ({ \atop VAR}(g_{n})))) (n + 1)) ⋆ λt^{′T} . i_{\underline{Λ}T} (\underline{LAM}(g_{n}, i_{\underline{Λ}T}^{−1} (⌊t⌋)))

(by Lemma 27)

= i_{\underline{Λ}T} (φ(f(↑ ({ \atop VAR}(g_{n})))) (n + 1)) ⋆ λt^{′T} . ⌊ι_{LLAM}(g_{n}, λu.⌊t⌋)⌋ (by Lemma 26(c))

□

Lemma 30 (cf. 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. The proof of Lemma 14 can be reused verbatim (using Lemma 28 instead of Lemma 12), except for the single subcase of application where the eval definitions actually differ.

We now establish this subcase, which is to be understood in the corresponding context from the proof of Lemma 14.

Case m = APP(m_{1}, m_{2}):

Case [[m_{1}]]_{r} ρ = tm(l_{1}): By Lemma 28(a), θ_{eval} m ⋆ λg.g ϱ

= [[case (eval m1 p) of TM l => TM(fn n ...) | ...]]^{ml} ξ′′

= [[TM(fn n => LAPP(...))]]^{ml} ξ′′[l ↦ λn. i_{\underline{Λ}T} (l_{1} n)]

= ⌊ι_{TM}(\underbrace{λn^{ℤ}.[[LAPP(...)]]^{ml} ξ′′[l ↦ λn. i_{\underline{Λ}T} (l_{1} n), n ↦ n]}_{l})⌋

Similarly, i_{DS}([[m]]_{r} ρ) = i_{DS}([[APP(m_{1}, m_{2})]]_{r} ρ) = i_{DS}(ψ_{r} (tm(l_{1})) ([[m_{2}]]_{r} ρ))

= i_{DS}(↑ { \atop APP}(l_{1}, ↓ ([[m_{2}]]_{r} ρ)))

= i_{DS}(tm({ \atop APP}(l_{1}, ↓ ([[m_{2}]]_{r} ρ)))) (by Def. of ↑) = ⌊ι_{TM}(λn. i_{\underline{Λ}T} ({ \atop APP}(l_{1}, ↓ ([[m_{2}]]_{r} ρ)) n))⌋ (by Lemma 28(a))

= ⌊ι_{TM}(\underbrace{λn.i_{\underline{Λ}T} (l_{1} n ⊙ ⋆ λM′_{1}.\underline{APP}(M′_{1}, ↓ ([[m_{2}]]_{r} ρ) n))}_{l′})⌋ (by Def. of { \atop APP})

Again, it remains to show that l = l′. Let any n ∈ ℤ be given. Let ξ′′′ = ξ′′[l ↦ λn. i_{\underline{Λ}T} (l_{1} n), n ↦ n]. We calculate:

l n

= [[LAPP((fn v => fn () => v) (l n), fn () => ...)]]^{ml} ξ′′′

= i_{\underline{Λ}T} (l_{1} n) ⋆ λt_{1}.[[fn () => ...]]^{ml} ξ′′′ ⋆ λt_{2}.⌊ι_{LAPP}(λu.⌊t_{1}⌋, t_{2})⌋ = i_{\underline{Λ}T} (l_{1} n) ⋆ λt_{1}.⌊ι_{LAPP}(λu.⌊t_{1}⌋, λu.[[down (eval m2 p) n]]^{ml} ξ′′′)⌋ = i_{\underline{Λ}T} (l_{1} n) ⋆ λt_{1}.⌊ι_{LAPP}(λu.⌊t_{1}⌋, λu.i_{DS}([[m_{2}]]_{r} ρ) ⋆ λs.θ_{down} s ⋆ λl_{2}.l_{2} n)⌋

(by IH on m_{2})

= i_{\underline{Λ}T} (l_{1} n) ⋆ λt_{1}. ⌊ι_{LAPP}(λu.⌊t_{1}⌋, λu.i_{\underline{Λ}T} (↓ ([[m_{2}]]_{r} ρ) n))⌋ (by Lemma 29) = i_{\underline{Λ}T} (l_{1} n) ⋆ λt_{1}. i_{\underline{Λ}T} (\underline{APP}(i_{\underline{Λ}T}^{−1} (⌊t_{1}⌋), ↓ ([[m_{2}]]_{r} ρ) n)) (by Lemma 26(d)) = i_{\underline{Λ}T} (l_{1} n ⊙ ⋆ λM_{1}. \underline{APP}(M_{1}, ↓ ([[m_{2}]]_{r} ρ) n)) (by Lemma 27) = l′ n

Since n was arbitrary, l = l′.

□

Theorem 6 (cf. Lemma 15) For all m ∈ Λ, i_{\underline{Λ}T} (bt(m)) = θ_{bt} m.

Proof: Let m be given, and let ξ = ∅[down ↦ θ_{down}, eval ↦ θ_{eval}, bt ↦ θ_{bt}, m ↦ m]. Let further ⌊ϱ⌋ = [[fn x => TM(fn n => LVAR(x))]]^{ml} ξ and ρ = (λx^{V}.↑ ({ \atop VAR}(x))).

We first verify that ϱ and ρ satisfy the requirements of Lemma 30, namely that for all x′ ∈ V ⊃ F V (m), ϱ(x′)

   = [[fn x => TM(fn n => LVAR(x))]]^{ml} ξ ⋆ λf.f(x′)
   = [[TM(fn n => LVAR(x))]]^{ml} ξ[x ↦ x′]

= ⌊ι_{TM}(λn^{ℤ}.⌊ι_{LVAR}(x′)⌋)⌋

= ⌊ι_{TM}(λn^{ℤ}.i_{\underline{Λ}T} (\underline{VAR}(x′)))⌋ (by Lemma 26(b)) = ⌊ι_{TM}(λn^{ℤ}.i_{\underline{Λ}T} ({ \atop VAR}(x′) n))⌋ (by Def. 6 of { \atop VAR}) = i_{DS}(tm(λn^{ℤ}.{ \atop VAR}(x′) n)) (by Lemma 28(a)) = i_{DS}(↑ ({ \atop VAR}(x′))) (by Def. of ↑) = i_{DS}(ρ(x′))

Hence, by a single unrolling of the fixed-point equation θ_{bt} = Θ_{bt}(θ_{bt}),

   θ_{bt} m
   = [[down (eval m (fn x => TM(fn n => LVAR(x)))) 0]]^{ml} ξ
   = [[eval m (fn x => TM(fn n => LVAR(x)))]]^{ml} ξ ⋆ λs.θ_{down} s ⋆ λl.l 0

= θ_{eval} m ⋆ λg.g ϱ ⋆ λs.θ_{down} s ⋆ λl.l 0

= i_{DS}([[m]]_{r} ρ) ⋆ λs.θ_{down} s ⋆ λl.l 0 (by Lemma 30) = i_{\underline{Λ}T} (↓ ([[m]]_{r} ρ) 0) (by Lemma 29) = i_{\underline{Λ}T} (bt(m)) (by Def. 7 of bt)

□

We thus have that the concrete Böhm-tree algorithm is denotationally correct (up to isomorphism). However, BT, although well-typed and closed, is not a complete program, since tree is not a ground type. Hence, unlike for NORM, we cannot readily observe the program output: we first need a formal model of observation of Böhm trees.

5.5 Observing Böhm trees

5.5.1 Computations with infinite results

When the output of the normalizer is a partial, infinitary data structure, it is far less clear what to consider a legitimate notion of observation of the output. In particular, unlike linear streams, which can be naturally produced and printed incrementally, general trees need either a concept of “fair” autonomous production (every non-□ node will eventually be printed), or a model based on interaction, where an independent observer explicitly asks for successive nodes of the tree, while avoiding branches that are (or might be) □. Properly formalizing each of these in the context of our simple functional language, would be far beyond the scope of the present paper, however.

Instead, we will consider a very simple model of observation, where the observer can only ask about one specific node in the tree, for each run; the notion of interaction is thus lifted out as an extralinguistic concept into multiple (possibly even concurrent) top-level evaluations. (Of course, since the language fragment we consider is pure, many subcomputations can be shared across such evaluations; but our denotational model deliberately does not account for such quantitative aspects.) This approach will still allow us to state precisely that we can correctly inspect any reachable part of the output tree, and observationally distinguish any non-identical trees.

To keep the construction concise in our limited ML fragment, we use a uniform, numeric indexing scheme for nodes. In general, for any finitely branching (but potentially infinitely deep) rooted tree, we can associate a unique natural number to each node as follows: the root node has index 0, and for a node with index n in the i’th subtree of a k-ary root node, its index in the whole tree is n · k + i. That is, if we consider a tree to be a node label a, and k (possibly 0) subtrees, we access the label of the n’th node of a tree t, t @ n, as follows:

a(t_{1}, …, t_{k}) @ 0 = a (0≤k) a(t_{1}, …, t_{k}) @ n·k+i = t_{i} @ n (1≤i≤k)

Note that the only invalid indices are those that would correspond to subtrees of a zero-ary (i.e., leaf) node.

5.5.2 Observing λ-trees

For the specific case of λ-trees, we must also take into account partiality, and the fact that various nodes have different information as the label. Accordingly, we define the set of observation results by

O = {VR(v) | v ∈ V} ∪ {LM(v) | v ∈ V} ∪ {AP} ∪ {ER}

and define the operation · @ · : \underline{Λ} × ω → O_{⊥} by course-of-values induction on the second argument:

□ @ n = ⊥  \underline{VAR}(v) @ 0 = ⌊VR(v)⌋  \underline{VAR}(v) @ n+1 = ⌊ER⌋
\underline{LAM}(v, M_{0}) @ 0 = ⌊LM(v)⌋ \underline{LAM}(v, M_{0}) @ n+1 = M_{0} @ n
\underline{APP}(M_{1}, M_{2}) @ 0 = ⌊AP⌋

\underline{APP}(M_{1}, M_{2}) @ 2·n+1 = M_{1} @ n \underline{APP}(M_{1}, M_{2}) @ 2·n+2 = M_{2} @ n

We note that node-observations completely characterize a λ-tree:

Lemma 31 If for all n ∈ ω, M @ n = M′ @ n, then M = M′.

Proof: By Lemma 16, it suffices to show that ∀k. |M|^{k} = |M′|^{k}, by induction on k. The case k = 0 is trivial: both sides are □. For the inductive step, we have to show |M|^{k+1} = |M′|^{k+1} assuming the kth cuts are equal. We proceed by cases on M:

Case M = □: Then M @ 0 = ⊥, so by assumption, also M′ @ 0 = ⊥, and we must have M′ = □. Hence, in particular, |M|^{k+1} = |M′|^{k+1} = □.

Case M = \underline{VAR}(v): Then M @ 0 = ⌊VR(v)⌋, so also M′ @ 0 = ⌊VR(v)⌋, which can only happen if M′ = \underline{VAR}(v), so again we get |M|^{k+1} = |M′|^{k+1} = \underline{VAR}(v).

Case M = \underline{LAM}(v, M_{0}): Then M @ 0 = ⌊LM(v)⌋, so also M′ @ 0 = ⌊LM(v)⌋, which means that M′ = \underline{LAM}(v, M′_{0}) for some M′_{0}. Moreover, we have, for any n, M_{0} @ n = M @ n+1 = M′ @ n+1 = M′_{0} @ n. So by the IH, |M_{0}|^{k} = |M′_{0}|^{k}, and thus |M|^{k+1} = \underline{LAM}(v, |M_{0}|^{k}) = \underline{LAM}(v, |M′_{0}|^{k}) = |M′|^{k+1}.

Case M = \underline{APP}(M_{1}, M_{2}): Then M @0 = ⌊AP⌋, so also M′ @0 = ⌊AP⌋, which means that M′ = \underline{APP}(M′_{1}, M′_{2}) for some M′_{1} and M′_{2}. Now, for any n, M_{1} @ n = M @ 2·n+1 = M′ @ 2·n+1 = M′_{1} @ n, so by IH, |M_{1}|^{k} = |M′_{1}|^{k}. Analogously, we get |M_{2}|^{k} = |M′_{2}|^{k}, and thus |M|^{k+1} = \underline{APP}(|M_{1}|^{k}, |M_{2}|^{k}) = \underline{APP}(|M′_{1}|^{k}, |M′_{2}|^{k}) = |M′|^{k+1}.

□

datatype res = VR of string | LM of string | AP of unit | ER of unit;
let fun obs (t:tree):int->res = fn n =>
     (case t of
        LVAR x => if n = 0 then VR x else ER ()
      | LLAM(x,t0) => if n = 0 then LM x else obs (t0 ()) (n-1)
      | LAPP(t1,t2) => if n = 0 then AP ()
                       else if n mod 2 = 1 then obs (t1 ()) ((n-1) div 2)
                                           else obs (t2 ()) ((n-2) div 2))
in obs end

Figure 5: A simple observation function, OBS.

5.5.3 Implementing tree-observations in ML

The ML implementation of the observation function is shown in Figure 5. To represent observation results, we introduce another ground datatype res; like for term, we assume that [[res]]^{ml} = O, and that the meanings of the constructors agree. We also assume that the ML fragment has been extended with aritmetic operators -, div, and mod, completely analogous to the existing +.

Lemma 32 For all M ∈ \underline{Λ} and n ∈ ω, M @ n = i_{\underline{Λ}T} (M) ⋆ λt. θ_{obs} t ⋆ λf. f n.

Proof: We first calculate, using that θ_{obs} = fix(Θ_{obs}), for any t ∈ T:

θ_{obs} t ⋆ λf. f n

= Θ_{obs}(θ_{obs}) t ⋆ λf. f n

= case t of \begin{cases}ι_{LVAR}(v) & → case n = 0 of \begin{cases}tt & → ⌊VR(v)⌋ \\ ff & → ⌊ER⌋ \end{cases} \\ ι_{LLAM}(v, t′_{0}) & → case n = 0 of \begin{cases}tt & → ⌊LM(v)⌋ \\ ff & → (t′_{0} ∗) ⋆ λt_{0}. θ_{obs} t_{0} ⋆ λf. f (n − 1) \end{cases} \\ ι_{LAPP}(t′_{1}, t′_{2}) & →(\begin{matrix}case n = 0 \\ of & \begin{cases}tt & → ⌊AP⌋ \\ ff & →(\begin{matrix}case n mod 2 = 1 \\ of & \begin{cases}tt & → (t′_{1} ∗) ⋆ λt_{1}. θ_{obs} t_{1} ⋆ λf. f \frac{n−1}{2} \\ ff & → (t′_{2} ∗) ⋆ λt_{2}. θ_{obs} t_{2} ⋆ λf. f \frac{n−2}{2} \end{cases} \end{matrix} ) \end{cases} \end{matrix}) \end{cases}

= case t of \begin{cases}ι_{LVAR}(v) & → case n of \begin{cases}0 & → ⌊VR(v)⌋ \\ n′ + 1 & → ⌊ER⌋ \end{cases} \\ ι_{LLAM}(v, t′_{0}) & → case n of \begin{cases}0 & → ⌊LM(v)⌋ \\ n′ + 1 & → (t′_{0} ∗) ⋆ λt_{0}. θ_{obs} t_{0} ⋆ λf. f n′ \end{cases} \\ ι_{LAPP}(t′_{1}, t′_{2}) & → case n of \begin{cases}0 & → ⌊AP⌋ \\ 2 · n′ + 1 & → (t′_{1} ∗) ⋆ λt_{1}. θ_{obs} t_{1} ⋆ λf. f n′ \\ 2 · n′ + 2 & → (t′_{2} ∗) ⋆ λt_{2}. θ_{obs} t_{2} ⋆ λf. f n′ \end{cases} \end{cases}

The proof then proceeds by a straightforward course-of-values induction on n. We assume the lemma holds for all n′ < n, and consider the four possibilities for M:

When M = □, both sides are ⊥, by Lemma 26(a). Of the remaining cases, we show just M = \underline{LAM}(x, M_{0}) in detail: i_{\underline{Λ}T} (\underline{LAM}(x, M_{0})) ⋆ λt. θ_{obs} t ⋆ λf. f n = ⌊ι_{LLAM}(x, λu.i_{\underline{Λ}T} M_{0})⌋ ⋆ λt. θ_{obs} t ⋆ λf. f n (by Lemma 26(c)) = θ_{obs} (ι_{LLAM}(x, λu.i_{\underline{Λ}T} M_{0})) ⋆ λf. f n

= case n of \begin{cases}0 & → ⌊LM(v)⌋ \\ n′ + 1 & → ((λu.i_{\underline{Λ}T} M_{0}) ∗) ⋆ λt_{0}. θ_{obs} t_{0} ⋆ λf. f n′ \end{cases} (by calc. above)

= case n of \begin{cases}0 & → ⌊LM(v)⌋ \\ n′ + 1 & → i_{\underline{Λ}T} M_{0} ⋆ λt_{0}. θ_{obs} t_{0} ⋆ λf. f n′ \end{cases}

= case n of \begin{cases}0 & → ⌊LM(v)⌋ \\ n′ + 1 & → M_{0} @ n′ \end{cases} (by IH)

= \underline{LAM}(x, M_{0}) @ n (by Def. of @) The cases for M = \underline{VAR}(v) and M = \underline{APP}(M_{1}, M_{2}) are completely analogous. □

Consider now an ML program whose datatype declarations are a union of those in Figures 4 and 5 (in any order), and take

                     OBSBT = fn m => OBS (BT m).

This is an ML expression of type term -> int -> res, i.e., a complete program.

Theorem 7 (cf. Theorem 4) For all m ∈ Λ, n ∈ ω, and o ∈ O, OBSBT •(m, n) = o iff bt(m) @ n = ⌊o⌋.

Proof: We first note that, since BT and OBS are closed, for any ξ, [[BT]]^{ml} ξ = ⌊θ_{bt}⌋ and [[OBS]]^{ml} ξ = ⌊θ_{obs}⌋. Then,

[[OBSBT]]^{ml}∅ ⋆ λf_{1}. f_{1} m ⋆ λf_{2}. f_{2} n

= [[fn m => OBS (BT m)]]^{ml}∅ ⋆ λf_{1}. f_{1} m ⋆ λf_{2}. f_{2} n

= [[OBS (BT m)]]^{ml} ∅[m ↦ m] ⋆ λf_{2}. f_{2} n

= (θ_{bt} m ⋆ λt. θ_{obs} t) ⋆ λf_{2}. f_{2} n

= θ_{bt} m ⋆ λt. θ_{obs} t ⋆ λf_{2}. f_{2} n

= i_{\underline{Λ}T} (bt(m)) ⋆ λt. θ_{obs} t ⋆ λf_{2}. f_{2} n (by Theorem 6) = bt(m) @ n (by Lemma 32)

The result then follows immediately from Theorem 3. □

Moreover, Lemma 31 tells us that BT is also operationally correct with respect to any other observation function (including ones using more user-friendly access paths), because OBS-observations can already distinguish all elements of type tree, even those that do not represent proper Böhm trees.

6 Conclusions and perspectives

We have presented a domain-theoretic analysis of a normalization-by-evaluation construction for the untyped λ-calculus. 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 or modify the present work. Especially in the infinitary variant of the algorithm, there is some leeway in exactly what kind of λ-trees we wish to consider as output, and our observation model for them. 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, as well as the FOS-SACS’04 and RAIRO-ITA reviewers, for their insightful comments.

A Existence of invariant relations

For completeness, we review Pitts’s technique. For conciseness, let us fix our attention to the recursive domain equation

X ≅ (A + [X → X])_{⊥}

where A is a cpo.

A solution to this equation is a pointed cpo D and an isomorphism i : D →^{≅} (A + [D → D])_{⊥}. Define the continuous function δ : [D → D] → [D → D] as

δ(e)(d) = case d of \begin{cases}i^{−1}(⌊in_{1}(a)⌋) & → i^{−1}(⌊in_{1}(a)⌋) \\ i^{−1}(⌊in_{2}(f)⌋) & → i^{−1}(⌊in_{2}(e ∘ f ∘ e)⌋) \\ ⊥_{D} & → ⊥_{D} \end{cases}

A solution is called a minimal invariant if fix(δ) = id_{D}.

The following is well-known and can be found in in e.g. Pitts [Pit96]:

Theorem 8 For any cpo A, there exists a minimal invariant to the recursive domain equation X ≅ (A + [X → X])_{⊥}.

This section establishes the following result, which is an abstract version of the construction used by Pitts to show computational adequacy for untyped PCF [Pit93]:

Theorem 1 Let A be a cpo, and let i : D →^{≅} (A + [D → D])_{⊥} be a minimal invariant. 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, such that, for all d ∈ D and t ∈ T,

d ◁ t iff ( \begin{matrix}d = ⊥_{D} ∨ \\ ∃a. d = i^{−1}(⌊in_{1}(a)⌋) ∧ P_{1}(a, t) ∨ \\ ∃f. d = i^{−1}(⌊in_{2}(f)⌋) ∧ P_{2}(t) ∧ \\ ∀d′ ∈ D; t′, t′′ ∈ T. P_{3}(t, t′, t′′) ∧ d′ ◁ t′ ⇒ f(d′) ◁ t′′ \end{matrix} ) .

To show the theorem, let A, (D, i), and T be given. Define a set Rel of relations on D × T by

R ∈ Rel iff for all t ∈ T, {d | (d, t) ∈ R} is a pointed, inclusive subset of D.

Then (Rel, ⊆) is a partial order, where ⊆ is ordinary set inclusion. Since Rel is closed under arbitrary intersection, (Rel, ⊆) is in fact a complete lattice. (Note, however, that joins in this lattice are not in general set-theoretic unions, since the union of an arbitrary family of inclusive relations need not itself be inclusive. Rather, ⨆{R_{i} | i ∈ I} = ⋂{R ∈ Rel | ∀i ∈ I. R_{i} ⊆ R}, i.e., the smallest inclusive relation containing all of the R_{i}.) In particular, Rel^{op}, i.e., Rel ordered by ⊇, is also a complete lattice, and so is Rel^{op} × Rel.

Now, let predicates P_{1} ⊆ A×T, P_{2} ⊆ T,and P_{3} ⊆ T ×T ×T be given, with P_{1}(·, t) inclusive for all t ∈ T. Define R : Rel^{op} × Rel → Rel by

\begin{matrix}R(R^{−}, R^{+}) = \\ \{(d, t) | \begin{matrix}d = ⊥_{D} ∨ \\ ∃a. d = i^{−1}(⌊in_{1}(a)⌋) ∧ P_{1}(a, t) ∨ \\ ∃f. d = i^{−1}(⌊in_{2}(f)⌋) ∧ P_{2}(t) ∧ \\ ∀d′ ∈ D; t′, t′′ ∈ T. P_{3}(t, t′, t′′) ∧ (d′, t′) ∈ R^{−} ⇒ (f(d′), t′′) ∈ R^{+} \end{matrix} \} . \end{matrix}

R is clearly monotone. It is also easy to check that it preserves inclusivity: in addition to the usual closure under abitrary intersection, finite union, and inverse image, we use that the two existentials are guarded by order-monics, so that, e.g., in the second disjunct, a chain d_{1} ⊑ d_{2} ⊑ ⋯ also induces a chain a_{1} ⊑ a_{2} ⊑ ⋯, allowing us to exploit inclusivity of P_{1}(·, t). To prove Theorem 1, we thus only need to show that there exists a relation ◁ ∈ Rel such that ◁ = R(◁, ◁). We first establish a seemingly weaker result:

Lemma 33 There exist relations ◁^{−}, ◁^{+} ∈ Rel, satisfying:

a. ◁^{−} = R(◁^{+}, ◁^{−}) and ◁^{+} = R(◁^{−}, ◁^{+}).

b. For all R^{−}, R^{+} ∈ Rel, if R^{−} ⊆ R(R^{+}, R^{−}) and R(R^{−}, R^{+}) ⊆ R^{+}, then R^{−} ⊆ ◁^{−} and ◁^{+} ⊆ R^{+}.

Proof: Define the symmetric extension of R, R̂ : Rel^{op} × Rel → Rel^{op} × Rel, by

R̂(R^{−}, R^{+}) = (R(R^{+}, R^{−}), R(R^{−}, R^{+})) .

Now R̂ is a monotonic operator on a complete lattice, so by the Knaster-Tarski fixed-point theorem, R̂ has a fixed point (◁^{−}, ◁^{+}) that is also the least prefixed point of R̂. That is, we have (a) (◁^{−}, ◁^{+}) = R̂(◁^{−}, ◁^{+}), and (b) if R̂(R^{−}, R^{+}) ⊑_{Rel^{op}×Rel} (R^{−}, R^{+}) then (◁^{−}, ◁^{+}) ⊑_{Rel^{op}×Rel} (R^{−}, R^{+}). And these are precisely the properties claimed in the statement of the lemma. □

For relations R, S ∈ Rel, we now define a predicate on e ∈ [D → D] by:

e : R ⊂ S iff ∀d ∈ D, t ∈ T.(d, t) ∈ R ⇒ (e(d), t) ∈ S .

Since this predicate is defined as an intersection of inverse images of the inclusive S, it is itself inclusive.

Lemma 34 If e : R ⊂ S then δ(e) : R(S, R) ⊂ R(R, S).

Proof: Assume e : R ⊂ S, and let (d, t) ∈ R(S, R) be given; we must show that (δ(e)(d), t) ∈ R(R, S). Consider d. The cases d = ⊥_{D} and d = i^{−1}(⌊in_{1}(l)⌋) do not depend on R, S, or e, and are thus immediate. Assume now d = i^{−1}(⌊in_{2}(f)⌋) where by assumption, P_{2}(t) and ∀d′, t′, t′′.P_{3}(t, t′, t′′) ∧ (d′, t′) ∈ S ⇒ (f(d′), t′′) ∈ R. Then δ(e)(d) = i^{−1}(⌊in_{2}(e ∘ f ∘ e)⌋). P_{2}(t) still holds. Let d′, t′, t′′ be given, such that P_{3}(t, t′, t′′) ∧ (d′, t′) ∈ R; we must show (e ∘ f ∘ e)(d′), t′′) ∈ S. We calculate: by e : R ⊂ S, (e(d′), t′) ∈ S; by assumption on f, (f(e(d′)), t′′) ∈ R; and by e : R ⊂ S again, (e(f(e(d′))), t′′) ∈ S, as required. □

Finally, we can show that ◁^{−} and ◁^{+} are in fact the same relation:

Lemma 35 The relations ◁^{−} and ◁^{+} are equal.

Proof: We show that each relation is included in the other. First, take R^{−} = ◁^{+} and R^{+} = ◁^{−}. By Lemma 33(a) we then get that R^{+} = R(R^{−}, R^{+}) and R^{−} = R(R^{+}, R^{−}). Hence, by Lemma 33(b) (either half), ◁^{+} ⊆ ◁^{−}.

Conversely, we have by Lemma 33(a) and Lemma 34 that if e : ◁^{−} ⊂ ◁^{+} then δ(e) : ◁^{−} ⊂ ◁^{+}. Since (⊥, t) ∈ ◁^{+} for any t, we also have ⊥_{[D→D]} : ◁^{−} ⊂ ◁^{+}. Thus, by fixed-point induction, fix(δ) : ◁^{−} ⊂ ◁^{+}. And since (D, i) is a minimal invariant, fix(δ) = id_{D}, and so id_{D} : ◁^{−} ⊂ ◁^{+}, i.e. ◁^{−} ⊆ ◁^{+}. □

Taking ◁ = ◁^{+} = ◁^{−}, and using Lemma 33(a) (either half), we have thus established ◁ = R(◁, ◁), and hence proven Theorem 1.

B Existence of isomorphisms

In the following, we show that the recursive domains used in the abstract normalization constructions, correspond naturally to the predomains arising as the denotations of recursive types in the ML implementation. Naturally, the two specific instances covered here are examples of a more general correspondance, essentially building on currying/uncurrying isomorphisms; however, setting up a proper framework for obtaining such correspondences uniformly, would be too tangential to the paper’s main topic of NBE constructions.

B.1 Isomorphisms for the redualizing model

In appendix A, we considered minimal-invariant solutions (D, i) of the recursive domain equation,

X ≅ (A + [X → X])_{⊥} ,

where A was some fixed cpo. Similarly, we may consider the recursive predomain equation,

Y ≅ B + [[1 → Y_{⊥}] → Y_{⊥}] ,

for some cpo B. A solution to this equation consists of a (bottomless) cpo S and an isomorphism j : S →^{≅} B + [[1 → S_{⊥}] → S_{⊥}]. Define the continuous function γ : [S → S_{⊥}] → [S → S_{⊥}] by

γ(e)(s) = case s of \begin{cases}j^{−1}(in_{1}(a)) & → ⌊j^{−1}(in_{1}(a))⌋ \\ j^{−1}(in_{2}(f)) & → ⌊j^{−1}(in_{2}(λt^{1→S_{⊥}}.f(λu.(t ∗) ⋆ e) ⋆ e))⌋ \end{cases}

A solution is called a minimal invariant if fix(γ) = λs.⌊s⌋. The standard inverse-limit construction, re-expressed in the setting of predomains and total continuous functions, finds minimal-invariant solutions in this sense.

We will also need the following simple property about fixed points:

Lemma 36 Let D and E be pointed cpos, and let f : D → D and g : E → E be continuous functions. If c : D → E is a strict continuous function such that c ∘ f = g ∘ c, then c(fix(f)) = fix(g).

Proof: By fixed point induction. Define the admissible predicate P (d, e) ⇔ c(d) = e as an inverse image of the equality predicate. Since c is strict, we have P (⊥_{D}, ⊥_{E}) and so P is also pointed. Let now d and e be given such that P (d, e), i.e., c(d) = e. By assumption on f and g, also c(f(d)) = g(c(d)) = g(e), i.e., P (f(d), g(e)). Thus by the continuity of f and g, P (fix(f), fix(g)) or simply c(fix(f)) = fix(g). □

We are now in a position to establish the existence of isomorphisms between domains and predomains from minimal invariants for the above equations.

Lemma 37 Let A and B be isomorphic cpos via i_{AB} : A →^{≅} B; let (D, i) be a minimal invariant for the recursive domain equation X ≅ (A + [X → X])_{⊥}; and let (S, j) be a minimal invariant for the recursive predomain equation Y ≅ B + [[1 → Y_{⊥}] → Y_{⊥}]. Then there exists an isomorphism i_{DS} : D →^{≅} S_{⊥}, satisfying

a. For all a ∈ A, i_{DS}(i^{−1}(⌊in_{1}(a)⌋)) = ⌊j^{−1}(in_{1}(i_{AB}(a)))⌋.

b. For all f ∈ [D → D], i_{DS}(i^{−1}(⌊in_{2}(f)⌋)) = ⌊j^{−1}(in_{2}(λt^{1→S_{⊥}}. i_{DS}(f(i_{DS}^{−1}(t ∗)))))⌋.

c. i_{DS}(⊥_{D}) = ⊥_{S_{⊥}}.

Proof: By direct construction. For any strict functions h : D → S_{⊥} and k : S_{⊥} → D, define the strict H(h, k) : D → S_{⊥} and K(h, k) : S_{⊥} → D by

H(h, k) = λd.case d of \begin{cases}i^{−1}(⌊in_{1}(a)⌋) & → ⌊j^{−1}(in_{1}(i_{AB}(a)))⌋ \\ i^{−1}(⌊in_{2}(f)⌋) & → ⌊j^{−1}(in_{2}(λt^{1→S_{⊥}}. h(f(k(t ∗)))))⌋ \\ ⊥_{D} & → ⊥_{S_{⊥}} \end{cases}

K(h, k) = λs′.s′ ⋆ λs. case s of \begin{cases}j^{−1}(in_{1}(b)) & → i^{−1}(⌊in_{1}(i_{AB}^{−1}(b))⌋) \\ j^{−1}(in_{2}(g)) & → i^{−1}(⌊in_{2}(λd. k(g(λu^{1}.h d)))⌋) \end{cases}

Then define (i_{DS}, i_{DS}^{−1}) = fix(λ(h, k)^{[D→S_{⊥}]×[S_{⊥}→D]}.(H(h, k), K(h, k))).

We need to show that i_{DS} and i_{DS}^{−1} are in fact two-sided inverses. Let c be the strict function λ(h, k).k ∘ h : [D → S_{⊥}] × [S_{⊥} → D] → [D → D]. Now,

(c ∘ λ(h, k).(H(h, k), K(h, k))) (h, k)

= K(h, k) ∘ H(h, k)

= λd.case d of \begin{cases}i^{−1}(in_{1}(a)) & → K(h, k)(⌊j^{−1}(in_{1}(i_{AB}(a)))⌋) \\ i^{−1}(in_{2}(f)) & → K(h, k)(⌊j^{−1}(in_{2}(λt. h(f(k(t ∗)))))⌋) \\ ⊥_{D} & → K(h, k)(⊥_{S_{⊥}}) \end{cases}

= λd.case d of \begin{cases}i^{−1}(in_{1}(a)) & → i^{−1}(⌊in_{1}(i_{AB}^{−1}(i_{AB}(a)))⌋) \\ i^{−1}(in_{2}(f)) & → i^{−1}(⌊in_{2}(λd.k((λt. h(f(k(t ∗)))) (λu.h d)))⌋) \\ ⊥_{D} & → ⊥_{D} \end{cases}

= λd.case d of \begin{cases}i^{−1}(in_{1}(a)) & → i^{−1}(⌊in_{1}(a)⌋) \\ i^{−1}(in_{2}(f)) & → i^{−1}(⌊in_{2}(k ∘ h ∘ f ∘ k ∘ h)⌋) \\ ⊥_{D} & → ⊥_{D} \end{cases}

= (λe.λd.case d of \begin{cases}i^{−1}(in_{1}(a)) & → i^{−1}(⌊in_{1}(a)⌋) \\ i^{−1}(in_{2}(f)) & → i^{−1}(⌊in_{2}(e ∘ f ∘ e)⌋) \\ ⊥_{D} & → ⊥_{D} \end{cases}\}) (k ∘ h)

= (δ ∘ c) (h, k) Hence, by Lemma 36 and the minimal invariant property of (D, i),

i_{DS}^{−1} ∘ i_{DS} = c(fix(λ(h, k).(H(h, k), K(h, k)))) = fix(δ) = id_{D} .

For the other direction, let c′ be the strict function λ(h, k).h ∘ k ∘ (λs.⌊s⌋) : [D → S_{⊥}] × [S_{⊥} → D] → [S → S_{⊥}]. We proceed similarly,

(c′ ∘ λ(h, k).(H(h, k), K(h, k))) (h, k)

= H(h, k) ∘ K(h, k) ∘ (λs.⌊s⌋)

= λs.case s of \begin{cases}j^{−1}(in_{1}(b)) & → H(h, k) (i^{−1}(⌊in_{1}(i_{AB}^{−1}(b))⌋)) \\ j^{−1}(in_{2}(g)) & → H(h, k) (i^{−1}(⌊in_{2}(λd.k(g(λu.h d)))⌋)) \end{cases}

= λs.case s of \begin{cases}j^{−1}(in_{1}(b)) & → ⌊j^{−1}(in_{1}(i_{AB}(i_{AB}^{−1}(b))))⌋ \\ j^{−1}(in_{2}(f)) & → ⌊j^{−1}(in_{2}(λt.h((λd.k(g(λu.h d))) (k(t ∗)))))⌋ \end{cases}

= λs.case s of \begin{cases}j^{−1}(in_{1}(b)) & → ⌊j^{−1}(in_{1}(b))⌋ \\ j^{−1}(in_{2}(f)) & → ⌊j^{−1}(in_{2}(λt.h(k(f(λu.h(k(t ∗)))))))⌋ \end{cases}

= λs.case s of \begin{cases}j^{−1}(in_{1}(b)) & → ⌊j^{−1}(in_{1}(b))⌋ \\ j^{−1}(in_{2}(f)) & → ⌊j^{−1}(in_{2}(λt.(\begin{matrix}f(λu.(t ∗) ⋆ λs. h(k(⌊s⌋))) ⋆ \\ λs. h(k(⌊s⌋)) \end{matrix} )))⌋ \end{cases}

(by strictness of h and k)

= (λe.λs.case s of \begin{cases}j^{−1}(in_{1}(b)) & → ⌊j^{−1}(in_{1}(b))⌋ \\ j^{−1}(in_{2}(f)) & → ⌊j^{−1}(in_{2}(λt.f(λu.(t ∗) ⋆ e) ⋆ e))⌋ \end{cases}\})

(λs.h(k(⌊s⌋)))

= (γ ∘ c′) (h, k)

By Lemma 36 and the minimal-invariant property of (S, j),

i_{DS} ∘ i_{DS}^{−1} ∘ (λs.⌊s⌋) = c′(fix(λ(h, k).(H(h, k), K(h, k)))) = fix(γ) = λs.⌊s⌋ .

Also, i_{DS}(i_{DS}^{−1}(⊥)) = ⊥ by strictness of i_{DS} and i_{DS}^{−1}. Thus, i_{DS} : D →^{≅} S_{⊥} is indeed an isomorphism. From the fixed point equation i_{DS} = H(i_{DS}, i_{DS}^{−1}), we can then immediately read off the additional properties in parts (a-c) of the Lemma. □

Lemma 37 in particular establishes Lemma 12, taking A = B = [ℤ → Λ_{⊥}] and i_{AB} = id_{[ℤ→Λ_{⊥}]}. It also establishes Lemma 28, with A = [ℤ → \underline{Λ}], B = [ℤ → T_{⊥}], and i_{AB} = λl.λn.i_{\underline{Λ}T} (l n), where i_{\underline{Λ}T} : \underline{Λ} →^{≅} T_{⊥} is the isomorphism from Lemma 26.

B.2 Isomorphisms for Böhm trees

The proof of the existence of isomorphisms for Böhm trees proceeds analogously with above. For a cpo A, a solution to the recursive domain equation,

X ≅ (A + A × X + X × X)_{⊥}

is a pointed cpo D and an isomorphism i : D →^{≅} (A + A × D + D × D)_{⊥}. The corresponding δ : [D → D] → [D → D] is given by,

δ(e)(d) = case d of \begin{cases}i^{−1}(⌊in_{1}(a)⌋) & → i^{−1}(⌊in_{1}(a)⌋) \\ i^{−1}(⌊in_{2}(a, d_{0})⌋) & → i^{−1}(⌊in_{2}(a, e(d_{0}))⌋) \\ i^{−1}(⌊in_{3}(d_{1}, d_{2})⌋) & → i^{−1}(⌊in_{3}(e(d_{1}), e(d_{2}))⌋) \\ ⊥_{D} & → ⊥_{D} \end{cases}

Again, a solution is a minimal invariant if fix(δ) = id_{D}.

Similarly, the recursive predomain equation,

Y ≅ A + A × [1 → Y_{⊥}] + [1 → Y_{⊥}] × [1 → Y_{⊥}]

has a minimal-invariant solution consisting of a (bottomless) cpo S and an isomorphism j : S →^{≅} A + A × [1 → S_{⊥}] + [1 → S_{⊥}] × [1 → S_{⊥}], such that the continuous function γ : [S → S_{⊥}] → [S → S_{⊥}] given by

γ(e)(s) = case s of \begin{cases}j^{−1}(in_{1}(a)) & → ⌊j^{−1}(in_{1}(a))⌋ \\ j^{−1}(in_{2}(a, t_{0})) & → ⌊j^{−1}(in_{2}(a, λu. (t_{0} ∗) ⋆ e))⌋ \\ j^{−1}(in_{3}(t_{1}, t_{2})) & → ⌊j^{−1}(in_{3}(λu. (t_{1} ∗) ⋆ e, λu. (t_{2} ∗) ⋆ e))⌋ \end{cases}

satisfies fix(γ) = λs.⌊s⌋.

Lemma 38 Let A a cpo, let (D, i) be a minimal invariant for the recursive domain equation X ≅ (A + A × X + X × X)_{⊥}, and let (S, j) be a minimal invariant for the recursive predomain equation Y ≅ A + A × [1 → Y_{⊥}] + [1 → Y_{⊥}] × [1 → Y_{⊥}]. Then there exists an isomorphism i_{DS} : D →^{≅} S_{⊥}, satisfying

a. i_{DS}(⊥_{D}) = ⊥_{S_{⊥}}.

b. For all a, i_{DS}(i^{−1}(⌊in_{1}(a)⌋)) = ⌊j^{−1}(in_{1}(a))⌋.

c. For all a and d, i_{DS}(i^{−1}(⌊in_{2}(a, d_{0})⌋) = ⌊j^{−1}(in_{2}(a, λu^{1}.i_{DS}(d_{0})))⌋.

d. For all d_{1} and d_{2}, i_{DS}(i^{−1}(⌊in_{3}(d_{1}, d_{2})⌋)) = ⌊j^{−1}(in_{3}(λu^{1}.i_{DS}(d_{1}), λu^{1}.i_{DS}(d_{2})))⌋.

Proof: By direct construction. For any strict functions h : D → S_{⊥} and k : S_{⊥} → D, define the strict H(h) : D → S_{⊥} and K(k) : S_{⊥} → D by

H(h) = λd.case d of \begin{cases}i^{−1}(⌊in_{1}(a)⌋) & → ⌊j^{−1}(in_{1}(a))⌋ \\ i^{−1}(⌊in_{2}(a, d_{0})⌋) & → ⌊j^{−1}(in_{2}(a, λu. h(d_{0})))⌋ \\ i^{−1}(⌊in_{3}(d_{1}, d_{2})⌋) & → ⌊j^{−1}(in_{3}(λu. h(d_{1}), λu. h(d_{2})))⌋ \\ ⊥_{D} & → ⊥_{S_{⊥}} \end{cases}

K(k) = λs′.s′ ⋆ λs. case s of \begin{cases}j^{−1}(in_{1}(a)) & → i^{−1}(⌊in_{1}(a)⌋) \\ j^{−1}(in_{2}(a, t_{0})) & → i^{−1}(⌊in_{2}(a, k(t_{0} ∗))⌋) \\ j^{−1}(in_{3}(t_{1}, t_{2})) & → i^{−1}(⌊in_{3}(k(t_{1} ∗), k(t_{2} ∗))⌋) \end{cases}

Then define (i_{DS}, i_{DS}^{−1}) = fix(λ(h, k)^{[D→S_{⊥}]×[S_{⊥}→D]}.(H(h), K(k))).

Again, we need to show that i_{DS} and i_{DS}^{−1} are in fact two-sided inverses. Let c be the strict function λ(h, k).k ∘ h : [D → S_{⊥}] × [S_{⊥} → D] → [D → D]. Now,

(c ∘ λ(h, k).(H(h), K(k))) (h, k)

= K(k) ∘ H(h)

= λd.case d of \begin{cases}i^{−1}(⌊in_{1}(a)⌋) & → i^{−1}(⌊in_{1}(a)⌋) \\ i^{−1}(⌊in_{2}(a, d_{0})⌋) & → i^{−1}(⌊in_{2}(a, k((λu. h(d_{0})) ∗))⌋) \\ i^{−1}(⌊in_{3}(d_{1}, d_{2})⌋) & → i^{−1}(⌊in_{3}(k((λu. h(d_{1})) ∗), k((λu. h(d_{2})) ∗))⌋) \\ ⊥_{D} & → ⊥_{D} \end{cases}

= λd.case d of \begin{cases}i^{−1}(⌊in_{1}(a)⌋) & → i^{−1}(⌊in_{1}(a)⌋) \\ i^{−1}(⌊in_{2}(a, d_{0})⌋) & → i^{−1}(⌊in_{2}(a, (k ∘ h)(d_{0}))⌋) \\ i^{−1}(⌊in_{3}(d_{1}, d_{2})⌋) & → i^{−1}(⌊in_{3}((k ∘ h)(d_{1}), (k ∘ h)(d_{2}))⌋) \\ ⊥_{D} & → ⊥_{D} \end{cases}

= (δ ∘ c) (h, k) By Lemma 36 and the minimal invariant property of (D, i),

i_{DS}^{−1} ∘ i_{DS} = c(fix(λ(h, k).(H(h), K(k)))) = fix(δ) = id_{D} .

For the other direction, let c′ be the strict function λ(h, k).h ∘ k ∘ (λs.⌊s⌋) : [D → S_{⊥}] × [S_{⊥} → D] → [S → S_{⊥}]. We proceed similarly,

(c′ ∘ λ(h, k).(H(h), K(k))) (h.k)

= λs.case s of \begin{cases}j^{−1}(in_{1}(a)) & → ⌊j^{−1}(in_{1}(a))⌋) \\ j^{−1}(in_{2}(a, t_{0})) & → ⌊j^{−1}(in_{2}(a, λu.h(k(t_{0} ∗))))⌋) \\ j^{−1}(in_{3}(t_{1}, t_{2})) & → ⌊j^{−1}(in_{3}(λu.h(k(t_{1} ∗)), λu.h(k(t_{2} ∗))))⌋) \end{cases}

= (γ ∘ c′) (h, k) (by strictness of h and k)

By Lemma 36 and the minimal invariant property of (S, j),

i_{DS} ∘ i_{DS}^{−1} ∘ (λs.⌊s⌋) = c′(fix(λ(h, k).(H(h), K(k)))) = fix(γ) = λs.⌊s⌋.

Thus, i_{DS} : D →^{≅} S_{⊥} is indeed an isomorphism.

As before, the fixed point equation i_{DS} = H(i_{DS}, i_{DS}^{−1}) immediately yields the remainder of the lemma. □

Lemma 38 establishes Lemma 26.

References

[AJ04] Klaus Aehlig and Felix Joachimski. Operational aspects of untyped normalization by evaluation. Mathematical Structures in Computer Science, 14:587–611, August 2004.

[Bar84] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.

[BS91] 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.

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

[Fil99] 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.

[FR03] Andrzej Filinski and Henning Korsholm Rohde. A denotational account of untyped normalization by evaluation (extended version, with detailed proofs). BRICS Report RS-03-40, University of Aarhus, Denmark, De-

cember 2003. Available from http://www.brics.dk/RS/03/40/.

[FR04] Andrzej Filinski and Henning Korsholm Rohde. A denotational account of untyped normalization by evaluation. In I. Walukiewicz, editor, 7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2004), volume 2987 of Lecture Notes in Computer Science, pages 167–181, Barcelona, Spain, March 2004. Springer-Verlag.

[GL02] Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Simon Peyton Jones, editor, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Notices, Vol. 37, No. 9, pages 235–246, Pittsburgh, Pennsylvania, September 2002. ACM Press.

[Mit96] John C. Mitchell. Foundations for Programming Languages. The MIT Press, 1996.

[MTHM97] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML. The MIT Press, revised edition, 1997.

[Pit93] 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.

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

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

[SPG03] 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 2003.

Recent BRICS Report Series Publications

RS-05-4 Andrzej Filinski and Henning Korsholm Rohde. Denotational Aspects of Untyped Normalization by Evaluation. February 2005. 51 pp. Extended version of an article to appear in the FOSSACS 2004 special issue of RAIRO, Theoretical Informatics and Applications.

RS-05-3 Olivier Danvy and Mayer Goldberg. There and Back Again. January 2005. iii+16 pp. Extended version of an article to appear in Fundamenta Informatica. This version supersedes BRICS RS-02-12.

RS-05-2 Dariusz Biernacki and Olivier Danvy. On the Dynamic Extent of Delimited Continuations. January 2005. ii+30 pp.

RS-05-1 Mayer Goldberg. On the Recursive Enumerability of Fixed-Point Combinators. January 2005. 7 pp. Superseedes BRICS report RS-04-25.

RS-04-41 Olivier Danvy. Sur un Exemple de Patrick Greussay. December 2004. 14 pp.

RS-04-40 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. December 2004. 22 pp. To appear in TOPLAS. Supersedes BRICS report RS-03-20.

RS-04-39 Olivier Danvy and Lasse R. Nielsen. CPS Transformation of Beta-Redexes. December 2004. ii+11 pp. Superseedes an article to appear in Information Processing Letters and BRICS report RS-00-35.

RS-04-38 Olin Shivers and Mitchell Wand. Bottom-Up β-Substitution: Uplinks and λ-DAGs. December 2004.

RS-04-37 Jørgen Iversen and Peter D. Mosses. Constructive Action Semantics for Core ML. December 2004. 68 pp. To appear in a special Language Definitions and Tool Generation issue of the journal IEE Proceedings Software.

RS-04-36 Mark van den Brand, Jørgen Iversen, and Peter D. Mosses. An Action Environment. December 2004. 27 pp. Appears in Hedin and Van Wyk, editors, Fourth ACM SIGPLAN Workshop on Language Descriptions, Tools and Applications, LDTA ’04, 2004, pages 149–168.