BRICS RS-00-47 L. R. Nielsen: A Denotational Investigation of Defunctionalization BRICS

Basic Research in Computer Science

A Denotational Investigation of Defunctionalization

Lasse R. Nielsen BRICS Report Series RS-00-47 ISSN 0909-0878 December 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Lasse R. Nielsen.

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/00/47/

A Denotational Investigation of Defunctionalization

Lasse R. Nielsen BRICS ^{∗}

Department of Computer Science, University of Aarhus ^{†}

June 1999, revised in July 2000, and reformatted in May 2001

Abstract

Defunctionalization was introduced by John Reynolds in his 1972 article Definitional Interpreters for Higher-Order Programming Languages. Defunctionalization transforms a higher-order program into a first-order one, representing functional values as data structures. Since then it has been used quite widely, but we observe that it has never been proven correct.

We formalize defunctionalization denotationally for a typed functional language, and we prove that it preserves the meaning of any terminating program. Our proof uses logical relations.

Keywords: defunctionalization, program transformation, denotational semantics, logical relations.

∗ Basic Research in Computer Science (http://www.brics.dk/), Centre of the Danish National Research Foundation.

† Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

E-mail: lrn@brics.dk

Contents

1 Introduction 4 1.1 This work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Defunctionalization . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 Scope of the results . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 Related subjects . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.5 Prerequisites and notation . . . . . . . . . . . . . . . . . . . . 9

1.5.1 Indexed products . . . . . . . . . . . . . . . . . . . . . 9 1.5.2 Disjoint indexed unions . . . . . . . . . . . . . . . . . 11 1.5.3 Lifting CPOs . . . . . . . . . . . . . . . . . . . . . . . 12

1.6 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

2 The source language 12 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2 Typing judgments . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3 Denotational semantics . . . . . . . . . . . . . . . . . . . . . . 13 2.4 Annotated source language . . . . . . . . . . . . . . . . . . . 14

3 The target language 17 3.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.2 Typing judgments . . . . . . . . . . . . . . . . . . . . . . . . 19 3.3 Denotational semantics . . . . . . . . . . . . . . . . . . . . . . 21 3.4 Comments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

4 The defunctionalizing transformation 25 4.1 Definition of the transformation . . . . . . . . . . . . . . . . . 26 4.2 Comments on the transformation . . . . . . . . . . . . . . . . 28

5 Type preservation 29 5.1 Defining solutions to typing judgments . . . . . . . . . . . . . 29 5.2 Data-type declarations are well-typed . . . . . . . . . . . . . 30 5.3 Expressions are well-typed . . . . . . . . . . . . . . . . . . . . 30 5.4 Function declarations are well-typed . . . . . . . . . . . . . . 31 5.5 Summary and conclusion . . . . . . . . . . . . . . . . . . . . 31

6 Meaning preservation 31 6.1 Properties of the semantics of the program . . . . . . . . . . 32 6.2 Definition of the logical relation . . . . . . . . . . . . . . . . . 34 6.3 Translations of expressions . . . . . . . . . . . . . . . . . . . . 35 6.4 Summary and conclusion . . . . . . . . . . . . . . . . . . . . 38 7 Applicability and conclusion 38

7.1 Extensions of the target language . . . . . . . . . . . . . . . . 38 7.2 Extensions of the source language . . . . . . . . . . . . . . . . 38 7.3 Extensions of annotations: analysis . . . . . . . . . . . . . . . 39 7.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

A Proof of type preservation 40

B Proof of Lemma 3 43

C Proof of Lemma 5 44

List of Figures

1 Example program . . . . . . . . . . . . . . . . . . . . . . . . . 7 2 Syntax of the source language . . . . . . . . . . . . . . . . . . 13 3 Typing judgments for the source language . . . . . . . . . . . 14 4 Call-by-value denotational semantics of well-typed programs . 15 5 Syntax of the target language . . . . . . . . . . . . . . . . . . 18 6 The logical relation . . . . . . . . . . . . . . . . . . . . . . . . 35

1 Introduction

In a language with lexical scope and higher-order functions, evaluating a function abstraction naturally yields a function value, a closure [Lan64], that contains information about both the definition of the function and the denotation of its free variables. Functions taking functions as arguments are common in functional programming with map- and fold-like functions. Functions returning functions occur when applying curried functions like iterators, or, e.g., a function implementing function composition, which takes two functions as arguments and returns a function as result.

Defunctionalization is a program transformation that turns a program with higher-order functions into one with only first-order functions, thus removing the need to have closures as expressible values, using Strachey’s terminology [Str00]. The method was described by Reynolds in his influential ’72 paper, “Definitional Interpreters for Higher-Order Programming Languages” [Rey98]. It is based on (1) using algebraic data-types to represent the functional values as data values, at each declaration point; and (2) decoding the representation with an apply function defined by cases over the data-type, at each application point. Reynolds only applies defunctionalization to one class of programs, definitional interpreters, but his method is generally applicable to any closed program.

Reynolds’s method became an instant classic, one that has been used in many contexts, not only for implementing interpreters for higher-order languages in first-order languages [Bel93, CJW00]. Defunctionalization can be used in program transformers, such as compilers and partial evaluators, either to simplify the language (implicit in Bondorf’s work [Bon90] section 5.6: Representing Higher-Order Values) or to support higher-order functions if the target language of the transformation does not support such [CJW00]. Recently, Bell, Bellegarde, and Hook have applied defunctionalization to typed languages [BH94, BBH97]. In the latter of these papers they formalize a defunctionalizing translation and prove that it preserves typability; however they provide no formal proof that defunctionalization is also a meaning preserving transformation, although there is no real doubt that it is one.

1.1 This work

In this article, we choose a prototypical simply-typed functional language, and define a defunctionalizing transformation from an annotated version of this source language to a target language without higher-order functions. This language and approach resemble the ones in Bell, Bellegarde, and Hook’s work [BBH97].

The target language is chosen as a subset of the one considered by Bell et al., which is itself very standard:

• It is typed.

• It has top-level, mutually recursive function declarations, but not firstclass functions. That is, the function identifiers can only occur in function position in applications, and only such function identifiers can occur there. “Ordinary” variables cannot denote function values and expressions cannot evaluate to such, and the language only supports functions with two arguments. This is sufficient for the output of the defunctionalization transformation, and we restrict the language to avoid unnecessary features.

• It has user-defined algebraic data-types, with a syntax resembling that of Standard ML. The datatype constructors are used for the representation of function values when defunctionalizing, The data-types denote sets constructed by products, disjoint sums, and recursive definitions, and as such they can be implemented in any language with these type constructions.

• Its set of variable names includes the ones of the source language.

• It has the same operations on base type (natural numbers) as the source language, making translation of these immediate.

Programs in the target language can be translated easily to any language with top-level functions, product and sum constructions and recursive types, and operations on integers, e.g., Standard ML or even C, using tuples and inductive datatypes in the former and pointers to structures and tagged unions in the latter [TO98].

We give the semantics of the source and target languages, and formalize a defunctionalization transformation. We then prove that the translation preserves the semantics of terminating programs.

1.2 Defunctionalization

Reynolds’s transformation works on untyped expressions. It turns function abstractions into constructors applied to the denotation of the free variables, and it turns applications into applications of a first-order apply function to a value and an argument.

We define a translation on both types and (typing derivations of) expressions that maps function types into names of data-types, and expressions into equivalent expressions, with only the above changes. In other words, expressions that are not function abstractions or applications are merely traversed to translate the subexpressions. We are translating typing derivations, so we can only translate well-typed programs.

Translating the types makes it clear how to proceed. Any function type is translated to a data-type, so any expression having a functional type must be translated into a new expression having the type of the data-type. Functiontype introduction (function abstractions) is then translated to data-type construction, i.e., a constructor application. Function-type elimination, i.e., application, must then be turned into data-type deconstruction, i.e., a case construct. Each case then corresponds to the body of each function that could have flowed there in the original program.

Implementing this directly, using syntax that is introduced in Section 3, would give

(fun f x : τ_{1} →τ_{2} = … x_{2} … x … x_{7} …)

which is the syntax we use for a recursive function value where x_{1} … x_{n} are free variables. Transforming this function definition yields

C ⟨v_{1} = x_{1}⟩…⟨v_{n} = x_{n}⟩

which is the syntax used for applying a data-type constructor to a tuple indexed by the names v_{1} through v_{n} (reminiscent of, e.g., ML records).

Likewise, function application

f(y)

is transformed into a case dispatch matching the constructor that represents the function definition:

case f of C ⟨v_{1} = x_{1}⟩…⟨v_{m} = x_{n}⟩=> … x_{2} … y … x_{7} …

This immediate implementation falls short for recursive functions. A recursive function can call itself inside the body of the function, so if the transformation places the body of the function at its possible application points, it would have to expand the application infinitely. This is where we need the “apply” function mentioned earlier. An application thus induces a global function definition for each data-type

fun app ff xx = case ff of C_{l} ⟨v_{1} = x_{1}⟩…⟨v_{m} = x_{n}⟩=> …

Program (fun f x : nat →nat = ifz(x, 0, y.succ(succ(f y))))_{l}^{⟨⟩}

(succ(succ(0)))

is translated into

datatype c_{τ_{1}→τ_{2}} = C_{l} ⟨⟩ fun app_{τ_{1}→τ_{2}} ff xx =

case ff of C_{l} ⟨⟩ => ifz(xx , 0, y.succ(succ(app_{τ_{1}→τ_{2}} ff y)))

in

app_{τ_{1}→τ_{2}} (C_{l} ⟨⟩) succ(succ(0))

Figure 1: Example program

and the application itself becomes just

app f y

To preserve well-typedness, we also translate the types. We give a datatype declaration defining one data-type for each function type occurring in the program, such that each translated type is defined in the target program. For each function abstraction we add, to the datatype corresponding to the type of the abstraction, a constructor with an argument that contains the values in the environment of the abstraction.

Notice that this data-type declaration might define data-types with no constructors. Such declarations are allowed, but they are only needed if the program contains unreachable code or a diverging expression, since it is a symptom of there being an expression with a type for which no values are ever created. On the other hand it is easy to write a well-typed program with this property, so the translation must treat it properly.

We then define a group of top-level application functions, one for each functional type occurring in an application. These functions take two arguments, a function representation and an argument, and dispatch on the function representation. The case contains a match for each constructor of that type, with the body of the corresponding function as expression (and a renaming of the arguments of the apply function to the name of the formal parameters of the original function). We place the translation of the expression of the original program in the scope of these declarations. See Figure 1 for an example.

1.3 Scope of the results

We prove the weak correctness of the defunctionalization translation of a prototypical typed functional language with higher-order functions. In other words, if the original program terminates, then so does the defunctionalized one, and with the same result. Eventually, we want to prove full correctness, i.e., semantic equivalence of the two programs.

The source language is monomorphic, whereas Bell, Bellegarde, and Hook treat a polymorphic language, albeit by turning it into a monomorphic one by code duplication. Reynolds’s programs are untyped, and only implicitly group the occurring functions into “continuations” and “abstractions” in the interpreters.

Where Reynolds stores only the values of the free variables of a function in the constructed value, our transformation stores the entire environment. Only storing the value of the free variables is an optimization which does not change the correctness of the translation, and we have omitted it from the present work.

Reynolds does not translate all function abstractions into values, only the ones that are actually used as arguments or results of higher-order functions. He leaves the globally defined functions, such as the one called eval, as functions. The present transformation, on the other hand, turns all abstractions in the source program into constructed values in the target program.

Reynolds can avoid transforming such functions because he knows that the function is not used as an argument or result of a function in the translated program, so there is no need to turn it into a non-functional value. In this paper we do not assume such knowledge, though it could be added with a prior analysis step. There is also another consideration at work; the function eval does occur as a free variable in another function abstraction which is translated into a constructor. If the value of eval is to be used as part of the argument to this constructor, being a free variable in the body of the function abstraction, then that value should have been translated too. Here Reynolds recognizes that it is not necessary to put the eval function into the “closure” he creates because it is defined at top level, and therefore still in scope for the code of the body of the abstraction when the body is moved into the apply function. This optimization is similar to Johnsson’s λ-lifting which generates recursive equations [Joh85].

An analysis that detects whether the value of a function abstraction is used as an argument or result is trivial for the source language we use.

To summarize, if the value of a function definition is not being passed around, and the function is closed, then it can be made into a global (toplevel) function. If it is not closed, but not being passed around and not free in some other function that is being converted, then it can be left in place. Reynolds at least uses the latter rule, and his program already has as many functions global as possible. The present transformation does neither of these optimizations. Rather, it makes the pessimistic, but safe, assumption that any function can possibly be used as argument to another function, so all function abstractions must be translated, just as in super-combinator conversion [Pey85].

1.4 Related subjects

Defunctionalization is closely related to two other transformations: Closure Conversion and Lambda Lifting.

Closure Conversion is a program transformation that turns all function abstractions into pairs of closed code (no free variables) and a representation of the values of the free variables in the original code. The closed code is still a function, so this is not defunctionalization, but it shares the concept of turning abstractions into values containing the values of the free variables at the point of definition. Closure conversion has also been studied in a typed setting by Harper, Morrisett, and Minamide [MMH96], and used in, e.g., a the compiler for Standard ML of New Jersey [AJ89].

Lambda Lifting is a program transformation that bypasses the need to represent closures by removing the lexical nesting. It “lifts” abstractions out of the program and into “global” top-level declarations (traditionally a set of mutually recursive equations), capturing the non-functional free variables by abstracting over them. Their denotation must then be passed at each application. The functions themselves are then all defined at the same level, and need not be captured in the same way. They can still be passed as arguments if needed, though [Joh85, DS00, FH00].

1.5 Prerequisites and notation

The reader is assumed to be familiar with Reynolds’s “Definitional Interpreters for Higher-Order Programming Languages” [Rey98], and the concepts and notation of denotational semantics, as presented in, e.g., Winskel’s textbook [Win93].

1.5.1 Indexed products

A product space, A × B, is characterized by, amongst other things, the existence of the associated projection functions, π_{1} : A × B → A and π_{2} :

A × B → B, i.e., the product is implicitly indexed by the numbers 1 and 2. That is, A × B is isomorphic to the subset of the function space {1, 2} → A ∪ B that maps 1 to something in A and 2 to something in B.

Generalizing this to products over arbitrary finite sets, if for each s ∈ S we can construct a set A_{s}, then ∏_{s∈S} A_{s} is a product space with projections π_{s} : (∏_{s∈S} A_{s}) → A_{s} for each s in S. If the A_{s} are all equal to some set M, the product can be written M^{S}. The set of indices is called the “index set”.

Let A =^{def} ∏_{s∈S} A_{s} be an arbitrary product space, and α a tuple in it. The notation for elements of such products will be {s_{1} = a_{1}, …, s_{n} = a_{n}} where a_{i} ∈ A_{s_{i}}, reminiscent of, e.g., records in ML.

An element of a product space is uniquely determined by its values under the projections. That is, we can define an element of a product space, ∏_{s∈S} A_{s}, by giving an element a_{s} ∈ A_{s} for each s ∈ S.

Dom(A)

The domain of a product space is the index set of the product. In this case Dom(A) = S.

The Dom function may also be used on elements of the product, i.e., Dom(α). In that case it is just a shorthand for “Dom(A) where α ∈ A”.

Projection

Instead of writing π_{s}(α), we write α(s), i.e., we interpret the tuple as the corresponding function in S → ∪_{s∈S}A_{s}.

If it is not obvious from the context that s ∈ Dom(α) then writing α(s) = x implicitly means s ∈ Dom(α) ∧ α(s) = x.

This notation is also used on the product spaces themselves, i.e., A(s) is the set A_{s}, corresponding to the usual notation for applying a function to a set of arguments:

A(s) = π_{s}(A) = {π_{s}(α) |α ∈ A} = A_{s}

Extending a product

If A is a product space then A{x=M} is the product space

∏_{y∈Dom(A)∪{x}} A′_{y}

where A′_{x} = M and if y ≠ x then A′_{y} = A_{y}.

This definition allows extending the product both if the new index is in the domain of the old product and if it is not.

The same notation will also be used for elements of the products, i.e., if α ∈ A and v ∈ M then α{x=v} ∈ A{x=M}, and α{x=v} (x) = v.

Restricting a product

If A is a product then A\{x} is the product with domain Dom(A)\{x}, s.t. for y ∈ Dom(A) \ {x} we get (A \ {x})(y) = A(y).

Again, we will use the same notation on the elements of the product.

Terminology: environment

We use the word “environments” about the elements of a product space of denotable values where the index set is a set of identifiers.

1.5.2 Disjoint indexed unions

A disjoint sum of two sets is usually defined as A+B = inl(A)∪inr(B) where inl and inr are injection functions s.t. inl(A) ∩ inr(B) = ∅. Traditionally these injections are defined as inl : A → ({1} × A) and inr : B → ({2} × B) with inl(a) = (1, a) and inr(b) = (2, b), but any pair of bijective functions with disjoint images can be used.

Binary disjoint sums can be generalized to sums over arbitrary finite index sets. If for each s ∈ S we can construct a set A_{s}, then ∑_{s∈S} A_{s} = ⋃_{s∈S}{s} × A_{s} is a sum with injections in_{s} : A_{s} → {s} × A_{s} for each s in S.

Product spaces come with an associated tupling operation, and similarly a disjoint sum has an associated deconstructor. To deconstruct a sum, we use the associated case function, that for binary sums has the “type scheme”

case_{A+B} : (A → M) × (B → M) → A + B → M

and satisfies case_{A+B}(f, g)(inl(x)) = f(x) and case_{A+B}(f, g)(inr(y)) = g(y).

Generalizing to more than two summands we have the function

case : (∏_{s∈S} A_{s} → M) → (∑_{s∈S} A_{s}) → M

defined as case(p)(in_{s}(a)) = case(p)(s, a) = p(s)(a).

1.5.3 Lifting CPOs

If (D, ⊑) is the chain-complete partial order (CPO) with carrier set D and partial ordering relation ⊑, then (D_{⊥}, ⊑_{⊥}) is the “lifted” partial order with carrier set {up(x) |x ∈ D } ∪ {⊥}

If a CPO has a least element, the CPO is called pointed, and its least element is called bottom, written ⊥. A lifted CPO is always pointed, so the use of ⊥ is consistent.

If f is a function in the CPO D → E with E pointed then (f)^{†} : D_{⊥} → E is defined as (f)^{†} (⊥) = ⊥ and (f)^{†} (up(x)) = f(x).

Both the up(…) : D → D_{⊥} and (…)^{†} : (D → E) → (D_{⊥} → E) are continuous as functions from CPOs to CPOs, and the latter also preserves continuity [Win93, Chapter 8].

1.6 Overview

Section 1 describes Reynolds’s defunctionalization and related work. Sections 2 through 4 formalize the source and target languages, and define the defunctionalizing program transformation. While lengthy, these three sections uses only elementary constructions and concepts to establish the basis for the following sections. Sections 5 and 6 show that the transformation preserves typability and that it is weakly semantics preserving, i.e., it preserves the semantics of all terminating programs. Finally Section 7 describes possible extensions of the proof and suggests several directions for further work.

2 The source language

In order to formalize defunctionalization, we give a formal definition of both the source language and the target language with their denotational semantics.

As a source language we use a prototypical higher-order functional language.

2.1 Syntax

The syntax is given by the grammar in Figure 2, where x and f ranges over a set of identifiers.

τ ::= nat
| τ → τ
e ::= x
| 0
| succ(e)
| ifz(e, e, x.e)
| (fun f x : τ → τ = e)
| (e e)
p ::= Program e

Figure 2: Syntax of the source language

2.2 Typing judgments

The typing rules in Figure 3 define well-typed expressions. The judgments are of the form Γ ⊢ e : τ, where Γ is a type assignment (an environment mapping variables to types), e is an expression and τ a type, or of the form ⊢ p where p is a program (“Program e” for some expression e of type nat).

If we can derive ⊢ Program e then we say that the program is well-typed, and the derivation is called a typing derivation of the program.

Since all function abstractions include their type syntactically, for any type assignment Γ and expression e, there is at most one τ such that there exists a typing derivation of Γ⊢e : τ, and there is at most one derivation of any judgment (easy proof by induction on structure of program omitted). Therefore there can be no ambiguity when referring to the derivation of Γ⊢e : τ.

2.3 Denotational semantics

The denotational semantics used is a standard call-by-value semantics. It is given as a inductively defined function over the structure of typing derivations, so it only makes sense to talk about the denotation of an expression or a program if the expression or program is well-typed.

The denotation of a derivation is written as a function of the conclusion only, but this is just for ease of representation. The function actually takes the entire derivation as argument, and references to sub-derivations (again

\frac{Γ(x) = τ}{Γ⊢x : τ}  \overline{Γ⊢0 : nat}
\frac{Γ⊢e : nat}{Γ⊢succ(e) : nat}

\frac{Γ⊢e : nat Γ⊢e_{1} : τ Γ\{x =nat\}⊢e_{2} : τ}{Γ⊢ifz(e, e_{1}, x.e_{2}) : τ}

\frac{Γ\{f =τ_{1} →τ_{2}\}\{x =τ_{1}\}⊢e : τ_{2}}{Γ⊢(fun f x : τ_{1} → τ_{2} = e) : τ_{1} →τ_{2}}

\frac{Γ⊢e_{1} : τ_{1} →τ_{2} Γ⊢e_{2} : τ_{1}}{Γ⊢(e_{1} e_{2}) : τ_{2}}

\frac{\{\}⊢e : nat}{⊢ Program e}

Figure 3: Typing judgments for the source language

represented by their conclusions) are still compositional.

The semantic functions are shown in Figure 4. The arrow(→) in the denotation of a function type represents the continuous function space between the CPOs.

2.4 Annotated source language

The defunctionalizing transformation is inherently nonlocal, since it moves the bodies of functions from their original position in the program and into the application functions. To reference specific subexpressions of the program, we annotate each expression with a unique label taken from some countably infinite set of label identifiers.

Also, we annotate function abstractions with the variables bound by the type assignment of the expression. This annotation is of the form:

\begin{aligned}env & ::= & · \\ & | & env⟨x : τ⟩ \end{aligned}

That such an annotation really represents the type assignment is captured

S[[nat]] = N
S[[τ_{1} →τ_{2}]] = S[[τ_{1}]] → S[[τ_{2}]]_{⊥}
S[[Γ]] = ∏_{x∈Dom(Γ)} S[[Γ(x)]]
S[[Γ⊢e : τ]] : S[[Γ]] → S[[τ]]_{⊥}
S[[Γ⊢x : τ]]ρ = up(ρ(x))
S[[Γ⊢0 : nat]]ρ = up(0)
S[[Γ⊢succ(e) : nat]]ρ = (λx.up(x + 1))^{†} (S[[Γ⊢e : nat]]ρ)
S[[Γ⊢ifz(e, e_{1}, x.e_{2}) : τ]]ρ = (Ψ)^{†} (S[[Γ⊢e : nat]]ρ)

where Ψt = \{ \begin{matrix}S[[Γ⊢e_{1} : τ]]ρ & if t = 0 \\ S[[Γ\{x =nat\}⊢e_{2} : τ]]ρ\{x =t_{1}\} & if t > 0 \end{matrix}

S[[Γ⊢(fun f x : τ_{1} → τ_{2} = e) : τ_{1} →τ_{2}]]ρ

= up(fix(Ψ))

where ΨF = λX.S[[Γ{f =τ_{1} →τ_{2}}{x =τ}⊢e : τ_{2}]]ρ{f =F }{x =X}

S[[Γ⊢(e_{1} e_{2}) : τ_{2}]]ρ =

(λf.((λx.fx)^{†} (S[[Γ⊢e_{2} : τ_{1}]]ρ)))^{†} (S[[Γ⊢e_{1} : τ_{1} →τ_{2}]]ρ)

S[[⊢ p]] : N_{⊥}
S[[⊢ Program e]] = S[[{}⊢e : nat]]{}

Figure 4: Call-by-value denotational semantics of well-typed programs by the following judgment.

\overline{\{\} ⊢ ·}

\frac{Γ(x) = τ Γ \ \{x\} ⊢ env′}{Γ ⊢ env′⟨x : t⟩}

Let L be the set of labels occurring in the annotated program p. Since labels are unique, we can define a function mapping labels of L to the subderivations of ⊢p of the expression labeled by that label.

Definition 1 The PROOF (p) relation

We define a function recursively on the derivation of (annotated) expressions by.

PROOF (\frac{D}{Γ⊢e_{l} : τ} ) = \{(l, Γ⊢e_{l} : τ)\} ∪ ⋃_{d∈D} PROOF (d)

We can then show by an easy induction proof that for every Γ⊢e_{l} : τ the set PROOF (Γ⊢e_{l} : τ) defines the graph of a function from labels to derivations, since no l occurs more than once in a well-annotated program, and also that any sub-derivation of Γ⊢e : τ is in the image of PROOF (Γ⊢e : τ).

Extending this function to programs, we define

PROOF (⊢Program e_{l}) = PROOF ({}⊢e_{l} : nat)

It follows from the definition that the domain of PROOF (p) is exactly L.

We use functions for recognizing and deconstructing syntax: isfun(e) and isappl(e) are true if e is syntactically a function abstraction and respectively an application expression. If e = (fun f x : τ_{1} →τ_{2} = e′)^{env} then isfun(e) is true and

funvar(e) = f
argvar(e) = x
argtype(e) = τ_{1}
restype(e) = τ_{2}
body(e) = e′
envof(e) = env

Likewise, if e = (e_{1} e_{2}) then isappl(e) is true, funpart(e) = e_{1}, and argpart(e) = e_{2}. We do not define function deconstructing the remaining kinds of expressions, since we have no need for them.

The functions on expressions are extended to work on derivations too, by applying to the expression of the conclusion. Where the functions on expressions return subexpressions, the extended functions return the subderivation corresponding to that subexpression, e.g., funpart(Γ ⊢ (e_{1} e_{2}) : τ_{2}) = Γ ⊢ e_{1} : τ_{1} → τ_{2}. Also, we define the functions typeof(Γ ⊢ e : τ) = τ and envof(Γ⊢e : τ) = Γ.

To collect the set of all types occurring in the program p, we define typesof(p) as the set

{τ | τ ≠ nat ∧ (l, D) ∈ PROOF (p) ∧ (typeof(D) = τ ∨ (isfun(D) ∧

(argtype(D) = τ ∨ restype(D) = τ)))}

i.e., any type, other than nat, that is the type of an expression, or is the type of an argument or a result of a function. This set could equally well have been defined recursively in the structure of the derivation of p, in the same way as PROOF (p).

3 The target language

The language we want to transform our annotated source language programs into must necessarily have user-defined algebraic data-types for the translation to follow Reynolds’s method [Rey98]. It also needs mutually recursive functions, and operations on natural numbers corresponding to the ones in the source language. We do not need reflexive data-types (ones where the types themselves can occur negatively, i.e., as domain of a function type, in their own definition), since in the output of defunctionalization, the datatype constructors are first order, just as the functions.

The target language will consist of a set of mutually recursive top-level data-type definitions followed by a set of mutually recursive function definitions (with a fixed arity of two, which is all we need for the output of defunctionalization). Finally there is one expression that is evaluated in the scope of these declarations to give the result of the program.

3.1 Syntax

The syntax is more complex than for the source language, mainly due to the extra syntactic categories introduced by the top-level data-type and function declarations. It is displayed in Figure 5, where c ranges over type names (of user-defined types), C ranges over constructor names, f ranges over function names, x and y range over variable names, and v ranges over indices of records.

type  τ ::= nat | c
datadecl-list  ddl ::= · | dd and ddl
datadecl  dd ::= c = cdl
condecl-list  cdl ::= · | cd [] cdl
condecl  cd ::= C ct
con-tuple  ct ::= ⟨⟩ | ct⟨v : τ⟩
fundecl-list  fdl ::= · | fd and fdl
fundecl  fd ::= f x y : τ → τ → τ = exp
expression  exp ::= x
| 0
| succ(exp)
| ifz(exp, exp, x.exp)
| f exp exp
| C at
| case exp of ml
| let x = exp in exp
arg-tuple  at ::= ⟨⟩ | at⟨v = exp⟩
match-list  ml ::= · | m [] ml
match  m ::= C mt => exp
match-tuple  mt ::= ⟨⟩ | mt⟨v = x⟩
program  p ::= datatype ddl
fun fdl in exp

Figure 5: Syntax of the target language

3.2 Typing judgments

The target language is also typed. There will be a typing judgment for each syntactical category.

In the following, O ⊆ TypeID is a set of type names (ranged over by c ∈ TypeID in the syntax), Ω is an environment from type names to a Δ, where Δ is an environment from constructor names (C ∈ ConID) to tuple representations, V, where V again is an environment from label identifiers (v ∈ LabelID) to types. Also, Φ is a map from function-names to triples of types and Γ is a map from variable-names to types, i.e., a type assignment.

Notice that τ is used for types in both the source and the target language. It will be obvious from the context which is meant by an instance of τ. The typing judgment schema are as given below.

type: O ⊢ τ

\overline{O ⊢ nat}  \frac{c ∈ O}{O ⊢ c}

datadecl-list: O ⊢ddl : Ω

\overline{O ⊢· : \{\}}  \frac{O ⊢dd : (c, Δ) O ⊢ddl : Ω}{O ⊢dd and ddl : Ω\{c=Δ\}}

datadecl: O ⊢dd : (c, Δ)

\frac{O ⊢cdl : Δ}{O ⊢c = cdl : (c, Δ)}

condecl-list: O ⊢cdl : Δ

\overline{O ⊢· : \{\}}  \frac{O ⊢cd : (C, V) O ⊢cdl : Δ}{O ⊢cd[]cdl : Δ\{C =V\}}

condecl: O ⊢cd : (C, V)

\frac{O ⊢ct : V}{O ⊢C ct : (C, V)}

con-tuple: O ⊢ct : V

\overline{O ⊢⟨⟩ : \{\}}  \frac{O ⊢ct : V O ⊢ τ}{O ⊢ct⟨v : τ⟩: V\{v =τ\}}

fundecl-list: Ω, Φ⊢fdl : Φ′

\overline{Ω, Φ⊢· : \{\}}  \frac{Ω, Φ⊢fd : (f, (τ_{1}, τ_{2}, τ_{3})) Ω, Φ⊢fdl : Φ′}{Ω, Φ⊢fd and fdl : Φ′\{f =(τ_{1}, τ_{2}, τ_{3})\}}

fundecl: Ω, Φ⊢fd : (f, (τ_{1}, τ_{2}, τ_{3}))

\frac{Ω, Φ, \{x = τ_{1}, y = τ_{2}\}⊢e : τ_{3}}{Ω, Φ⊢f x y : τ_{1} → τ_{2} → τ_{3} = e : (f, (τ_{1}, τ_{2}, τ_{3}))}

expression: Ω, Φ, Γ⊢exp : τ

\frac{Γ(x) = τ Dom(Ω) ⊢ τ}{Ω, Φ, Γ⊢x : τ}

\overline{Ω, Φ, Γ⊢0 : nat}

\frac{Ω, Φ, Γ⊢e : nat}{Ω, Φ, Γ⊢succ(e) : nat}

\frac{Ω, Φ, Γ⊢e : nat Ω, Φ, Γ⊢e_{1} : τ Ω, Φ, Γ\{x =nat\}⊢e_{2} : τ}{Ω, Φ, Γ⊢ifz(e, e_{1}, x.e_{2}) : τ}

\frac{Φ(f) = (τ_{1}, τ_{2}, τ_{3}) Ω, Φ, Γ⊢e_{1} : τ_{1} Ω, Φ, Γ⊢e_{2} : τ_{2}}{Ω, Φ, Γ⊢f e_{1} e_{2} : τ_{3}}

\frac{Ω(c)(C) = V Ω, Φ, Γ⊢at : V}{Ω, Φ, Γ⊢C at : c}

\frac{Ω, Φ, Γ⊢e : c Ω, Φ, Γ⊢ml : c ⇒τ}{Ω, Φ, Γ⊢case e of ml : τ}

\frac{Ω, Φ, Γ⊢e_{1} : τ_{1} Ω, Φ, Γ\{x =τ_{1}\}⊢e_{2} : τ_{2}}{Ω, Φ, Γ⊢let x = e_{1} in e_{2} : τ_{2}}

arg-tuple: Ω, Φ, Γ⊢at : V

\overline{Ω, Φ, Γ⊢⟨⟩ : \{\}}  \frac{Ω, Φ, Γ⊢at : V \ \{v\} V(v) = τ Ω, Φ, Γ⊢e : τ}{Ω, Φ, Γ⊢at⟨v = e⟩: V}

match-list: Ω, Φ, Γ⊢ml : c ⇒τ

\overline{Ω, Φ, Γ⊢· : c ⇒τ}  \frac{Ω, Φ, Γ⊢ml : c ⇒τ Ω, Φ, Γ⊢m : c ⇒τ}{Ω, Φ, Γ⊢m [] ml : c ⇒τ}

match: Ω, Φ, Γ⊢m : c ⇒τ

\frac{Ω(c)(C) = V Γ, V ⊢mt : Γ′ Ω, Φ, Γ′ ⊢e : τ}{Ω, Φ, Γ⊢C mt => e : c ⇒τ}

match-tuple: Γ, V ⊢mt : Γ′

\overline{Γ, \{\}⊢⟨⟩ : Γ}  \frac{Γ, V \ \{v\}⊢mt : Γ′ V(v) = τ}{Γ, V ⊢mt⟨v = x⟩: Γ′\{x=τ\}}

program: ⊢ p

\frac{Dom(Ω)⊢ddl : Ω Ω, Φ⊢fdl : Φ Ω, Φ, \{\}⊢e : nat}{⊢ datatype ddl fun fdl in e}

3.3 Denotational semantics

Again we give a denotation to the derivations for each syntactic category and to Ω, Φ, etc.

We will let Set be the class of sets, ordered by inclusion. This ordering is a pointed partial order (has a least element: the empty set) and is closed under least upper-bounds (unions) of ω-chains, but it is not a partially ordered set.

Working in something that is not a set is not in itself a problem, since we will only referring to its elements, which are sets, and functions mapping sets to sets, but we will need a fixed point of some sort on this construction. The semantic domains are as follows.

D[[O]] = ∏_{c∈O} Set = Set^{O}
D[[O ⊢ Ω]] : D[[Dom(O)]] → D[[Dom(O)]]

Notice that the meaning of a user-defined type is a set.

When we write D[[O ⊢ Ω]], the function is actually defined on the entire derivation of the conclusion O ⊢ Ω. For ease of reading, we omit the derivation. Also, if the argument of a semantic function matches the format of the conclusion of a rule exactly, then only the expression is given (e.g., instead of [[Ω, Φ, Γ⊢e : τ]] we just write [[e]]). This shorthand is still unambiguous, since there is exactly one rule corresponding to each element of each syntactic category.

If o ∈ D[[O]] for the O in O ⊢ Ω then

D[[Ω]]^{o} = ∏_{c∈Dom(Ω)} D_{s}[[Ω(c)]]^{o}
D[[Δ]]^{o} = ∏_{C∈Dom(Δ)} D[[Δ(C)]]^{o}

D_{s}[[Δ]]^{o} = ∑_{C∈Dom(Δ)} D[[Δ(C)]]^{o}
D[[V]]^{o} = ∏_{v∈Dom(V)} D[[V(v)]]^{o}

D[[Φ]]^{o} = ∏_{f∈Dom(Φ)} D[[τ_{1}]]^{o} → D[[τ_{2}]]^{o} → D[[τ_{3}]]_{⊥}^{o}
where (τ_{1}, τ_{2}, τ_{3}) = Φ(f)
D[[Γ]]^{o} = ∏_{x∈Dom(G)} D[[Γ(x)]]^{o}

The first argument, o ∈ D[[Dom(Ω)]], is written in superscript only to indicate that it will be passed unchanged in any recursive calls, i.e., it can be considered a constant for the expression.

Expanding the definition, we see that D[[Ω]]^{o}, the meaning of the type declarations, can be written more readably as follows.

D[[Ω]]^{o} = ∏_{c∈Dom(Ω)} ∑_{C∈Dom(Ω(c))} ∏_{x∈Dom(Ω(c)(C))} D[[Ω(c)(C)(x)]]^{o}

In the following, we use the same convention as in the definition of the denotation of the source language: the semantic functions take full derivations as arguments, even though only the conclusion is written, and references to the premises are allowed and considered compositional.

type: To each type expression in the language we assign a set.

\begin{aligned}D[[O ⊢ τ]] & : & D[[O]] → Set \\ D[[O ⊢ nat]]^{o} & = & N \\ D[[O ⊢ c]]^{o} & = & o(c) \end{aligned}

datadecl-list

D[[O ⊢ddl : Ω]] : D[[Ω]]
D[[O ⊢· : {}]]^{o} = {}
D[[O ⊢dd and ddl : Ω]]^{o} = (D[[ddl]]^{o}){c=δ_{s}}
where (c, δ_{s}) = D[[dd]]^{o}

datadecl

D[[O ⊢dd : (c, Δ)]]^{o} : TypeID × D_{s}[[Δ]]^{o}
D[[O ⊢c = cdl : (c, Δ)]]^{o} = (c, ∑_{C∈Dom(δ)} δ(C))
where δ = D[[cdl]]^{o}

condecl-list

D[[O ⊢dcl : Δ]]^{o} : D[[Δ]]^{o}
D[[O ⊢· : {}]]^{o} = {}
D[[O ⊢cd [] cdl : Δ]]^{o} = D[[cdl]]^{o}{C =v}
where (C, v) = D[[cd]]^{o}

condecl

D[[O ⊢C ct : (C, V)]]^{o} : ConID × D[[V]]^{o}
D[[O ⊢C ct : (C, V)]]^{o} = (C, D[[ct]]^{o})

con-tuple

\begin{aligned}D[[O ⊢ct : V]]^{o} & : & D[[V]]^{o} \\ D[[O ⊢⟨⟩ : \{\}]]^{o} & = & \{\} \\ D[[O ⊢ct⟨v : τ⟩: V]]^{o} & = & D[[ct]]^{o}\{v =D[[τ]]^{o}\} \end{aligned}

fundecl-list

D[[Ω, Φ⊢fdl : Φ′]]^{o} : D[[Φ]]^{o} → D[[Φ′]]^{o}
D[[Ω, Φ⊢· : {}]]^{oϕ} = {}
D[[Ω, Φ⊢fd and fdl : {}]]^{oϕ} = D[[fdl]]^{oϕ}{f =F }
where (f, F) = D[[fd]]^{oϕ}

fundecl

D[[Ω, Φ⊢fd : (τ_{1}, τ_{2}, τ_{3})]]^{oϕ} : D[[τ_{1}]]^{o} → D[[τ_{2}]]^{o} → D[[τ_{3}]]_{⊥}^{o}
D[[Ω, Φ⊢f x y : τ_{1} → τ_{2} → τ_{3} = e : (τ_{1}, τ_{2}, τ_{3})]]^{oϕ} =
λX_{1}.λX_{2}.D[[e]]^{oϕ}{x = X_{1}, y = X_{2}}

exp

D[[Ω, Φ, Γ⊢e : τ]]^{o} : D[[Φ]]^{o} → D[[Γ]]^{o} → D[[τ]]^{o}_{⊥}
D[[Ω, Φ, Γ⊢x : τ]]^{oϕ}ρ = up(ρ(x))
D[[Ω, Φ, Γ⊢0 : nat]]^{oϕ}ρ = up(0)
D[[Ω, Φ, Γ⊢ifz(e, e_{1}, x.e_{2}) : τ]]^{oϕ}ρ = (ψ)^{†} (D[[Ω, Φ, Γ⊢e : nat]]^{oϕ}ρ)

where ψ(n) = \{ \begin{matrix}D[[e_{1}]]^{oϕ}ρ & if n = 0 \\ D[[e_{2}]]^{oϕ}ρ\{x =n − 1\} & if n > 0 \end{matrix}

D[[Ω, Φ, Γ⊢f e_{1} e_{2} : τ]]^{oϕ}ρ =

(λX_{1}. (λX_{2}.ϕ(f) X_{1} X_{2})^{†} (D[[e_{2}]]^{oϕ}ρ))^{†} (D[[e_{1}]]^{oϕ}ρ)

D[[Ω, Φ, Γ⊢C at : c]]^{oϕ}ρ = (in_{C}())^{†}(D[[at]]^{oϕ}ρ)
D[[Ω, Φ, Γ⊢case e of ml : τ]]^{oϕ}ρ =

(λX.case(D[[Ω, Φ, Γ⊢ml : c ⇒τ]]^{oϕ}ρ)(X))^{†} (D[[e]]^{oϕ}ρ)

D[[Ω, Φ, Γ⊢let x = e_{1} in e_{2} : τ_{2}]]^{oϕ}ρ =

(λX.D[[e_{2}]]^{oϕ}ρ{x =X})^{†} (D[[e_{1}]]^{oϕ}ρ) arg-tuple

D[[Ω, Φ, Γ⊢at : V]]^{o}ρ : D[[Φ]]^{o} → D[[Γ]]^{o} → D[[V]]_{⊥}^{o}
D[[Ω, Φ, Γ⊢⟨⟩ : {}]]^{oϕ}ρ = up({})
D[[Ω, Φ, Γ⊢at⟨v = e⟩: V]]^{oϕ}ρ =
(λX. (λV.up(V {x=X}))^{†} (D[[at]]^{oϕ}ρ))^{†} (D[[e]]^{oϕ}ρ)

match-list

D[[Ω, Φ, Γ⊢ml : c ⇒τ]]^{o} :

D[[Φ]]^{o} → D[[Γ]]^{o} → ∏_{C∈Dom(o(c))} (o(c)(C) → D[[τ]]_{⊥}^{o})

D[[Ω, Φ, Γ⊢· : c ⇒τ]]^{oϕ}ρ = Ψ

where Dom(Ψ) = Dom(o(c)) and

Ψ(C) = λX.⊥

D[[Ω, Φ, Γ⊢m [] ml : c ⇒τ]]^{oϕ}ρ = (D[[ml]]^{oϕ}ρ){C =F }

where (C, F) = D[[m]]^{oϕ}ρ

match

D[[Ω, Φ, Γ⊢C mt => e : c ⇒τ]]^{o} :
D[[Φ]]^{o} → D[[Γ]]^{o} → ConID × (o(c)(C) → D[[τ]]_{⊥}^{o})

D[[Ω, Φ, Γ⊢C mt => e : c ⇒τ]]^{oϕ}ρ = (C, λV.D[[e]]^{oϕ}(D[[mt]]^{o}ρV))

match-tuple

D[[Γ, V ⊢mt : Γ′]]^{o} : D[[Γ]]^{o} → D[[V]]^{o} → D[[Γ′]]^{o}
D[[Γ, V ⊢⟨⟩ : Γ]]^{o}ρν = ρ
D[[Γ, V ⊢mt⟨v = x⟩: Γ]]^{o}ρν = (D[[mt]]^{o}ρ){x =ν(v)}

program

D[[⊢ p]] : N_{⊥}
D[[⊢ datatype ddl fun fdl in e]] = D[[e]]^{oϕ}
where o = fix(λo.D[[ddl]]^{o})
ϕ = fix(λϕ.D[[fdl]]^{oϕ})

3.4 Comments

One can check that for any fixed element o ∈ D[[O]], and for any element of any of the syntactic categories, S, D[[S]]^{o} actually has the “type” stated next to its definition. Whereas most of the above definitions are given using standard notation for writing continuous functions between domains (as in [Win93, section 8]), and as such the fixed point used to find the recursive closure of the meaning of the function definitions is known to exist, there is one exception.

The part that is a source of possible problems is the fixed point of the function D[[ddl]], which has type D[[Ω]] → D[[Ω]]. If D[[Ω]] had been a chaincomplete partial order, we would just have used the usual fixed point theorems, but it is not even a set. It is defined to be a product of sets, and with no further restrictions, for all we know it belongs to something at least as “big” as the class of all sets.

We will not be using domain-theoretic methods then. Instead the meaning is purely set-theoretic. Since we are defining algebraic, not reflexive, data-types, the recursive set equations we need to solve are all defined “positively” (nothing that is being defined is used in a negative position, e.g., as the domain of a function space, since there are no function spaces at all), so we don’t need the methodology of domains for this case. All we define are countable sets.

What we mean when we write “fix” is then the union of the chain of (products of) countable sets, which is ordered by inclusion. It is easy to show that given a product (over the associated index set) of sets, o, the denotation D[[C_{p}]]o is again a product of sets (actually a product of sums of products of sets), since the only operations we use are products and disjoint sums of sets, which again define sets.

Iterating D[[C_{p}]] on the empty set defines the chain ordered by inclusion:

D[[C_{p}]]^{n}( ∏_{c_{τ} ∈Dom(Ω_{p})} ∅)

(i.e., D[[C_{p}]]^{n}(∅)), and as unions over sets of sets are always defined

⋃_{n∈N} D[[C_{p}]]^{n}(∅)

is again a well-defined and countable set. The elements form a chain because product and sum construction are monotone in their arguments. We will let this be the definition of fix(λo.D[[ddl]]^{o}).

4 The defunctionalizing transformation

The transformation we have been aiming at translates well-typed programs in the (annotated) source language to well-typed programs in the target language, while preserving the meaning of the program. The transformation turns all function declarations into constructions of a value containing information about the environment at the abstraction point. Applications of such values are transformed into case-constructs that decomposes the value and evaluates the appropriate function body in an environment corresponding to the environment in which the value was constructed. The transformation is given as a function of the typing derivations of a program in the source language.

In the remainder of the article, the program p is fixed, allowing us to write PROOF (l) as shorthand for PROOF (p) (l), and everywhere we write Γ ⊢ e : τ it will not only mean that Γ ⊢ e : τ is derivable, but also that the derivation of that judgment is part of the derivation of ⊢p, i.e., the judgment is in the image of PROOF (p). Also, we choose two identifiers, call them ff and xx, that do not occur in p.

4.1 Definition of the transformation

The functions are defined using the usual shorthand for functions on derivations, and they even abbreviate the argument. Instead of writing T [Γ⊢e : τ] we will leave out everything except e if it corresponds verbatim to the conclusion of the rule schema. We create index identifiers from normal identifiers by underlining, representing some injective mapping from normal identifiers into the set of index identifiers.

First, we transform the expressions.

T [τ] : type
T [nat] = nat
T [τ_{1} →τ_{2}] = c_{τ_{1}→τ_{2}}
T_{v} [env] : arg-tuple
T_{v} [⟨⟩] = ⟨⟩
T_{v} [env⟨x : τ⟩] = T_{v} [env]⟨\underline{x} = x⟩
T [e] : exp
T [x] = x
T [0] = 0
T [succ(e)] = succ(T [e])
T [ifz(e, e_{1}, x.e_{2})] = ifz(T [e] , T [e_{1}] , x.T [e_{2}])
T [(fun f x : τ_{1} →τ_{2} = e)_{l}^{env}] = C_{l} T_{v} [env]
T [(e_{1} e_{2})] = app_{τ_{1}→τ_{2}} T [Γ⊢e_{1} : τ_{1} →τ_{2}] T [e_{2}]

Then we build the data-type declarations, C_{p}, and function declarations, F_{p}.

In the following we use a translation from finite sets to lists, listof (S), where lists are either nil or x::xs where xs is again a list. It is not important how this translation works, but to make it a function, let us just decide that it gives us the sorted list of the set elements with regard to some total ordering. The two types of sets we work on are sets of types in the source language (elements of the syntactic category τ) and labels (ranged over by l). We can impose a total order on the syntax of types by, e.g., saying that nat is less than everything else, and τ_{1} →τ_{2} is less than τ′_{1} →τ′_{2} if τ_{2} is less than τ′_{2} or τ_{2} = τ′_{2} and τ_{1} is less than τ′_{1}.

That is, we can define listof (S) as

listof (∅) = nil
listof (S) = (min(S))::listof (S \ {min(S)}) if S ≠ ∅

as any finite and totally ordered set has a least element.

We will say that y member of (x:: xs) if x = y or y member of xs, and then we have the property that x ∈ S ⟺ x member of listof (S).

Using this way of ordering our types, we can define the datatype declarations corresponding to functions in the source program in a fixed order.

C_{p} : datadecl-list
C_{p} = C_{c}[listof ({τ |τ ∈ typesof(p)})]
C_{c}[…] : type list → datadecl-list
C_{c}[nil] = ·
C_{c}[τ::tl] = c_{τ} = C_{C}[listof ({l |PROOF (l) = D ∧ isfun(D) ∧ typeof(D) = τ })]
and C_{c}[tl]
C_{C}[…] : label list → condecl-list
C_{C}[nil] = ·
C_{C}[l::ls] = C_{l} C_{v}[envof(PROOF (l))] []C_{C}[ls]
C_{v}[…] : env → contuple
C_{v}[⟨⟩] = ⟨⟩
C_{v}[ct⟨x : τ⟩] = C_{v}[ct]⟨\underline{x} : T [τ]⟩

These functions construct a list of data-type declarations. We define one for each function type occurring in the program. The declarations of the associated application functions are generated as follows.

F_{p} : fundecl-list
F_{p} = F_{c}[listof ({τ |τ ∈ typesof(p)})]
F_{c}[…] : type list → fundecl-list
F_{c}[nil] = ·
F_{c}[τ_{1} →τ_{2} ::tl] = app_{τ_{1}→τ_{2}} ff xx : T [τ_{1} →τ_{2}] → T [τ_{1}] → T [τ_{2}] =
case ff
of F_{C}[listof (\{l | \begin{matrix}PROOF (l) = D ∧ isfun(D) \\ ∧ typeof(D) = τ \end{matrix} \})]
and F_{c}[tl]
F_{C}[…] : label list → match-list
F_{C}[nil] = ·
F_{C}[l::ls] = C_{l} (F_{v}[env]) => (let f = ff in let x = xx in T [e]) [] F_{C}[ls]

where PROOF (l) = Γ⊢(fun f x : τ_{1} →τ_{2} = e)_{l}^{env} : τ_{1} →τ_{2}

F_{v}[…] : env → match-tuple
F_{v}[⟨⟩] = ⟨⟩
F_{v}[vt⟨x : τ⟩] = F_{v}[vt]⟨\underline{x} = x⟩

where ff and xx are “fresh” variables, i.e., variables that does not appear in the program, p, at all.

Finally, we transform the program by adding the datatype- and function declarations we constructed above to the transformation of the main expression.

T [Program e] = datatype C_{p} fun F_{p} in T [e]

4.2 Comments on the transformation

Notice that we create data-types for any type appearing in the program (typesof(p) is any type, other than nat, mentioned in the program, i.e., as either domain, codomain, or function type of a function declaration), but not all of them will have constructors. In the case

Program((fun f x : ((nat →nat) →nat) →nat = 0)_{l}^{⟨⟩}
(fun g y : (nat →nat) →nat = (y 0))_{l′}^{⟨⟩})_{l′′}

we have nat →nat occurring in the program, so we need to define c_{nat→nat} in the translated program. Otherwise the translation of the above program would not type check, since the translation of nat → nat would not be a defined type. In this program there are no values of type nat → nat, and there will not be any constructors of type c_{nat→nat} in the translated program either. There is also an application-point where the function has type nat → nat, so we define a function app_{nat→nat} with a case-expression with an empty match-list.

5 Type preservation

The translation given in the preceding section translates programs in the source language into programs in the target language. In order for the translation to preserve the semantics of programs, it necessarily have to generate only well-typed programs, since the semantics of a program in the target language is undefined unless the program is well-type. This section shows that the translation generates only well-typed programs.

Formally, since we have fixed a program p, we need to prove that if ⊢ Program e then ⊢ datatype C_{p} fun F_{p} in T [e], where C_{p} and F_{p} are as defined by the translation.

To this end we show the premises of this rule: There exists Ω and Φ s.t. Dom(Ω)⊢C_{p} : Ω, Ω, Φ⊢F_{p} : Φ, and Ω, Φ, {}⊢T [e] : nat.

The following sections define such Ω_{p} and Φ_{p} and show that they satisfy the requirements.

5.1 Defining solutions to typing judgments

To prove the existence of Ω and Φ satisfying the premises for the welltypedness of a program, we define two such mappings.

Define Ω_{p} by

• Dom(Ω_{p}) = {c_{τ} |τ ∈ typesof(p)}

• Dom(Ω_{p}(c_{τ})) = {C_{l} |PROOF (l) = D ∧ isfun(D) ∧ typeof(D) = τ }

• Dom(Ω_{p}(c_{τ})(C_{l})) = \{\underline{x} |x ∈ Dom(envof(PROOF (l)))\}

• Ω_{p}(c_{τ})(C_{l})(\underline{x}) = T [envof(PROOF (l) (x))]

The above rules uniquely define Ω_{p}, since it gives both the domain of each indexed product as well as the value at each projection. It defines an object of the right “type” for an Ω (an environment from type names to environments from constructor names to environments from label names to types), and we can also prove that it satisfies Dom(Ω_{p})⊢C_{p} : Ω_{p}, Define Φ_{p} by

• Dom(Φ_{p}) = \{app_{τ_{1}→τ_{2}} | \begin{matrix}PROOF(l) = D ∧ isappl(D) \\ ∧ funtype(D, τ_{1} →τ_{2}) \end{matrix} \}

where

funtype(D, τ) = (isappl(D) ∧ typeof(funpart(D)) = τ) ∨

(isfun(D) ∧ typeof(D) = τ)

• Φ_{p}(app_{τ_{1}→τ_{2}}) = (T [τ_{1} →τ_{2}] , T [τ_{1}] , T [τ_{2}])

Again the above defines something of the right type (environment from function-names to type triples), and we can prove that Ω_{p}, Φ_{p} ⊢F_{p} : Φ_{p}.

Most of the proofs will be omitted from this article, since the main point is the semantic equivalence, not the preservation of typability, and the proofs are not themselves technically challenging. Also, Bell et al. [BBH97] have already shown that their translation preserves typability, so type preservation should not come as a surprise.

5.2 Data-type declarations are well-typed

The construction of Ω_{p} allows us to prove

Dom(Ω_{p})⊢C_{p} : Ω_{p}

by induction on the definition of C_{p}. It is a simple proof by unfolding the definition and checking each part, with induction proofs over the lists that are arguments to C_{c}[…] and C_{C}[…]. The proof has been omitted for brevity.

5.3 Expressions are well-typed

We can prove that if Γ ⊢ e : τ, then Ω_{p}, Φ_{p}, Γ′ ⊢ T [e] : T [τ] for any Γ′ that extends Γ, where “extends” is defined as follows.

Definition 2 Γ′ extends Γ

We will say that a type assignment in the target language Γ′ extends a type assignment in the source language Γ, if Dom(Γ) ⊆ Dom(Γ′) and ∀x ∈ Dom(Γ).Γ′(x) = T [Γ(x)].

We prove that for any sub-derivation, Γ ⊢ e : τ, of the derivation of p that

(Γ⊢e : τ ∧ Γ′ extends Γ) ⇒ Ω_{p}, Φ_{p}, Γ′ ⊢T [Γ⊢e : τ] : T [τ]

Proof.

The proof is by structural induction on the structure of the derivation (or, equivalently, on the structure of the expression e). The details can be seen in Appendix A.

5.4 Function declarations are well-typed

The last premise to show is

Ω_{p}, Φ_{p} ⊢F_{p} : Φ_{p}

Showing this is done using the same methods as for Ω_{p}, i.e., by showing that it works for any part of Φ_{p}, expanding its definition, and using inductions over the list-arguments to F_{c}[…] and F_{C}[…]. There is nothing subtle in this proof either, and it too has been omitted for brevity.

5.5 Summary and conclusion

We have shown that if the source program, p = Program e, is well-typed, and if Ω_{p} and Φ_{p} are chosen as described then Dom(Ω_{p})⊢C_{p} : Ω_{p}, Ω_{p}, Φ_{p} ⊢ F_{p} : Φ_{p}, and Ω_{p}, Φ_{p}, {} ⊢ T [e] : T [nat]. From these premises, we can infer that ⊢ datatype C_{p} fun F_{p} in T [e], i.e., that ⊢ T [p].

This result guarantees that the denotation of the translated program is defined. In the next section we show that the translation preserves the meaning of any terminating program.

6 Meaning preservation

In this section we show that the transformation is weakly correct, i.e., if the original program terminates (evaluates to a non-bottom value), then so does the translated program, and with the same value. It makes sense to use equality as the desired relation between the results, since the denotation of both source and destination programs have the same type: lifted natural numbers.

The proof will be by logical relations as described in, e.g., Mitchell’s textbook [Mit93].

We consider a single given program, so C_{p} and F_{p} are given. In the following we will let o =^{def} fix(λo.D[[C_{p}]]^{o}) and ϕ =^{def} fix(λϕ.D[[F_{p}]]^{oϕ}).

The following subsections relate the functions in ϕ to the functions in the original program, define the logical relation, prove that the translation of any expression gives expressions that are related by the logical relation, and finally extend this result to entire programs.

6.1 Properties of the semantics of the program

We need a few lemmas for the main proof.

Lemma 1 If PROOF (l) = Γ ⊢ (fun f x : τ_{1} → τ_{2} = e)^{env} : τ_{1} → τ_{2} and Γ′ extends Γ and ρ′ ∈ D[[Γ′]]^{o} then

D[[T_{v} [env]]]^{oϕ}ρ′ = up(ν)

where Dom(ν) = \{\underline{x} |x ∈ Dom(Γ)\} and ν(\underline{x}) = ρ′(x).

Proof of Lemma 1 (sketched). Simple induction on the length of env, since T_{v} [env⟨x : t⟩] = T_{v} [env]⟨\underline{x} = x⟩ so all expressions are variables, and as such cannot denote bottom, and then

D[[T_{v} [env]⟨\underline{x} = x⟩]]^{oϕ}ρ′ = ((λE.up(E\{\underline{x}=ρ′(x)\})))^{†} (D[[T_{v} [env]]]^{oϕ}ρ′)

Lemma 2 If PROOF (l) = Γ ⊢ (fun f x : τ_{1} → τ_{2} = e)^{env} : τ_{1} → τ_{2} and Γ′ extends Γ and ρ′ ∈ D[[Γ′]]^{o} then

ϕ(app_{τ_{1}→τ_{2}})(in_{C_{l}}(ν))b = D[[F_{C}[ll]]]^{oϕ}{ff = in_{C_{l}}(ν), xx = b}(C_{l})(ν)

where up(ν) = D[[T_{v} [env]]]^{oϕ}ρ′ (which by Lemma 1 isn’t bottom) and

ll = listof ({l |PROOF (l) = D ∧ isfun(D) ∧ typeof(D) = τ_{1} →τ_{2} })

Proof of Lemma 2. By definition of being a fixed point ϕ(app_{τ_{1}→τ_{2}}) = D[[F_{p}]]^{oϕ}(app_{τ_{1}→τ_{2}}), and by simple induction on the way F_{p} is constructed it follows that

D[[F_{p}]]^{oϕ}(app_{τ_{1}→τ_{2}}) = λF.λX.D[[case ff of F_{C}[ll]]]^{oϕ}{ff = F, xx = X}

where ll = listof ({l |PROOF (l) = D ∧ isfun(D) ∧ typeof(D) = τ_{1} →τ_{2} }).

If we let g = in_{C_{l}}(ν) (remember that in_{C_{l}}(ν) = (C_{l}, ν)) then this allows us to show

D[[F_{p}]]^{oϕ}(app_{τ_{1}→τ_{2}})(g)(b)

= D[[case ff of F_{C}[ll]]]^{oϕ}{ff = g, xx = b}
= (λX.case(D[[F_{C}[ll]]]^{oϕ}{ff = g, xx = b})(X))^{†} (D[[ff]]^{oϕ}{ff = g, xx = b})
= case(D[[F_{C}[ll]]]^{oϕ}{ff = g, xx = b})(g)
= (D[[F_{C}[ll]]]^{oϕ}{ff = g, xx = b})(π_{1}(g))(π_{2}(g))
= (D[[F_{C}[ll]]]^{oϕ}{ff = g, xx = b})(C_{l})(ν)

as needed.

Lemma 3 If PROOF (l) = Γ⊢(fun f x : τ_{1} →τ_{2} = e)^{env} : τ_{1} →τ_{2}, Γ ⊢ env, Γ′ extends Γ, ρ′ ∈ D[[Γ′]]^{o} and ν satisfies that Dom(ν) = \{\underline{x} |x ∈ Dom(Γ)\} and ν(\underline{x}) = ρ′(x) then

D[[F_{v}[env]]]^{oϕ}{ff = g, xx = b}(ν) = ρ′′

implies Dom(ρ′′) = Dom(Γ) ∪ {ff, xx} and ∀x ∈ Dom(Γ).ρ′′(x) = ρ′(x), ρ′′(ff) = g, and ρ′(xx) = b.

Proof of Lemma 3. The proof is (indirectly) by induction on the structure of env. The actual induction is on the size of Dom(Γ), which relates to env as we know Γ ⊢ env by inversion.

The details can be seen in Appendix B.

Lemma 4 If PROOF (l) = Γ ⊢ (fun f x : τ_{1} → τ_{2} = e)^{env} : τ_{1} → τ_{2}, Γ′ extends Γ, ρ′ ∈ D[[Γ′]]^{o} and up(ν) = D[[T_{v} [env]]]^{oϕ}ρ′, and if l member of ll then

D[[F_{C}[ll]]]^{oϕ}{ff = g, xx = b}(C_{l})(ν) = D[[T [e]]]^{oϕ}ρ′′

where Dom(ρ′′) = Dom(Γ) ∪ {ff, xx, f, x} and ∀x ∈ Dom(Γ) \ {f, x}.ρ′′(x) = ρ′(x), ρ′′(ff) = ρ′′(f) = g, and ρ′(xx) = ρ′′(x) = b.

Proof of Lemma 4. If l member of ll then we can easily show by induction on the list that

D[[F_{C}[ll]]]^{oϕ}{ff = g, xx = b}(C_{l})(ν)

= D[[let f = ff in let x = xx in T [e]]]^{oϕ}(D[[F_{v}[env]]]^{o}{ff = g, xx = b}(ν))

By Lemma 3 we know that

D[[F_{v}[env]]]^{oϕ}{ff = g, xx = b}(ν) = ρ′′

such that Dom(ρ′′) = Dom(Γ) ∪ {ff, xx} and ρ′′(xx) = b, ρ′′(ff) = g, and for x ∈ Dom(Γ) we have ρ′′(x) = ρ′(x).

By expanding the definitions we can see that

D[[let f = ff in let x = xx in T [e]]]^{oϕ}ρ′′

= (λX.D[[let x = xx in T [e]]]^{oϕ}ρ′′{f =X})^{†} (D[[ff]]^{oϕ}ρ′′)
= D[[let x = xx in T [e]]]^{oϕ}ρ′′{f =g}
= D[[T [e]]]^{oϕ}ρ′′{f =g}{x=b}

and ρ′′{f =g}{x=b} exactly satisfies the requirements of the lemma.

Theorem 1 If Γ ⊢ (fun f x : τ_{1} → τ_{2} = e)_{l}^{env} : τ_{1} → τ_{2}, Γ′ extends Γ, ρ ∈ D[[Γ′]]^{o}, and up(ν) = D[[T_{v} [env]]]^{oϕ}ρ′ then

ϕ(app_{τ})(in_{C_{l}}(ν))b = D[[T [e]]]^{oϕ}ρ′′

where Dom(ρ′′) = Dom(ρ) ∪ {ff, xx, x, f} and ρ′′(x) = ρ′′(xx) = b, ρ′′(f) = ρ′′(ff) = in_{C_{l}}(ν), and y ∈ Dom(Γ) \ {f, x} ⇒ ρ′′(y) = ρ′(y).

Proof of Theorem 1. By Lemma 1 we know that if up(ν) = D[[T_{v} [env]]]^{oϕ}ρ′ then ∀x ∈ Dom(Γ).ν(\underline{x}) = ρ′(x), so we can use Lemma 2, from which we know that

ϕ(app_{τ})(in_{C_{l}}(ν))b = D[[F_{C}[ll]]]^{oϕ}{ff = in_{C_{l}}(ν), xx = b}(C_{l})(ν)

By Lemma 4 we know that

D[[F_{C}[ll]]]^{oϕ}{ff = in_{C_{l}}(ν), xx = b}(C_{l})(ν) = D[[T [e]]]^{oϕ}ρ′′

where ρ′′ is exactly the environment claimed in the theorem.

6.2 Definition of the logical relation

We define the type-indexed families of relations ≺_{τ} and ⪯_{τ} between S[[τ]] and D[[T [τ]]]^{o}, and between S[[τ]]_{⊥} and D[[T [τ]]]^{o}_{⊥} respectively, as given in Figure 6.

n ≺nat m iff n = m
f ≺_{τ_{1}→τ_{2}} g iff ∀a ≺_{τ_{1}} b.fa ⪯_{τ_{2}} ϕ(app_{τ_{1}→τ_{2}})gb
x ⪯_{τ} y iff x = ⊥ ∨ (∃x′, y′.x = up(x′) ∧ y = up(y′) ∧ x′ ≺_{τ} y′)

Figure 6: The logical relation

These relations satisfy that for any g ∈ D[[T [τ_{1} →τ_{2}]]]^{o} and any y ∈ D[[T [τ]]]^{o}_{⊥} the relations over S[[τ_{1} →τ_{2}]] and S[[τ]]_{⊥}, defined as {f |f ≺_{τ_{1}→τ_{2}} g } and {x |x ⪯_{τ} y }, are inclusive. That is, the relations contains the bottom of the corresponding domains and they are closed under least upper bounds of ω-chains.

This can be shown by well-founded induction on the structure of types and the dependencies between the relations, and noticing that the relations are all constructed as intersections and inverse images by strict continuous functions of smaller relations, which according to [Win93, Chapter 10] guarantees that the relations are inclusive if the smaller ones are. The base case will be ⪯nat, which follows directly, since the discrete set N is closed under least upper bound of ω-chains.

We further define a family of relations indexed by type assignments such that if Γ′ extends Γ and ρ ∈ S[[Γ]] and ρ′ ∈ D[[Γ′]]^{o} then

ρ ≺_{Γ} ρ′ iff ∀x ∈ Dom(Γ).ρ(x) ≺_{Γ(x)} ρ′(x)

6.3 Translations of expressions

Now, we can show that the values of expressions are related to the values of the translated expression, which then directly implies the same for programs.

Lemma 5 For any expression e, if PROOF (l) = Γ ⊢ e : τ and Ω_{p}, Φ_{p}, Γ′ ⊢ T [e] : T [τ] where Γ′ extends Γ then for all ρ ∈ S[[Γ]] and ρ′ ∈ D[[Γ′]]^{o}

ρ ≺_{Γ} ρ′ ⇒ S[[e]]ρ ⪯_{τ} D[[T [e]]]^{oϕ}ρ′

Proof of Lemma 5.

The proof is by structural induction on the structure of expressions. The interesting cases are abstraction and application: case e = (fun f x : τ_{1} →τ_{2} = e′)_{l}^{env}: As defined

S[[e]]ρ = up(fix(λF.λX.S[[e]]ρ{f =F }{x=X}))

and

D[[T [e]]]^{oϕ}ρ′ = (λv.up(in_{C_{l}}(v)))^{†} (D[[T_{v} [env]]]^{oϕ}ρ′)

and we know from Lemma 1 that (D[[T_{v} [env]]]^{oϕ}ρ′) = up(ν) for some ν, i.e., D[[T [e]]]^{oϕ}ρ′ = up(in_{C_{l}}(ν)). To show that these are ⪯_{τ_{1}→τ_{2}}-related we use fixed-point induction over the inclusive set

S =^{def} {f |f ≺_{τ_{1}→τ_{2}} in_{C_{l}}(ν)}

to show that fix(λF.λX.S[[e]]ρ{f =F }{x=X}) belongs to it. That is, we must show that the set is closed under the function

F =^{def} λF.λX.S[[e]]ρ{f =F }{x=X}

Let p be any element of S. Then

F(p) ≺_{τ_{1}→τ_{2}} in_{C_{l}}(ν)

since for any a ≺_{τ_{1}} b

F(p)(a) = S[[e′]]ρ{f =p}{x=a}

and from Theorem 1 we know that

ϕ(app_{τ_{1}→τ_{2}})(in_{C_{l}}(ν))b = D[[T [e′]]]^{oϕ}ρ′′

where ρ{f =p}{x=a} ≺_{Γ} ρ′′ necessarily by the requirements on ρ′′ (in combination the two properties, ρ ≺_{Γ} ρ′ and ∀x ∈ Dom(Γ).ρ′′(x) = ρ′(x), implies ρ ≺_{Γ} ρ′′) By induction hypothesis (e′ is smaller than e) the denotation of these expressions are related, i.e. F(p)(a) ⪯_{τ_{2}} app_{τ_{1}→τ_{2}}(in_{C_{l}}(v))(b) which proves that F(p) ≺_{τ_{1}→τ_{2}} in_{C_{l}}(v). Since p ∈ S ⇒ F(p) ∈ S, and S is inclusive, we can conclude that fix(F) ∈ S, i.e.

fix(F) ≺_{τ_{1}→τ_{2}} in_{C_{l}}(v)

We then conclude that

up(fix(F))⪯_{τ_{1}→τ_{2}}up(in_{C_{l}}(v))

as needed. case e = (e_{1} e_{2}): By induction hypothesis we know that

S[[e_{1}]]ρ ⪯_{τ_{1}→τ_{2}} D[[T [e_{1}]]]^{oϕ}ρ′

and

S[[e_{2}]]ρ ⪯_{τ_{1}} D[[T [e_{2}]]]^{oϕ}ρ′

Also, by definition,

S[[(e_{1} e_{2})]]ρ = (λf. (λx.fx)^{†} (S[[e_{2}]]ρ))^{†} (S[[e_{1}]]ρ)

and

\begin{matrix}D[[app_{τ_{1}→τ_{2}} T [e_{1}] T [e_{2}]]]^{oϕ}ρ′ & = \\ (λx_{1}.((λx_{2}.ϕ(app_{τ_{1}→τ_{2}})x_{1}x_{2})^{†} (D[[T [e_{2}]]]^{oϕ}ρ′)))^{†} (D[[T [e_{1}]]]^{oϕ}ρ′) \end{matrix}

If either S[[e_{1}]]ρ or S[[e_{2}]]ρ is ⊥ then so is S[[(e_{1} e_{2})]]ρ (by strictness), and ⊥ is ⪯_{τ_{2}} related to anything.

If neither is ⊥, then their values are up(v_{1}) and up(v_{2}) respectively (for some v_{1} and v_{2}), so S[[(e_{1} e_{2})]]ρ = v_{1}v_{2}. By definition of ⪯_{τ} there exist v′_{1} and v′_{2} such that D[[T [e_{1}]]]^{oϕ}ρ′ = up(v′_{1}) and v_{1} ≺_{τ_{1}→τ_{2}} v′_{1} and D[[T [e_{2}]]]^{oϕ}ρ′ = up(v′_{2}) and v_{2} ≺_{τ_{1}} v′_{2}, meaning that D[[T [(e_{1} e_{2})]]]^{oϕ}ρ′ = ϕ(app_{τ_{1}→τ_{2}})v′_{1}v′_{2}

Now, v_{1} ≺_{τ_{1}→τ_{2}} v′_{1} means that for any a ≺_{τ_{1}} b, especially a = v_{2} and b = v′_{2}, we know that

v_{1}v_{2} ⪯_{τ_{2}} ϕ(app_{τ_{1}→τ_{2}})v′_{1}v′_{2}

but that is exactly the definition of

S[[(e_{1} e_{2})]]ρ ⪯_{τ_{2}} D[[T [(e_{1} e_{2})]]]^{oϕ}ρ′

The entire proof can be seen in Appendix C.

Theorem 2 For any program p,

S[[p]] = up(n) ⇒ D[[T [p]]] = up(n)

Proof of Theorem 2.

S[[Program e]] = S[[e]]{}

and

D[[T [Program e]]] = D[[datatype C_{p} fun F_{p} in T [e]]] = D[[T [e]]]^{oϕ}{}

and these are ⪯nat-related by lemma 5. That is, if S[[p]] = up(n) then D[[T [p]]] = up(m) s.t. n ≺nat m, but being related at type nat is the same as being equal, i.e., n = m.

6.4 Summary and conclusion

We have shown that the translation preserves the meaning of a program if this meaning is up(n) for some n ∈ N, i.e., if the program terminates. Section 7 discusses possible extensions of both the setting and the proof that would make the result stronger or more widely applicable.

7 Applicability and conclusion

The previous sections have presented a proof that for a simple, typed functional language, the naïve defunctionalization algorithm (no analysis or optimization) into a fairly restricted target language preserves the meaning of terminating programs.

This section discusses possible extensions of the translation and the source language that would increase the applicability of the result.

7.1 Extensions of the target language

There is no problem in extending the target language – the translation still only translate into the same subset of it. If we use a more general target language, e.g., Standard ML then we have a different semantics. For the present result to be applicable, it is sufficient to show that the semantics of the target language and of ML agree on the subset that is the image of the translation.

7.2 Extensions of the source language

The source language is chosen to be simple. It could easily be extended with a number of features without significantly increasing the difficulty of the proof.

More Base Types: If the source language had booleans or strings or other base types, and the target language had the same types and operations on them, then they could be translated directly, just like the operations on natural numbers.

Data-types: The source language could have data-types like the ones of the target language, and these could even allow function types as arguments to the constructors. Such data-types would be treated as base types by the translation, i.e., the name of the type and the operations (case) on it would be copied verbatim. The types of the arguments of the constructors would be converted if they were functional, just like the arguments to functions. That is, the constructors are treated as functions. Even allowing reflexive datatypes in the source language would not necessitate changes to the target language, though the semantics of the source language would of course have to take that into account.

Global Declarations: The source language could have global function declarations in the same way as the current target language. By design they can never be used as arguments to functions or be the value of an expression, since they can only occur in a specific position. Therefore they can be translated merely by translating their bodies and types.

Polymorphic Types: The source language is simply typed. If we added let-polymorphism then we could use the same method as Bell, Hook, and Bellegarde [BBH97] to translate a program with polymorphic functions into a monomorphic program.

This translation, however, potentially gives an exponential blow-up in the size of the program, since each function is replicated at all the types it can possibly be used at.

7.3 Extensions of annotations: analysis

The translation as it is now is very naïve. It basically assumes that any function of a type can float to any application matching that type, which is of course not always true. In the case where only one function can reach a given application point, we could inline the body rather than putting it in an apply-function. If this is the only application point that function can reach, this will even be a saving. This is what Shivers calls “superβ” reduction [Shi90]. Generally, if the functions of a type can be split into groups such that no application point can be reached by functions from more than one group, then the data-types can be split into these groups too. This is not a saving in code size as much as in readability of the produced code, since such groups would usually be of functions that are used in similar ways, and it would improve the accuracy of most types of analysis on the translated program.

Also, functions that are never applied could be put in a group of their own, and there would not need to be an application function for these. The current approach is the crudest approximation to such grouping, but, e.g., a control/data flow analysis [Shi91] would make better approximations possible.

Another optimization is only storing the values of the free variables of a function abstraction in the constructed values, just as Reynolds does.

7.4 Conclusion

We have proven that naïve defunctionalization preserves the meaning of terminating programs in a typical simple, typed, functional language. The proof is by logical relations. We expect that the proof can easily be extended to a larger source language, and that the translation can be improved by using global information, e.g., in the form of a control-flow analysis.

Acknowledgments

Thanks to Andrzej Filinski for a timely consultancy and useful comments, and to John Reynolds for encouraging and insightful comments. Also thanks to Olivier Danvy for encouragement and supervision.

Postlude Since finishing the present work, I have become aware of Banerjee, Heintze, and Riecke’s new work which provides a complete correctness proof for defunctionalization using operational semantics [BHR01].

A Proof of type preservation

We prove that for any sub-derivation, Γ⊢e : τ, of the derivation of p that

(Γ⊢e : τ ∧ Γ′ extends Γ) ⇒ Ω_{p}, Φ_{p}, Γ′ ⊢T [Γ⊢e : τ] : T [τ]

Proof. The proof is by structural induction on the derivation of Γ⊢e : τ. Proof by Structural Induction Basis (Axioms): The basic derivations are of the variable and null expres-

sions.

case e = x : If Γ ⊢ x : τ then it must be because Γ(x) = τ. If Γ′ extends Γ then Γ′(x) = T [τ], and as T [x] = x we can also conclude that Ω_{p}, Φ_{p}, Γ′ ⊢T [x] : T [τ] from the corresponding rule for the destination language.

case e = 0 : If Γ ⊢ 0 : τ then τ = nat, and as T [0] = 0 and T [nat] = nat, we can use the corresponding rule in the destination language to conclude Ω_{p}, Φ_{p}, Γ′ ⊢0 : nat

Induction Hypothesis : Assume it holds for expressions structurally smaller than e.

Induction Step : case e = succ(e′) If Γ ⊢ succ(e′) : τ then τ = nat and Γ⊢e′ : nat Since e′ is structurally smaller than e, we know by induction hypothesis that Ω_{p}, Φ_{p}, Γ′ ⊢ T [e′] : nat. By definition T [succ(e′)] = succ(T [e′]) so it suffices that we can conclude Ω_{p}, Φ_{p}, Γ′ ⊢succ(T [e′]) : nat.

case e = ifz(e′, e_{1}, x.e_{2}): If Γ ⊢ e : τ then we know, by inversion, that Γ⊢e′ : nat, Γ⊢e_{1} : τ, and Γ{x =nat}⊢:. By induction hypothesis we can see that Ω_{p}, Φ_{p}, Γ′ ⊢ T [e′] : nat, Ω_{p}, Φ_{p}, Γ′ ⊢ T [e_{1}] : T [τ], and Ω_{p}, Φ_{p}, Γ′{x =nat} ⊢ T [e_{2}] : T [τ] (noticing that if Γ′ extends Γ then Γ′{x=T [τ]} extends Γ{x=τ}). As T [e] = ifz(T [e′] , T [e_{1}] , x.T [e_{2}]) it suffices that we can derive, using the above, that

Ω_{p}, Φ_{p}, Γ′ ⊢ifz(T [e′] , T [e_{1}] , x.T [e_{2}]) : T [τ]

case e = (fun f x : τ_{1} →τ_{2} = e)_{l}^{env}: If Γ ⊢ e_{l} : τ then τ = τ_{1} → τ_{2}. Note that τ_{1} →τ_{2} ∈ typesof(p) then. We can see that for this to be derivable, the premise (Γ ⊢ env) must be derivable too. Now, T [e] = C_{l} T_{v} [env], so we must show that Ω_{p}, Φ_{p}, Γ′ ⊢ T_{v} [env] : Ω_{p}(c_{τ})(C_{l}) to get the result we need. To this end, we show the more general statement

Γ ⊢ env ∧ Γ′ extends Γ ⇒ Ω_{p}, Φ_{p}, Γ′ ⊢T_{v} [env] : V_{Γ}

where Dom(V_{Γ}) = \{\underline{x} |x ∈ Dom(Γ)\} and V_{Γ}(\underline{x}) = T [Γ(x)]. This statement is shown by mathematical induction on the size of Dom(Γ). Proof by Mathematical Induction Basis (n = 0): Assume Γ ⊢ env and Γ′ extends Γ. If |Dom(G)| =

0 then Γ = {}. If {} ⊢ env then env = ⟨⟩, and then T_{v} [env] = ⟨⟩ too. Also V_{Γ} = {}, since Dom(V_{Γ}) = ∅. From all this we can directly derive

Ω_{p}, Φ_{p}, Γ′ ⊢T_{v} [env] : V_{Γ}

Induction Hypothesis : Assume it works for |Dom(Γ)| = k Induction Step (n = k + 1): Assume |Dom(Γ)| = k + 1, Γ ⊢

env, and Γ′ extends Γ.

Now, env must be of the form env′⟨x : τ⟩ for some env′, x, and τ, s.t. Γ \ {x} ⊢ env′ and Γ(x) = τ. Then T [v]env = T_{v} [env′]⟨\underline{x} : x⟩. If Γ′ extends Γ then Γ′ extends Γ \ {x}, so by the mathematical induction hypothesis we know that Ω_{p}, Φ_{p}, Γ′ ⊢T_{v} [env′] : V_{Γ\{x}} As Γ′ extends Γ we know that Γ′(x) = T [Γ(x)], so Ω_{p}, Φ_{p}, Γ′ ⊢ x : T [τ]. From this we can derive

Ω_{p}, Φ_{p}, Γ′ ⊢T_{v} [env] : V_{Γ\\{x\}}\{\underline{x}=T [τ]\}

and since V_{Γ} = V_{Γ\{x}}{x=T [Γ(x)]}, this is what we want. By definition of Ω_{p} we can see that Ω_{p}(c_{τ})(C_{l}) = V_{Γ}, so Ω_{p}, Φ_{p}, Γ′ ⊢ T_{v} [env] : Ω_{p}(c_{τ})(C_{l}). Then we can conclude that

Ω_{p}, Φ_{p}, Γ′ ⊢C_{l} T_{v} [env] : c_{τ}

and as T [τ_{1} →τ_{2}] = c_{τ_{1}→τ_{2}} this shows that

Ω_{p}, Φ_{p}, Γ′ ⊢T [e] : T [τ]

case e = (e_{1} e_{2}): If Γ ⊢ (e_{1} e_{2}) : τ_{2} then there exists τ_{1} s.t. Γ ⊢ e_{1} : τ_{1} →τ_{2} and Γ⊢e_{2} : τ_{1}. Then τ_{1} →τ_{2} ∈ typesof(p) and

τ_{1} →τ_{2} ∈ {τ |∃l.PROOF (l) = D ∧ isappl(D) ∧ typeof(funpart(D)) = τ } In other words, c_{τ_{1}→τ_{2}} ∈ Dom(Ω_{p}) and app_{τ_{1}→τ_{2}} ∈ Dom(Φ_{p}) with Φ_{p}(app_{τ_{1}→τ_{2}}) = (T [τ_{1} →τ_{2}] , T [τ_{1}] , T [τ_{2}]). By induction hypothesis we can derive

Ω_{p}, Φ_{p}, Γ′ ⊢T [e_{1}] : T [τ_{1} →τ_{2}]

and

Ω_{p}, Φ_{p}, Γ′ ⊢T [e_{2}] : T [τ_{1}]

and since T [(e_{1} e_{2})] = app_{τ_{1}→τ_{2}} T [e_{1}] T [e_{2}] we can use the above to conclude

Ω_{p}, Φ_{p}, Γ′ ⊢T [(e_{1} e_{2})] : T [τ_{2}]

B Proof of Lemma 3

Lemma 3 is given as:

If PROOF (l) = Γ ⊢ (fun f x : τ_{1} → τ_{2} = e)^{env} : τ_{1} → τ_{2}, Γ ⊢ env, Γ′ extends Γ, ρ′ ∈ D[[Γ′]]^{o} and ν satisfies that Dom(ν) = \{\underline{x} |x ∈ Dom(Γ)\} and ν(\underline{x}) = ρ′(x) then

D[[F_{v}[env]]]^{oϕ}{ff = g, xx = b}(ν) = ρ′′

implies Dom(ρ′′) = Dom(Γ) ∪ {ff, xx} and ∀x ∈ Dom(Γ).ρ′′(x) = ρ′(x), ρ′′(ff) = g, and ρ′(xx) = b. Proof of Lemma 3. The proof will indirectly be by induction on the structure of env. The actual induction will be in the size of Dom(Γ), which relates to env since we know Γ ⊢ env by inversion.

We prove the following property for any sub-derivation, Γ⊢e : τ, of the derivation of p:

(Γ⊢e : τ ∧ Γ′ extends Γ) ⇒ Ω_{p}, Φ_{p}, Γ′ ⊢T [Γ⊢e : τ] : T [τ]

The proof is by mathematical induction on the size of Γ. Proof by Mathematical Induction

Basis (|Dom(Γ)| = 0): Then Γ = {} and if {} ⊢ env then env = ⟨⟩. Then F_{v}[env] = ⟨⟩, and D[[⟨⟩]]^{oϕ}{ff = g, xx = b}ν = {ff = g, xx = b}, which trivially satisfies the requirements.

Induction Hypothesis : Assume the property holds for |Dom(Γ)| = k.

Induction Step (|Dom(Γ)| = k + 1|): If Γ ≠ {} and Γ ⊢ env, then env = env′⟨x : τ⟩ such that Γ(x) = τ and Γ \ {x} ⊢ env′.

Let ρ′′ = D[[F_{v}[env′]]]^{oϕ}\{ff = g, xx = b\}(ν \ \{\underline{x}\})

Then, by induction hypothesis, Dom(ρ′′) = Dom(Γ \ {x}) ∪ {ff, xx} and x ∈ Dom(Γ \ {x}) ⇒ ρ′′(x) = ρ′(x) (and values at ff and xx are preserved).

Then D[[F_{v}[env′]⟨\underline{x} : x⟩]]^{oϕ}\{ff = g, xx = b\}(ν) = ρ′′\{x=ν(\underline{x})\}

We know that ν(\underline{x}) = ρ′(x), and as x occurs in the program, it is not equal to ff or xx which are chosen fresh, so

D[[F_{v}[env]]]^{oϕ}{ff = g, xx = b}(ν) = ρ′′{x=ρ′(x)}

which satisfies the requirements of the lemma, since Dom(ρ′′{x=ρ′(x)}) = Dom(ρ′′)∪{x} = {ff, xx}∪Dom(Γ \ {x})∪{x} = {ff, xx}∪Dom(Γ) and if y ∈ Dom(Γ) then either x = y and then ρ′′{x=ρ′(x))} (y) = ρ′(y) or x ∈ Dom(Γ \ {x}) and then ρ′′{x=ρ′(x))} (y) = ρ′′(y) = ρ′(y), and ρ′′{x=ρ′(x))} (ff) = ρ′′(ff) = g and likewise xx is mapped to b.

C Proof of Lemma 5

Lemma 5 states that for any expression e, if PROOF (l) = Γ ⊢ e : τ and Ω_{p}, Φ_{p}, Γ′ ⊢ T [e] : T [τ] where Γ′ extends Γ then for all ρ ∈ S[[Γ]] and ρ′ ∈ D[[Γ′]]^{o}

ρ ≺_{Γ} ρ′ ⇒ S[[e]]ρ ⪯_{τ} D[[T [e]]]^{oϕ}ρ′

Proof of Lemma 5.

The proof is by structural induction on the structure of expressions.

case e = x: Then T [e] = x. As ρ ≺_{Γ} ρ′ we know that ρ(x) ≺_{Γ(x)} ρ′(x). Then it follows that

up(ρ(x)) ⪯_{Γ(x)} up(ρ′(x))

which is exactly

S[[e]]ρ ⪯_{Γ(x)} D[[T [e]]]^{oϕ}ρ′

case e = 0: The proof of this case follows directly from S[[e]]ρ = up(0) and D[[T [e]]]^{oϕ}ρ′ = up(0) and up(0) ⪯nat up(0). case e = succ(e′): By induction hypothesis S[[e′]]ρ ⪯nat D[[T [e]]]^{oϕ}ρ′. That

means that either S[[e′]]ρ = ⊥, but then S[[e]]ρ = ⊥ too, and by definition S[[e]]ρ ⪯nat D[[T [e]]]^{oϕ}ρ′.

If S[[e′]]ρ ≠ ⊥ then there must exist some n ∈ N s.t. S[[e′]]ρ = up(n).

If up(n) ⪯nat D[[T [e]]]^{oϕ}ρ′ then D[[T [e]]]^{oϕ}ρ′ = up(n) too.

Then S[[e]]ρ = up(n + 1) and D[[T [e]]]^{oϕ}ρ′ = up(n + 1), which are ⪯nat-related.

case e = ifz(e′, e_{1}, x.e_{2}): By an argument similar to the case for succ(e′), either S[[e′]]ρ = ⊥ and we are finished, or S[[e′]]ρD[[T [e′]]]^{oϕ}ρ′ = up(n).

If n = 0 then S[[e]]ρ = S[[e_{1}]]ρ and D[[T [e]]]^{oϕ}ρ′ = D[[T [e_{1}]]]^{oϕ}ρ′, which are ⪯_{τ} -related by induction hypothesis.

If n > 0 then S[[e]]ρ = S[[e_{2}]]ρ{x =n − 1} and

D[[T [e]]]^{oϕ}ρ′ = D[[T [e_{2}]]]^{oϕ}ρ′{x =n − 1}

which, since ρ{x =n − 1} ≺_{Γ{x=nat}} ρ′{x =n − 1}, are also ⪯_{τ} -related by induction hypothesis.

case e = (fun f x : τ_{1} →τ_{2} = e′)_{l}^{env}: As defined

S[[e]]ρ = up(fix(λF.λX.S[[e]]ρ{f =F }{x=X}))

and

D[[T [e]]]^{oϕ}ρ′ = (λv.up(in_{C_{l}}(v)))^{†} (D[[T_{v} [env]]]^{oϕ}ρ′)

and we know from Lemma 1 that (D[[T_{v} [env]]]^{oϕ}ρ′) = up(ν) for some ν, i.e., D[[T [e]]]^{oϕ}ρ′ = up(in_{C_{l}}(ν)).

To show that these are ⪯_{τ_{1}→τ_{2}}-related we will use fixed-point induction over the inclusive set

S =^{def} {f |f ≺_{τ_{1}→τ_{2}} in_{C_{l}}(ν)}

to show that fix(λF.λX.S[[e]]ρ{f =F }{x=X}) is in it. That is, we must show that the set is closed under the function

F =^{def} λF.λX.S[[e]]ρ{f =F }{x=X}

Let p be any element of S. Then

F(p) ≺_{τ_{1}→τ_{2}} in_{C_{l}}(ν)

as for any a ≺_{τ_{1}} b

F(p)(a) = S[[e′]]ρ{f =p}{x=a}

and from Theorem 1 we know that

ϕ(app_{τ_{1}→τ_{2}})(in_{C_{l}}(ν))b = D[[T [e′]]]^{oϕ}ρ′′

where ρ{f =p}xa ≺_{Γ} ρ′′ necessarily by the requirements on ρ′′ (in combination the two properties, ρ ≺_{Γ} ρ′ and ∀x ∈ Dom(Γ).ρ′′(x) = ρ′(x), implies ρ ≺_{Γ} ρ′′).

By induction hypothesis (e′ is smaller than e) the denotation of these expressions are related, i.e., F(p)(a) ≺_{τ_{2}} app_{τ_{1}→τ_{2}}(in_{C_{l}}(v))(b) which proves that F(p) ≺_{τ_{1}→τ_{2}} in_{C_{l}}(v).

As p ∈ S ⇒ F(p) ∈ S, and S is inclusive, we can conclude that fix(F) ∈ S, i.e.,

fix(F) ≺_{τ_{1}→τ_{2}} in_{C_{l}}(v)

Then we can then conclude that

up(fix(F))⪯_{τ_{1}→τ_{2}}up(in_{C_{l}}(v))

as needed.

case e = (e_{1} e_{2}): By induction hypothesis we know that

S[[e_{1}]]ρ ⪯_{τ_{1}→τ_{2}} D[[T [e_{1}]]]^{oϕ}ρ′

and

S[[e_{2}]]ρ ⪯_{τ_{1}} D[[T [e_{2}]]]^{oϕ}ρ′

Also, by definition,

S[[(e_{1} e_{2})]]ρ = (λf. (λx.fx)^{†} (S[[e_{2}]]ρ))^{†} (S[[e_{1}]]ρ)

and

\begin{matrix}D[[app_{τ_{1}→τ_{2}} T [e_{1}] T [e_{2}]]]^{oϕ}ρ′ & = \\ (λx_{1}.((λx_{2}.ϕ(app_{τ_{1}→τ_{2}})x_{1}x_{2})^{†} (D[[T [e_{2}]]]^{oϕ}ρ′)))^{†} (D[[T [e_{1}]]]^{oϕ}ρ′) \end{matrix}

If either S[[e_{1}]]ρ or S[[e_{2}]]ρ is ⊥ then so is S[[(e_{1} e_{2})]]ρ (by strictness), and ⊥ is ⪯_{τ_{2}} related to anything.

If neither is ⊥, then their values are up(v_{1}) and up(v_{2}) respectively (for some v_{1} and v_{2}), so S[[(e_{1} e_{2})]]ρ = v_{1}v_{2}.

By definition of ⪯_{τ} there exists v′_{1} and v′_{2} s.t. D[[T [e_{1}]]]^{oϕ}ρ′ = up(v′_{1}) and v_{1} ≺_{τ_{1}→τ_{2}} v′_{1} and D[[T [e_{2}]]]^{oϕ}ρ′ = up(v′_{2}) and v_{2} ≺_{τ_{1}} v′_{2}.

From that we infer that D[[T [(e_{1} e_{2})]]]^{oϕ}ρ′ = ϕ(app_{τ_{1}→τ_{2}})v′_{1}v′_{2}

Now, v_{1} ≺_{τ_{1}→τ_{2}} v′_{1} means that for any a ≺_{τ_{1}} b, especially a = v_{2} and b = v′_{2}, we know that

v_{1}v_{2} ⪯_{τ_{2}} ϕ(app_{τ_{1}→τ_{2}})v′_{1}v′_{2}

which is exactly the definition of

S[[(e_{1} e_{2})]]ρ ⪯_{τ_{2}} D[[T [(e_{1} e_{2})]]]^{oϕ}ρ′

References

[AJ89] Andrew W. Appel and Trevor Jim. Continuation-passing, closurepassing style. In Michael J. O’Donnell and Stuart Feldman, editors, Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, pages 293–302, Austin, Texas, January 1989. ACM Press.

[BBH97] Jeffrey M. Bell, Françoise Bellegarde, and James Hook. Typedriven defunctionalization. In Proceedings of the 1997 ACM SIG-PLAN International Conference on Functional Programming, pages 25–37, Amsterdam, The Netherlands, 9–11 June 1997.

[Bel93] Jeffrey M. Bell. An implementation of Reynolds’ defunctionalization method for a modern functional language. Master’s thesis, Oregon Graduate Institute of Science and Technology, November 1993.

[BH94] Jeffrey M. Bell and James Hook. Defunctionalization of typed programs. Technical Report CSE-94-024, Oregon Graduate Institute of Science and Technology, May 1994.

[BHR01] Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Semanticsbased design and correctness of control-flow analysis-based program transformations. Unpublished, March 2001.

[Bon90] Anders Bondorf. Self-Applicable Partial Evaluation (Revised Version). PhD thesis, DIKU, Computer Science Department, University of Copenhagen, December 1990. DIKU Rapport 90/17.

[CJW00] Henry Cejtin, Suresh Jagannathan, and Stephen Weeks. Flowdirected closure conversion for typed languages. In Gert Smolka, editor, Proceedings of the Ninth European Symposium on Programming, number 1782 in Lecture Notes in Computer Science, pages 56–71, Berlin, Germany, March 2000. Springer-Verlag.

[DS00] Olivier Danvy and Ulrik P. Schultz. Lambda-dropping: Transforming recursive equations into programs with block structure. Theoretical Computer Science, 248(1-2):243–287, 2000.

[FH00] Adam Fischbach and John Hannan. Specification and correctness of lambda lifting. In W. Taha, editor, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation (SAIG 2000), number 1924 in Lecture Notes in Computer Science, pages 108–128, Montréal, Canada, September 2000. Springer-Verlag.

[Joh85] Thomas Johnsson. Lambda lifting: Transforming programs to recursive equations. In Jean-Pierre Jouannaud, editor, Functional Programming Languages and Computer Architecture, number 201 in Lecture Notes in Computer Science, pages 190–203, Nancy, France, September 1985. Springer-Verlag.

[Lan64] Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6:308–320, 1964.

[Mit93] John C. Mitchell. Foundations for Programming Languages. The MIT Press, 1993.

[MMH96] Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Guy L. Steele Jr., editor, Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, pages 271–283, St. Petersburg Beach, Florida, January 1996. ACM Press.

[Pey85] Simon L. Peyton Jones. An introduction to fully-lazy supercombinators. In Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet, editors, Combinators and Functional Programming Languages, number 242 in Lecture Notes in Computer Science, pages 176–208, Val d’Ajol, France, 1985. Springer-Verlag.

[Rey98] John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363–397, 1998. Reprinted from the proceedings of the 25th ACM National Conference (1972).

[Shi90] Olin Shivers. Super-β: Copy, constant, and lambda propagation in Scheme, May 1990. Available at

http://www.cc.gatech.edu/fac/Olin.Shivers/citations.html#superbeta.

[Shi91] Olin Shivers. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, May 1991. Technical Report CMU-CS-91-145.

[Str00] Christopher Strachey. Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, 13(1/2):1–49, 2000.

[TO98] Andrew Tolmach and Dino P. Oliva. From ML to Ada: Stronglytyped language interoperability via source translation. Journal of Functional Programming, 8(4):367–412, 1998.

[Win93] Glynn Winskel. The Formal Semantics of Programming Languages. Foundation of Computing Series. The MIT Press, 1993.

Recent BRICS Report Series Publications

RS-00-47 Lasse R. Nielsen. A Denotational Investigation of Defunctionalization. December 2000. 50 pp. Presented at 16th Workshop on the Mathematical Foundations of Programming Semantics, MFPS ’00 (Hoboken, New Jersey, USA, April 13–16, 2000).

RS-00-46 Zhe Yang. Reasoning About Code-Generation in Two-Level Languages. December 2000.

RS-00-45 Ivan B. Damgård and Mads J. Jurik. A Generalisation, a Simplification and some Applications of Paillier’s Probabilistic Public-Key System. December 2000. 18 pp. Appears in Kim, editor, Fourth International Workshop on Practice and Theory in Public Key Cryptography, PKC ’01 Proceedings, LNCS 1992, 2001, pages 119–136. This revised and extended report supersedes the earlier BRICS report RS-00-5.

RS-00-44 Bernd Grobauer and Zhe Yang. The Second Futamura Projection for Type-Directed Partial Evaluation. December 2000. To appear in Higher-Order and Symbolic Computation. This revised and extended report supersedes the earlier BRICS report RS-99-40 which in turn was an extended version of Lawall, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’00 Proceedings, 2000, pages 22–32.

RS-00-43 Claus Brabrand, Anders Møller, Mikkel Ricky Christensen, and Michael I. Schwartzbach. PowerForms: Declarative Client-Side Form Field Validation. December 2000. 21 pp. Appears in World Wide Web Journal, 4(3), 2000.

RS-00-42 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. The <bigwig> Project. December 2000. 25 pp.

RS-00-41 Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. The DSD Schema Language and its Applications. December 2000. 32 pp. Shorter version appears in Heimdahl, editor, 3rd ACM SIGSOFT Workshop on on Formal Methods in Software Practice, FMSP ’00 Proceedings, 2000, pages 101–111.