BRICS RS-00-46 Z. Yang: Reasoning About Code-Generation in Two-Level Languages BRICS

Basic Research in Computer Science

Reasoning About Code-Generation in Two-Level Languages

Zhe Yang BRICS Report Series RS-00-46 ISSN 0909-0878 December 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Zhe Yang.

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/46/

Reasoning about Code Generation in Two-Level Languages

Zhe Yang^{∗}^{†}

Department of Computer Science, New York University

251 Mercer Street, New York, NY 10012, USA

           E-mail: zheyang@cs.nyu.edu

Abstract

We show that two-level languages are not only a good tool for describing code-generation algorithms, but a good tool for reasoning about them as well. Indeed, some general properties of two-level languages capture common proof obligations of code-generation algorithms in the form of two-level programs.

• To prove that the generated code behaves as desired, we use an erasure property, which equationally relates the generated code to an erasure of the original two-level program in the object language, thereby reducing the two-level proof obligation to a simpler one-level obligation.

• To prove that the generated code satisfies certain syntactic constraints, e.g., that it is in some normal form, we use a type-preservation property for a refined type system that enforces these constraints.

In addition, to justify concrete implementations of code-generation algorithms in one-level languages, we use a native embedding of a two-level language into a one-level language.

We present two-level languages with these properties both for a call-by-name object language and for a call-by-value object language with computational effects. Indeed, it is these properties that guide our language design in the call-by-value case. We consider two classes of non-trivial applications: one-pass transformations into continuation-passing style and type-directed partial evaluation for call-by-name and for call-by-value.

Keywords. Two-level languages, erasure, type preservation, native implementation, partial evaluation.

∗This work was carried out at BRICS (Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation).

†Contact address: BRICS, Dept. of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark. Phone: +45 8942 3109. Fax:

+45 8942 3255. Email: zheyang@brics.dk

Contents

1 Introduction 4 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 This work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2 The call-by-name two-level language nPCF^{2} 7 2.1 Syntax and semantics . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Example: the CPS transformation . . . . . . . . . . . . . . . . . 10 2.3 Semantic correctness of the generated code: erasure . . . . . . . 10 2.4 Embedding nPCF^{2} into a one-level language with a term type . . 12 2.5 Example: call-by-name type-directed partial evaluation . . . . . 15 2.6 Syntactic correctness of the generated code: type preservation . . 17

3 The general framework 19

4 The call-by-value two-level language vPCF^{2} 20 4.1 Design considerations . . . . . . . . . . . . . . . . . . . . . . . . 20 4.2 Syntax, semantics, and properties . . . . . . . . . . . . . . . . . . 21 4.3 Example: call-by-value type-directed partial evaluation . . . . . . 24

5 Related work 26 5.1 Two-level formalisms for compiler construction . . . . . . . . . . 27 5.2 Correctness of partial evaluators . . . . . . . . . . . . . . . . . . 28 5.3 Macros and syntactic abstractions . . . . . . . . . . . . . . . . . 29 5.4 Multi-level languages . . . . . . . . . . . . . . . . . . . . . . . . . 30 5.5 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

6 Conclusions 31 6.1 Summary of contributions . . . . . . . . . . . . . . . . . . . . . . 31 6.2 Direction for future work . . . . . . . . . . . . . . . . . . . . . . 33

A Call-by-name CPS translation 34

B Expanded proofs for nPCF^{2} 35 B.1 Type preservation and annotation erasure . . . . . . . . . . . . . 35 B.2 Native embedding . . . . . . . . . . . . . . . . . . . . . . . . . . 35 B.3 Call-by-name type-directed partial evaluation . . . . . . . . . . . 43

C Call-by-value two-level language vPCF^{2}: detailed development 45 C.1 Type preservation . . . . . . . . . . . . . . . . . . . . . . . . . . 46 C.2 Determinacy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 C.3 Annotation erasure . . . . . . . . . . . . . . . . . . . . . . . . . . 54 C.4 Native implementation . . . . . . . . . . . . . . . . . . . . . . . . 55

C.4.1 A more “realistic” language: ⟨v⟩PCF^{2} . . . . . . . . . . . 55 C.4.2 The implementation language: vPCF^{Λ,𝔰𝔱} . . . . . . . . . . 57 C.4.3 Native embedding . . . . . . . . . . . . . . . . . . . . . . 58 C.5 Call-by-value type-directed partial evaluation . . . . . . . . . . . 66

C.5.1 Semantic correctness . . . . . . . . . . . . . . . . . . . . . 66 C.5.2 Syntactic correctness . . . . . . . . . . . . . . . . . . . . . 67

D Notation and symbols 69

List of Figures

1 Base syntactic constituents . . . . . . . . . . . . . . . . . . . . . 7 2 The two-level call-by-name language nPCF^{2} . . . . . . . . . . . . 8 3 The one-level call-by-name language nPCF . . . . . . . . . . . . . 9 4 Call-by-value CPS transformation . . . . . . . . . . . . . . . . . . 11 5 Call-by-name type-directed partial evaluation . . . . . . . . . . . 16 6 Inference rules for terms in long βη-normal form . . . . . . . . . 18 7 nPCF^{2}-terms that generate code in long βη-normal form . . . . . 18 8 The type system of vPCF^{2} . . . . . . . . . . . . . . . . . . . . . . 22 9 The evaluation semantics of vPCF^{2} . . . . . . . . . . . . . . . . . 23 10 Call-by-value type-directed partial evaluation . . . . . . . . . . . 25 11 vPCF^{2}-terms that generate code in λ_{c}-normal form . . . . . . . . 27 12 Inference rules for terms in λ_{c}-normal form . . . . . . . . . . . . 27 13 Call-by-name CPS transformation . . . . . . . . . . . . . . . . . 34 14 One-level call-by-value language vPCF . . . . . . . . . . . . . . . 53 15 Changes of ⟨v⟩PCF^{2} over vPCF^{2} . . . . . . . . . . . . . . . . . . . 56 16 ML implementation of vPCF^{Λ,𝔰𝔱}-primitives . . . . . . . . . . . . . 58 17 The evaluation semantics of vPCF^{Λ,𝔰𝔱} . . . . . . . . . . . . . . . . 59

1 Introduction

1.1 Background

Programs that generate code, such as compilers and program transformers, appear everywhere, but it is often a demanding task to write them, and an even more demanding task to reason about them. The programmer needs to maintain a clear distinction between two languages of different binding times: the static (compile-time, meta) one in which the code-generation program is written, and the dynamic (run-time, object) one in which the generated code is written. To reason about code-generation programs, one always considers, at least informally, invariants about the code generated, e.g., that it type checks.

Two-level languages provide intuitive notations for writing code-generation programs succinctly. They incorporate both static constructs and dynamic constructs for modeling the binding-time separation. Their design usually considers certain semantic aspects of the object languages. For example, the typing safety of a two-level language states not only that (static) evaluation of well-typed programs does not go wrong, but also that the generated code is well-typed in the object language. The semantic benefit, however, often comes at the price of implementation efficiency and its related correctness proof. Semantics vs. implementation: Consider, for example, the pure simply typed λ-calculus as the object language. A possible corresponding two-level language could have the following syntax.

E ::= x | λx.E | E_{1} E_{2} | \underline{λ}x.E | E_{1}\underline{@}E_{2}

Apart from the standard (static) constructs, there are two dynamic constructs for building object-level expressions: \underline{λ}x.E for λ-abstractions, and E_{1}\underline{@}E_{2} for applications. As a first approximation, one can think of the type of object expressions as an algebraic data type

           E = VAR of string | LAM of string * E | APP of E * E

where \underline{λ}x.E is shorthand for LAM("x", E), E_{1}\underline{@}E_{2} is shorthand for APP(E_{1},E_{2}), and an occurrence of \underline{λ}-bound variable x is shorthand for VAR("x"). For instance, the term \underline{λ}x.x is represented by LAM("x", VAR "x").

This representation, by itself, does not treat variable binding in the object language. For instance, we can write a code transformer that performs η-expansion as eta ≜ λf.\underline{λ}x.f\underline{@}x, in the two-level language. Applying this code transformer to object terms with free occurrences of x exposes the problem that evaluation could capture names: For instance, evaluating \underline{λ}x.eta x yields the object term \underline{λ}x.\underline{λ}x.x\underline{@}x, which is wrong and not even typable in the simply typed lambda calculus.

If we are working in a standard, high-level operational semantics that describes evaluation as symbolic computations on the two-level terms, then the solution to the name-capturing problem is simple: Dynamic λ-bound variables, like usual bound variables, should be subject to renaming during a noncapturing substitution E{E′/x} (which is used in the evaluation of static applications). Therefore, in the earlier example, the two-level term \underline{λ}x.(λf.\underline{λ}x.f\underline{@}x)x does not evaluate to \underline{λ}x.\underline{λ}x.x\underline{@}x, but to \underline{λ}x.\underline{λ}y.x\underline{@}y. This precise issue is referred to as “hygienic macro expansion” in Kohlbecker’s work [27, 28].

Indeed, the analogy between the dynamic λ-bound variables and the static λ-bound variables has long been adopted in the traditional, staging view of twolevel languages, which is shaped by the pioneering work of Jones et al. [23, 24, 25]: Serving as an intermediate language of offline partial evaluators, a twolevel language is the staged version of a corresponding one-level language. In this context, in addition to typing safety, another property, which we call annotation erasure, is important for showing the correctness of partial evaluators: The result of two-level evaluation has the same semantics as the unstaged version of the program. Taking up the earlier example again, we can see that the unstaged version of \underline{λ}x.(λf.\underline{λ}x.f\underline{@}x)x, i.e., λx.(λf.λx.f x)x, is β-equivalent to the generated term λx.λy.x y. In the symbolic framework, it is relatively easy to establish annotation erasure, at least in a call-by-name, effect-free setting.

For realistic implementations of two-level languages, capture-avoiding substitution is expensive and undesirable. Indeed, most implementations use some strategy to generate variables such that they do not conflict with each other. Unsurprisingly, it is more difficult to reason about these implementations. In fact, existing work that proved annotation erasure while taking the name generation into account used denotational-semantics formulations and stayed clear of operational semantics [12, 16, 36] (see Section 5.2 for detail). Hand-written two-level programs: In the 1990s, two-level languages started to be used in expressing code-generation algorithms independently of dedicated partial evaluators. Such studies propel a second view of two-level languages: They are simply one-level languages equipped with a code type that represents object-level terms. This code-type view of two-level languages leads to two separate tracks of formal studies, again reflecting the tension between semantics and implementation.

The first track explores the design space of more expressive such languages, while retaining typing safety. Davies and Pfenning characterized multi-level languages in terms of temporal logic [10] and of modal logic [11]. Their work fostered the further development of multi-level languages such as MetaML [37]. In general, this line of work employs high-level operational semantics, in particular capture-free substitution, to facilitate a more conceptual analysis of design choices.

The second track uses the staging intuitions of two-level languages as a guide for finding new, higher-order code-generation algorithms; for the sake of efficiency, the algorithms are then implemented in existing (one-level) functional languages, using algebraic data types to encode the code types and generating names explicitly. As an example, Danvy and Filinski have used an informal two-level language to specify a one-pass CPS transformation that generates no administrative redexes [7], which is an optimization of Plotkin’s original CPS transformation [45]. Similarly, a study of binding-time coercions by twolevel eta-expansion has led Danvy to discover type-directed partial evaluation (TDPE), an efficient way to embed a partial evaluator into a pre-existing evaluator [5]. The proofs of correctness in both applications, as in the case of annotation erasure, stayed clear of two-level languages.

The case of TDPE deserves some interest of its own: Filinski formalized TDPE as a normalization process for terms in an unconventional two-level language, where the binding-time separation does not apply to all program constructs, but to only constants.^{1} Using denotational semantics, he characterized the native implementability of TDPE in a conventional functional language [12, 13]. On the other hand, the intuitive connection between TDPE and conventional two-level languages has not been formalized.

1.2 This work

Our thesis is that (1) we can formally connect the high-level operational semantics and the efficient, substitution-free implementation, and by doing so (2) we can both reason about code-generation algorithms directly in two-level languages and have their efficient and provably correct implementations.

First, to support high-level reasoning, we equip the two-level language, say L^{2}, with a high-level operational semantics, which, in particular, embodies capture-avoiding substitution that takes dynamic λ-bound variables into account. We use the semantics to give simple, syntactic proofs of general properties such as annotation erasure, which reflects the staging view, and type preservation, which reflects the code-type view. In turn, we use these properties to prove semantic correctness of the generated code (i.e., it satisfies certain extensional properties) and syntactic correctness of the generated code (i.e., it satisfies certain intensional, syntactic constraints).

Next, to implement L^{2}-programs efficiently in a conventional one-level language (e.g., ML), we show a native embedding of L^{2} into the implementation language. This native embedding provides efficient substitution-free implementation for the high-level semantics.

Overview of the paper The remainder of this paper fleshes out the preceding ideas with two instances of the framework. The first is a canonical twolevel language nPCF^{2} for a call-by-name object language (call-by-name “PCF of two-level languages”, following Moggi [36]). The second, designed from scratch while taking the aforementioned properties (in particular, annotation erasure and native implementability) into account, is a more practically relevant twolevel language vPCF^{2}: one with an instance of Moggi’s call-by-value computational λ-calculus as its object language.

In Section 2 we present nPCF^{2} together with its related one-level language nPCF, prove its properties, and apply them to the example of CPS transformations and call-by-name TDPE. From this study we abstract out, in Section 3, our general framework, in particular the desired properties and the corresponding proof obligations they support. With this framework in mind, in Section 4 we design vPCF^{2}, prove its properties, and apply them to the example of call-by-value TDPE. We present the related work in Section 5 and conclude this partn Section 6. The detailed proofs and development are given in the appendices.

1Without constants, the call-by-name version of TDPE coincides with Berger and Schwichtenberg’s notion of normalization by evaluation [2].

Notational conventions: Because we consider several different languages, we write L ⊢ J to assert a judgment J in the language L, or we write simply J when L is clear from the context. We write ≡ for strict syntactic equality, and ∼_{α} for equality up to α-conversion. Operations (syntactic translations) defined on types τ, say {|τ|}, are homomorphically extended to apply to contexts: {|x_{1} : τ_{1}, …, x_{n} : τ_{n}|} ≡ x_{1} : {|τ_{1}|}, …, x_{n} : {|τ_{n}|}. A type-preserving translation {|−|} of terms-in-contexts in language L_{1} into ones in language L_{2} is declared in the form L_{1} ⊢ Δ ⊳ E : σ ⟹ L_{2} ⊢ {|Δ|} ⊳ {|E|} : {|σ|} . Meta-variables τ, σ, Γ, and Δ respectively range over two-level types, one-level types, two-level contexts, and one-level contexts.

2 The call-by-name two-level language nPCF^{2}

We present a canonical call-by-name (CBN) two-level language nPCF^{2} (Section 2.1), cast the example of a one-pass CPS transformation as an nPCF^{2} program (Section 2.2), and use an erasure argument to prove its correctness (Section 2.3). Building on a native embedding of nPCF^{2} into a conventional language (Section 2.4), we formulate CBN TDPE in nPCF^{2} and show its semantic correctness as well as its syntactic correctness (Sections 2.5 and 2.6).

2.1 Syntax and semantics

Base types b ∈ 𝔹: bool (boolean type), int (integer type) Literals ℓ: 𝕃(bool) = {tt, ff}, 𝕃(int) = {…, −1, 0, 1, …} Binary operators ⊗: +, − : int × int → int,

=, <: int × int → bool

Figure 1: Base syntactic constituents

For the various languages in this article, we fix a set of base syntactic constituents (Figure 1). Figure 2 shows the type system (Γ ⊳ E : τ) and the evaluation semantics (E ⇓ V) of nPCF^{2} over a signature of typed constants d : σ in the object language. For example, for the conditional construct, we can have a family of object-level constants if_{σ} : bool → σ → σ in Sg.

In addition to the conventional CBN static part,^{2} the language nPCF^{2} has a. The object-level signature Sg is a set of (uninterpreted) typed constants

2We omit product types but it is straightforward to add them and will not affect the results below.

d : σ in the object language.

b. Syntax

Types  τ ::= b | ◯σ | τ_{1} → τ_{2} (two-level types)
σ ::= b | σ_{1} → σ_{2}  (object-code types)
Contexts Γ ::= · | Γ, x : τ
Raw terms E ::= ℓ | x | λx.E | E_{1} E_{2} | fix E | if E_{1} E_{2} E_{3}
| E_{1} ⊗ E_{2} | $_{b}E | \underline{d} | \underline{λ}x.E | E_{1}\underline{@}E_{2}
Typing Judgment  nPCF^{2} ⊢ Γ ⊳ E : τ

(Static)

[lit] \frac{ℓ ∈ 𝕃(b)}{Γ ⊳ ℓ : b} [var] \frac{x: τ ∈ Γ}{Γ ⊳ x : τ}
[lam] \frac{Γ, x: τ_{1} ⊳ E : τ_{2}}{Γ ⊳ λx.E : τ_{1} → τ_{2}} [app] \frac{Γ ⊳ E_{1} : τ_{2} → τ Γ ⊳ E_{2} : τ_{2}}{Γ ⊳ E_{1} E_{2} : τ}
[fix] \frac{Γ ⊳ E : τ → τ}{Γ ⊳ fix E : τ} [if ] \frac{Γ ⊳ E_{1} : bool Γ ⊳ E_{2} : τ Γ ⊳ E_{3} : τ}{Γ ⊳ if E_{1} E_{2} E_{3} : τ}

[bop] \frac{Γ ⊳ E_{1} : b_{1} Γ ⊳ E_{2} : b_{2}}{Γ ⊳ E_{1} ⊗ E_{2} : b} (⊗ : b_{1} × b_{2} → b)

(Dynamic)

[\underline{lift}] \frac{Γ ⊳ E : b}{Γ ⊳ $_{b}E : ◯b} [\underline{cst}] \frac{Sg(d) = σ}{Γ ⊳ \underline{d} : ◯σ}
[\underline{lam}] \frac{Γ, x: ◯σ_{1} ⊳ E : ◯σ_{2}}{Γ ⊳ \underline{λ}x.E : ◯(σ_{1} → σ_{2})} [\underline{app}] \frac{Γ ⊳ E_{1} : ◯(σ_{2} → σ) Γ ⊳ E_{2} : ◯σ_{2}}{Γ ⊳ E_{1}\underline{@}E_{2} : ◯σ}
c. Evaluation Semantics  nPCF^{2} ⊢ E ⇓ V

\begin{aligned}Values & V & ::= & ℓ | λx.E | O \\ & O & ::= & $_{b}ℓ | x | \underline{λ}x.O | O_{1}\underline{@}O_{2} | \underline{d} \end{aligned}

(Static) [lit] \overline{ℓ ⇓ ℓ} [lam] \overline{λx.E ⇓ λx.E} [app] \frac{E_{1} ⇓ λx.E′ E′\{E_{2}/x\} ⇓ V}{E_{1} E_{2} ⇓ V}

[fix] \frac{E(fix E) ⇓ V}{fix E ⇓ V} [if-tt] \frac{E_{1} ⇓ tt E_{2} ⇓ V}{if E_{1} E_{2} E_{3} ⇓ V} [if-ff] \frac{E_{1} ⇓ ff E_{3} ⇓ V}{if E_{1} E_{2} E_{3} ⇓ V}

[⊗] \frac{E_{1} ⇓ V_{1} E_{2} ⇓ V_{2}}{E_{1} ⊗ E_{2} ⇓ V} (V_{1} ⊗ V_{2} = V)

(Dynamic)

[\underline{lift}] \frac{E ⇓ ℓ}{$_{b}E ⇓ $_{b}ℓ} [\underline{var}] \overline{x ⇓ x} [\underline{cst}] \overline{\underline{d} ⇓ \underline{d}}
[\underline{lam}] \frac{E ⇓ O}{\underline{λ}x.E ⇓ \underline{λ}x.O}  [\underline{app}] \frac{E_{1} ⇓ O_{1} E_{2} ⇓ O_{2}}{E_{1}\underline{@}E_{2} ⇓ O_{1}\underline{@}O_{2}}

Figure 2: The two-level call-by-name language nPCF^{2}

Types  σ ::= b | σ_{1} → σ_{2}
Raw terms E ::= ℓ | x | λx.E | E_{1} E_{2} | d
| fix E | if E_{1} E_{2} E_{3} | E_{1} ⊗ E_{2}
Contexts Δ ::= · | Δ, x : σ
Typing Judgment  nPCF ⊢ Δ ⊳ E : σ

The static part of nPCF^{2} plus: [cst] \frac{Sg(d) = σ}{Δ ⊳ d : σ}

Equational Rules  nPCF ⊢ Δ ⊳ E_{1} = E_{2} : σ

The congruence rules, [β], [η], and equations for fix, if , and binary operators ⊗. (omitted)

Figure 3: The one-level call-by-name language nPCF

a family of code types ◯σ, indexed by the types σ of the represented object terms, and their associated constructors, which we call the dynamic constructs. For example, in the base case, dynamic constants \underline{d} : ◯σ represent the corresponding constants d : σ in the object language; static values of base types b, called the literals, can be “lifted” into the code types ◯b with $_{b}, so that the result of static evaluation can appear in the generated code. The dynamic constructs are akin to data constructors of the familiar algebraic types, but with the notable exception that the dynamic λ-abstraction is a binding operator: As mentioned in the introduction, the variables introduced are, like usual bound variables, subject to renaming during a non-capturing substitution E{E′/x} (which is used in the evaluation of static applications).

The evaluation judgment of the form E ⇓ V reads that evaluation of the term E leads to a value V. Evaluation is deterministic modulo α-conversion: If E ⇓ V_{1} and E ⇓ V_{2} then V_{1} ∼_{α} V_{2}. A value can be a usual static value (literal or λ-abstraction) or a code-typed value O. Code-typed values are in 1-1 correspondence with raw λ-terms in the object language by erasing their annotations (erasure will be made precise in Section 2.3).

Because evaluation proceeds under dynamic λ-abstractions, intermediate results produced during the evaluation can contain free dynamic variables [37]. Properties about the evaluation, therefore, are usually stated on terms which are closed on static variables, but not necessarily dynamic variables. For example, a standard property of evaluation in two-level languages is type preservation for statically closed terms.

Theorem 2.1 (Type preservation). If ◯Δ⊳E : τ and E ⇓ V, then ◯Δ⊳V : τ. (◯Δ is the element-wise application of the ◯(−) constructor to the context Δ.)

The proof, as most proofs for this part, can be found in the appendices. As a consequence of this theorem, if ◯Δ⊳E : ◯σ holds, then E ⇓ V implies that V is of the form O.

Figure 3 shows the corresponding one-level language nPCF. The language includes not only the constructs of the object language, but also the static constructs of nPCF^{2}. Though the static constructs will not appear in the generated code, they are needed to specify and prove the semantic correctness of the generated code.

The equational theory of nPCF is standard for CBN languages. We only note that there are no equational rules for the constants d in the object language, thereby leaving them uninterpreted. That is, any interpretation of these constants is a a model of nPCF.

2.2 Example: the CPS transformation

Our first example is the typed versions of two transformations of the pure, simply typed, call-by-value λ-calculus (Figure 4a) into continuation-passing style (CPS).^{3} The typed formulation [32] of Plotkin’s original transformation [45] maps a term E directly into a one-level term {|E|}_{pκ} (Figure 4b), but it generates a lot of administrative redexes—roughly all the bindings named k introduce an extra redex—and to remove these redexes requires a separate pass. Danvy and Filinski’s one-pass CPS transformation instead maps the term into a twolevel program {|E|}_{dfκ} (Figure 4c); evaluating {|E|}_{dfκ} produces the resulting CPS term. The potential administrative redexes are annotated as static, and thus are reduced during the evaluation of {|E|}_{dfκ}. Intuitively, the one-pass transformation is derived by staging the program {|E|}_{pκ} [7].

By the definition of the translation, the two-level program {|E|}_{dfκ} does not use the fixed-point operator. We can prove that the evaluation of such a term always terminates using a standard logical-relation argument (note that, with respect to the termination property, the code type behaves the same as a usual base type like int).^{4} The question is how to ensure that the resulting term has the same behavior as the output of Plotkin’s original transformation, {|E|}_{pκ}. An intuitive argument is that erasing the annotations in {|E|}_{dfκ} produces a term which is βη-equivalent to {|E|}_{pκ}.

2.3 Semantic correctness of the generated code: erasure

The notion of annotation erasure formalizes the intuitive idea of erasing all the binding-time annotations, relates nPCF^{2} to nPCF, and supports the general view of two-level programs as staged version of one-level programs.

Definition 2.2 (Erasure). The (annotation) erasure of a nPCF^{2}-phrase is the nPCF-phrase given as follows. Types: | ◯ σ| = σ, |b| = b, |τ_{1} → τ_{2}| = |τ_{1}| → |τ_{2}|. a. Source syntax: the pure simply typed λ-calculus vΛ

3The call-by-name CPS transformation is studied in Appendix A.

4Less directly, we can also use the embedding translation introduced in Section 2.4 and its associated correctness theorem: The embedding of a term without fixed-point operators does not use the fixed-point operator either, and thus its evaluation terminates in the standard operational semantics.

Types  σ ::= b | σ_{1} → σ_{2}
Raw terms E ::= x | λx.E | E_{1} E_{2}

Typing judgment vΛ ⊢ Δ ⊳ E : σ (omitted)

b. Plotkin’s original transformation:

vΛ ⊢ Δ ⊳ E : σ ⇒ nPCF ⊢ {|Δ|}_{pκ} ⊳ {|E|}_{pκ} : K{|σ|}_{pκ} .

Here, Kσ = (σ → Ans) → Ans for an answer type Ans. Types: {|b|}_{pκ} = b,

{|σ_{1} → σ_{2}|}_{pκ} = {|σ_{1}|}_{pκ} → K{|σ_{2}|}_{pκ}, Terms: {|x|}_{pκ} = λk.k x,

{|λx.E|}_{pκ} = λk.k λx.{|E|}_{pκ},

{|E_{1} E_{2}|}_{pκ} = λk.{|E_{1}|}_{pκ}λr_{1}.{|E_{2}|}_{pκ}λr_{2}.r_{1} r_{2} k.

c. Danvy and Filinski’s one-pass transformation:

vΛ ⊢ Δ ⊳ E : σ ⟹ nPCF^{2} ⊢ ◯{|Δ|}_{pκ} ⊳ {|E|}_{df^{2}κ} : K^{◯}(◯{|σ|}_{pκ}) .

Here, K^{◯}τ = (τ → ◯Ans) → ◯Ans. Terms:

{|x|}_{df^{2}κ} = λk.k x,
\{|λx.E|\}_{df^{2}κ} = λk.k \underline{λ}x.\underline{λ}k′.\{|E|\}_{df^{2}κ}λm.k′\underline{@}m,
\{|E_{1} E_{2}|\}_{df^{2}κ} = λk.\{|E_{1}|\}_{df^{2}κ}λr_{1}.\{|E_{2}|\}_{df^{2}κ}λr_{2}.r_{1}\underline{@}r_{2}\underline{@} \underline{λ}a.k a.

The complete translation

⟹ nPCF^{2} ⊢ ◯{|Δ|}_{pκ} ⊳ {|E|}_{dfκ} : ◯(K{|σ|}_{pκ}) .

\{|E|\}_{dfκ} = \underline{λ}k.\{|E|\}_{df^{2}κ}λm.k\underline{@}m

Figure 4: Call-by-value CPS transformation Terms: |x| = x, |$_{b}E| = E, |\underline{d}| = d, |\underline{λ}x.E| = λx.|E|,

|E_{1}\underline{@}E_{2}| = |E_{1}| |E_{2}|. Erasure of the static term constructs is homomorphic (e.g., |fix E| = fix |E|, |λx.E| = λx.|E|). If nPCF^{2} ⊢ Γ ⊳ E : τ, then nPCF ⊢ |Γ| ⊳ |E| : |τ|. Finally, the object-level term represented by a code-typed value O is its erasure |O|.

The following theorem states that evaluation of two-level terms in nPCF^{2} respects the nPCF-equality under erasure.

Theorem 2.3 (Annotation erasure). If nPCF^{2} ⊢ ◯Δ ⊳ E : τ and nPCF^{2} ⊢ E ⇓ V, then nPCF ⊢ Δ ⊳ |E| = |V | : |τ|.

Proof. By induction on E ⇓ V.

With Theorem 2.3, in order to show certain extensional properties of generated programs, it suffices to show them for the erasure of the original two-level program. As an example, we check the semantic correctness of the one-pass CPS transformation with respect to Plotkin’s transformation.

Proposition 2.4 (Correctness of one-pass CPS). If vΛ ⊢ Δ ⊳ E : σ and nPCF^{2} ⊢ {|E|}_{dfκ} ⇓ O then nPCF ⊢ {|Δ|}_{pκ} ⊳ |O| = {|E|}_{pκ} : K{|σ|}_{pκ}.

Proof. A simple induction on E establishes that nPCF ⊢ {|Δ|}_{pκ} ⊳ |{|E|}_{df^{2}κ}| = {|E|}_{pκ} : K{|σ|}_{pκ}, which has the immediate corollary that nPCF ⊢ {|Δ|}_{pκ} ⊳ |{|E|}_{dfκ}| = {|E|}_{pκ} : K{|σ|}_{pκ}. We then apply Theorem 2.3.

The proof of Proposition 2.4 embodies the basic pattern to establish semantic correctness based on annotation erasure. Although we are only interested in the extensional property of the generated code (which, we shall recall, is the erasure of the code-typed value O resulted from the evaluation), we need to recursively establish extensional properties (e.g., equal to specific one-level terms) for the erasures of all the sub-terms. Most of these sub-terms have higher types and do not generate code by themselves; for these subterms, Theorem 2.3 does not give any readily usable result about the semantics of code generation, since the theorem applies only to terms of code types. But since erasure is compositional, the extension of the sub-terms’ erasures builds up to that of the complete program’s erasure, for which Theorem 2.3 could deliver the result. It is worth noting the similarity between this process and the process of a proof based on a logical-relation argument.

2.4 Embedding nPCF^{2} into a one-level language with a term type

Our goal is also to justify native implementations of code-generation algorithms. To this end, we want to embed the two-level language nPCF^{2} in the one-level language nPCF^{Λ}, which is nPCF with object-level constants removed, and enriched with an inductive type Λ (the equational theory, correspondingly, is enriched with the congruence rules for the data constructors):

Λ = VAR of int | LIT_{b} of b | CST of const
| LAM of int × Λ | APP of Λ × Λ

The type const provides a representation ⟅d⟆ for constants d—usually the string type suffices. Type Λ provides a representation for raw λ-terms whose variable names are of the form v_{i} for all natural numbers i: A value V of type Λ encodes the raw term D(V):

D(VAR(i)) = v_{i}, D(LIT_{b}(ℓ)) = ℓ, D(CST(⟅d⟆)) = d
D(LAM(i, e)) = λv_{i}.D(e), D(APP(e_{1}, e_{2})) = D(e_{1}) D(e_{2})

The language nPCF^{Λ} has a standard, domain-theoretical CBN denotational semantics [34],^{5} which interprets the types as follows:

[[int]] = Z_{⊥}, [[bool]] = B_{⊥}, [[Λ]] = E_{⊥}, [[σ_{1} → σ_{2}]] = [[σ_{1}]] → [[σ_{2}]]

where Z, B and E are respectively the set of integers, the set of booleans, and the set of raw terms (i.e., the inductive set given as the smallest solution to the equation X = Z + Z + B + Cst + Z × X + X × X). Without giving the detailed semantics (which can be found in Appendix B), we remark that (1) the equational theory is sound with respect to the denotational semantics: If nPCF^{Λ} ⊢ Δ ⊳ E_{1} = E_{2} : σ, then [[E_{1}]] = [[E_{2}]], and (2) the evaluation function for closed terms of base types induced from the denotational semantics has (by its computational adequacy with respect to a environment-based (i.e., not substitution-based) call-by-name evaluation semantics where evaluation of the data constructors are strict; the proof of adequacy adapts the standard proof [46]) efficient implementations that do not perform capture-avoiding substitutions.

Definition 2.5 (Embedding of nPCF^{2} into nPCF^{Λ}: {|−|}_{nϵ}).

Types : {|◯σ|}_{nϵ} = int → Λ, {|b|}_{nϵ} = b,
{|τ_{1} → τ_{2}|}_{nϵ} = {|τ_{1}|}_{nϵ} → {|τ_{2}|}_{nϵ}
Terms : \{|$_{b}E|\}_{nϵ} = $_{b}^{nϵ}\{|E|\}_{nϵ}, \{|\underline{d}|\}_{nϵ} = λi.CST(⟅d⟆),
\{|\underline{λ}x.E|\}_{nϵ} = \underline{λ}^{nϵ}λx.\{|E|\}_{nϵ},
\{|E_{1}\underline{@}E_{2}|\}_{nϵ} = \underline{@}^{nϵ}\{|E_{1}|\}_{nϵ}\{|E_{2}|\}_{nϵ}

where we use the following terms:

$_{b}^{nϵ} ≡ λl.λi.LIT_{b}(l),

\underline{λ}^{nϵ} ≡ λf.λi.LAM(i, f(λi′.VAR(i))(i + 1)),
\underline{@}^{nϵ} ≡ λm.λn.λi.APP(mi, ni).

Static constructs are translated homomorphically.

5This is different from a lazy CBN semantics [54], which models Haskell-like languages where higher-order types are observable; there, function spaces are lifted, and the η-rule does not hold.

The three terms used in the embedding translation are nPCF^{Λ}-terms themselves, and are kept as-is in the result of the translation. For instance, \{|f\underline{@}x|\}_{nϵ} is the term \underline{@}^{nϵ}fx ≡ (λm.λn.λi.APP(mi, ni))fx, not the simplified term λi.fi, xi. This is crucial for the validity of the following substitution lemma (Lemma 2.6); moreover, this also models the actual implementation, where the dynamic constructs are provided as combinators in the implementation language nPCF^{Λ}.

The translation uses a de Bruijn-level encoding for generating variable bindings. Furthermore, a dynamic λ-abstraction is translated using a static λabstraction^{6} and thus the two terms have the same binding behavior—a fact reflected in the following substitution lemma.

Lemma 2.6 (Substitution lemma for {|−|}_{nϵ}). If nPCF^{2} ⊢ Γ, x : τ′ ⊳ E : τ and nPCF^{2} ⊢ Γ ⊳ E′ : τ′, then {|E{E′/x}|}_{nϵ} ∼_{α} {|E|}_{nϵ}{{|E′|}_{nϵ}/x}.

We shall establish that the embedding translation preserves the behavior of closed terms of the code type, ◯σ in nPCF^{2} and Λ in nPCF^{Λ}.

Lemma 2.7 (Evaluation preserves translation). If nPCF^{2} ⊢ ◯Δ ⊳ E : τ and nPCF^{2} ⊢ E ⇓ V, then nPCF^{Λ} ⊢ {|◯Δ|}_{nϵ} ⊳ {|E|}_{nϵ} = {|V |}_{nϵ} : {|τ|}_{nϵ}.

Proof. By induction on nPCF^{2} ⊢ E ⇓ V. For E ≡ E_{1} E_{2}, we use Lemma 2.6.

Lemma 2.8 (Translation of code-typed value). If nPCF^{2} ⊢ v_{1}:◯σ_{1}, …, v_{n}: ◯σ_{n} ⊳ O : ◯σ, then there is a value t : Λ such that

• nPCF^{Λ} ⊢ ⊳ ({|O|}_{nϵ}(n + 1)){λi.VAR(1)/v_{1}, …, λi.VAR(n)/v_{n}} = t : Λ,

• nPCF ⊢ v_{1} : σ_{1}, …, v_{n} : σ_{n} ⊳ D(t) : σ, and

• |O| ∼_{α} D(t).

Proof. By induction on the size of term O. For the case O ≡ \underline{λ}x.O_{1}, we use induction hypothesis on the term O_{1}{v_{n+1}/x}.

Lemma 2.9 (Computational adequacy). If nPCF^{2} ⊢ ⊳E : ◯σ, and there is a nPCF^{Λ}-value t : Λ such that [[{|E|}_{nϵ}(1)]] = [[t]], then ∃O.E ⇓ O.

Proof. (Sketch) We use a Kripke logical relation between nPCF^{2}-terms and the standard denotational semantics of nPCF^{Λ}, which relates a term E and the denotation of {|E|}_{nϵ}. The definition of the logical relation at the type ◯σ implies the conclusion.

Theorem 2.10 (Correctness of embedding). If nPCF^{2} ⊢ ⊳E : ◯σ, then the following statements are equivalent.

(a) There is a value O : ◯σ such that nPCF^{2} ⊢ E ⇓ O.

6This is an instance of higher-order abstract syntax [44]. It might come as a surprise that we use both higher-order abstract syntax and de Bruijn levels. In fact, they serve two different but related functions: higher-order abstract syntax makes the object-level capturingbehavior consistent with the meta-level capturing-behavior, and the de Bruijn levels are used to generate the concrete names of the object terms.

(b) There is a value t : Λ such that [[{|E|}_{nϵ}(1)]] = [[t]]. When these statements hold, we further have that

(c) nPCF ⊢ ⊳D(t) : σ and |O| ∼_{α} D(t).

Proof. (a) ⇒ (b),(c): We combine Lemmas 2.7 and 2.8 to show the existence of value t : Λ such that (c) holds and nPCF^{Λ} ⊢ ⊳ {|E|}_{nϵ}(1) = t : Λ, which implies (b) by the soundness of the type theory.

(b) ⇒ (a),(c): By Lemma 2.9, we have (a); by (a) ⇒ (c), we have a value t′ : Λ that satisfies (c). It is easy to show that t ≡ t′.

The embedding provides a native implementation of nPCF^{2} in nPCF^{Λ}: Static constructs are translated to themselves and dynamic constructs can be defined as functions. Explicit substitution in the operational semantics has been simulated using de Bruijn-style name generation through the translation. The code generation in the implementation is one-pass, in that code is only generated once, without further traversal over it, as in a substitution-based implementation. Furthermore, native embeddings exploit the potentially efficient implementation of the one-level language, and they also offer users the flexibility to use extra syntactic constructs in the one-level language—as long as these constructs are semantically equivalent to terms in the proved part.

2.5 Example: call-by-name type-directed partial evaluation

We now turn to a bigger example: Type-Directed Partial Evaluation (TDPE) [6]. Following Filinski’s formalization [12], we describe TDPE as a native normalization process for fully dynamic terms (i.e., terms whose types are built solely from dynamic base types) in the somewhat different two-level language nPCF^{tdpe}. Here, by a native normalization process, we mean an normalization algorithm that is implemented through a native embedding from nPCF^{tdpe} into the implementation language.

The syntax of nPCF^{tdpe} is displayed in Figure 5a. The language nPCF^{tdpe} differs from nPCF^{2} in that only base types are binding-time annotated as static (b) or dynamic (b^{𝔡}, instead of ◯b, for clarity), and the language does not have any dynamic type constructors (like the dynamic function type in nPCF^{2}). Apart from lifted literals, dynamic constants d^{𝔡} are the only form of term construction that introduces dynamic types. Their types, written in the form σ^{𝔡}, are the fully dynamic counterpart of the constants’ type σ in the object language: For example, for the object-level constant eq : int → int → bool, the corresponding dynamic constant is eq^{𝔡} : int^{𝔡} → int^{𝔡} → bool^{𝔡}; consequently, for what we write \underline{eq}\underline{@}($_{int}(1 + 2)) : ◯(int→bool) in nPCF^{2}, we write eq^{𝔡} ($_{int}(1 + 2)) : int^{𝔡}→bool^{𝔡} in nPCF^{tdpe}. Let us stress that there is no binding-time annotation for applications here.

The semantics is described through a standard instantiation^{7} into the onea. The language of CBN TDPE: nPCF^{tdpe}

7An instantiation is a homomorphic syntactic translation. It is specified by a substitution from the base types to types and from constants to terms.

Type  φ ::= b | b^{𝔡} | φ_{1} → φ_{2}
Raw terms E ::= x | ℓ | λx.E | E_{1} E_{2} | fix E_{1}
| if E_{1} E_{2} E_{3} | E_{1} ⊗ E_{2} | $_{b}E | d^{𝔡}

Typing judgment: nPCF^{tdpe} ⊢ Γ ⊳ E : φ Typing rules: same as those of nPCF^{2}, with the dynamic ones replaced by

[cst^{𝔡}] \frac{Sg(d) = σ}{Γ ⊳ d^{𝔡} : σ^{𝔡}} [lift^{𝔡}] \frac{Γ ⊳ E : b}{Γ ⊳ $_{b}E : b^{𝔡}} ,

where σ^{𝔡} ≜ σ{b^{𝔡}/b : b ∈ 𝔹}, i.e., fully dynamic counterpart of the type σ.

b. Standard instantiation (TDPE-erasure)

nPCF^{tdpe} ⊢ Γ ⊳ E : φ ⟹ nPCF ⊢ |Γ| ⊳ |E| : |φ|

|b^{𝔡}| = b; |$_{b}E| = |E|, |d^{𝔡}| = d

c. Extraction functions ↓^{σ} and ↑_{σ}:

We write σ^{◯} for σ{◯b/b : b ∈ 𝔹}.

\{ \begin{matrix}nPCF^{2} ⊢ ⊳↓^{σ} : σ^{◯} → ◯σ \\ ↓^{b} = λx.x \\ ↓^{σ_{1}→σ_{2}} = λf.\underline{λ}x.↓^{σ_{2}}(f (↑_{σ_{1}}x)) \end{matrix}

\{ \begin{matrix}nPCF^{2} ⊢ ⊳↑_{σ} : ◯σ → σ^{◯} \\ ↑_{b} = λx.x \\ ↑_{σ_{1}→σ_{2}} = λe.λx.↑_{σ_{2}}(e\underline{@}(↓^{σ_{1}}x)) \end{matrix}

d. Residualizing instantiation

nPCF^{tdpe} ⊢ Γ ⊳ E : φ ⇒ nPCF^{2} ⊢ {|Γ|}_{ri} ⊳ {|E|}_{ri} : {|φ|}_{ri}

\{|b^{𝔡}|\}_{ri} = ◯b; \{|$_{b}E|\}_{ri} = $_{b}\{|E|\}_{ri}, \{|d^{𝔡} : σ^{𝔡}|\}_{ri} = ↑_{σ}\underline{d}

e. The static normalization function NF is defined on closed terms E of fully

dynamic types σ^{𝔡}:

NF (E : σ^{𝔡}) = ↓^{σ}{|E|}_{ri} : ◯σ

Figure 5: Call-by-name type-directed partial evaluation

level language nPCF (Figure 5b), which amounts to erasing all the annotations; thus we overload the notation of erasure here.

Normalizing a closed nPCF^{tdpe}-term E of fully dynamic type σ^{𝔡} amounts to finding a nPCF-term E′ : σ in long βη-normal form (fully η-expanded terms with no β-redexes; see Section 2.6 for detail) such that nPCF ⊢ ⊳ |E| = E′ : σ. For example, normalizing the term eq^{𝔡} ($_{int}(1 + 2)) should produce the object term λx.eq 3 x. As in Filinski’s treatment, this notion of normalization leaves the dynamic constants uninterpreted—E and E′ need to be the same under all interpretations of constants, since there are no equations for dynamic constants.

The TDPE algorithm, formulated in nPCF^{2}, is shown in Figure 5c-e. It finds the normal form of a nPCF^{tdpe}-term E : σ^{𝔡} by applying a type-indexed extraction function ↓^{σ} (“reification”) on a particular instantiation, called the residualizing instantiation {|E|}_{ri}, of term E in the language nPCF^{2}. Being an instantiation, which maps static constructs to themselves, {|·|}_{ri} makes the TDPE algorithm natively implementable in nPCF^{Λ} through the embedding {|−|}_{nϵ} of Section 2.4. Indeed, the composition of {|−|}_{ri} and the embedding {|−|}_{nϵ} is essentially the same as Filinski’s direct formulation in the one-level language.

We first use the erasure argument to show that the result term of TDPE is semantically correct, i.e., that the term generated by running NF (E) has the same semantics as the standard instantiation |E| of E.

Lemma 2.11. For all types σ, nPCF ⊢ ⊳ |↓^{σ}| = λx.x : σ → σ and nPCF ⊢ ⊳ |↑_{σ}| = λx.x : σ → σ.

The lemma captures the intuition of TDPE as two-level η-expansion, as Danvy stated in his initial presentation of TDPE [5].

Theorem 2.12 (Semantic correctness of TDPE). If nPCF^{tdpe} ⊢ ⊳E : σ^{𝔡} and nPCF^{2} ⊢ NF (E) ⇓ O, then nPCF ⊢ ⊳ |O| = |E| : σ.

Proof. A simple induction on E establishes that nPCF ⊢ ⊳ |{|E|}_{ri}| = |E| : σ, which has the immediate corollary that nPCF ⊢ ⊳ |NF (E)| = |E| : σ. We then apply Theorem 2.3.

2.6 Syntactic correctness of the generated code:

type preservation

Semantic correctness of the generated terms does not give much syntactic guarantee of the generated terms, but using the standard type preservation (Theorem 2.1), we can already infer some intensional properties about the output of TDPE: It does not contain static constructs, and it is typable in nPCF. Furthermore, a quick inspection of the TDPE algorithm reveals that it will never construct a β-redex in the output—since there is no way to pass a dynamic λ-abstraction to the ↑ function. Indeed, an ad-hoc native implementation can be easily refined to express this constraint by changing the term type Λ. To capture that the output is fully η-expanded by typing, however, appears to require dependent types for the term representation.^{8}

8On the other hand, through some extra reasoning on the way the two-level program is written, it is possible to prove that the output is fully η-expanded in such a setting, as done by Danvy and Rhiger recently [9].

To show that the output of TDPE is always in long βη-normal form, i.e., typable according to the rules in Figure 6 (directly taken from Filinski [12]), we can take inspiration from the evaluation of nPCF^{2}-terms of type ◯σ. Type preservation shows that evaluating these terms always yields a value of type ◯σ, which corresponds to a well-typed nPCF-term. Similarly, to show that evaluating NF (E) always yields long βη-terms, we can refine the dynamic typing rules of nPCF^{2}, so that values of code type correspond to terms in long βη-normal form, and then we show that (1) evaluation preserves typing in the new type system; and (2) the term NF (E) is always typable in this new type system.

The two-level language with dynamic typing rules refined according to the rules for long βη-normal forms is shown in Figure 7. Briefly, we attach the sort of the judgment, atomic at or normal form nf, with the code type, and add another code type ◯^{var}(−) for variables in the context. This way, evaluation of static β-redexes will not substitute the wrong sort of syntactic phrase and introduce ill-formed code. The type system is a refinement of the original type system in the sense that all the new dynamic typing rules are derivable in the original system, if we ignore the new “refinement” tags (at, nf, var), and hence any term typable in the new type system is trivially typable in the original one.

\frac{Δ ⊳^{at} E : b}{Δ ⊳^{nf} E : b} \frac{Δ, x : σ_{1} ⊳^{nf} E : σ_{2}}{Δ ⊳^{nf} λx.E : σ_{1} → σ_{2}}  \frac{ℓ ∈ 𝕃(b)}{Δ ⊳^{at} ℓ : b}

\frac{Sg(d) = σ}{Δ ⊳^{at} d : σ} \frac{x: σ ∈ Δ}{Δ ⊳^{at} x : σ} \frac{Δ ⊳^{at} E_{1} : σ_{2} → σ Δ ⊳^{nf} E_{2} : σ_{2}}{Δ ⊳^{at} E_{1} E_{2} : σ}

Figure 6: Inference rules for terms in long βη-normal form

Types τ ::= b | ◯^{var}(σ) | ◯^{nf} (σ) | ◯^{at}(σ)

Typing Judgment  nPCF^{2} ⊢ Γ ▶ E : τ

(Static) same as the static rules for nPCF^{2} ⊢ Γ ⊳ E : τ

(Dynamic)

\frac{Γ ▶ E : ◯^{at}(b)}{Γ ▶ E : ◯^{nf} (b)} \frac{Γ, x : ◯^{var}(σ_{1}) ▶ E : ◯^{nf} (σ_{2})}{Γ ▶ \underline{λ}x.E : ◯^{nf} (σ_{1} → σ_{2})} \frac{Γ ▶ E : b}{Γ ▶ $_{b}E : ◯^{at}(b)}
\frac{Sg(d) = σ}{Γ ▶ \underline{d} : ◯^{at}(σ)} \frac{Γ ▶ E : ◯^{var}(σ)}{Γ ▶ E : ◯^{at}(σ)}

\frac{Γ ▶ E_{1} : ◯^{at}(σ_{2} → σ) Γ ▶ E_{2} : ◯^{nf} (σ_{2})}{Γ ▶ E_{1}\underline{@}E_{2} : ◯^{at}(σ)}

Figure 7: nPCF^{2}-terms that generate code in long βη-normal form

Theorem 2.13 (Refined type preservation). If nPCF^{2} ⊢ ◯^{var}(Δ) ▶ E : τ and nPCF^{2} ⊢ E ⇓ V, then nPCF^{2} ⊢ ◯^{var}(Δ) ▶ V : τ.

Theorem 2.14 (Normal-form code types). If V is an nPCF^{2}-value (Figure 2), then

(1) if nPCF^{2} ⊢ ◯^{var}(Δ) ▶ V : ◯^{at}(σ), then V ≡ O for some O and Δ ⊳^{at} |O| : σ;

(2) if nPCF^{2} ⊢ ◯^{var}(Δ) ▶ V : ◯^{nf} (σ), then V ≡ O for some O and Δ⊳^{nf} |O| : σ.

For our example, we are left to check that the TDPE algorithm can be typed with normal-form types in this calculus.

Lemma 2.15. (1) The extraction functions (Figure 5c) have the following normal-form types (writing σ^{◯nf} for σ{◯^{nf} (b)/b : b ∈ 𝔹}).

▶ ↓^{σ} : σ^{◯nf} → ◯^{nf} (σ), ▶ ↑_{σ} : ◯^{at}(σ) → σ^{◯nf}.

(2) If nPCF^{tdpe} ⊢ Γ ⊳ E : φ, then nPCF^{2} ⊢ {|Γ|}_{ri}^{nf} ▶ {|E|}_{ri} : {|φ|}_{ri}^{nf}, where {|φ|}_{ri}^{nf} = φ{◯^{nf} (b)/b^{𝔡} : b ∈ 𝔹}

Theorem 2.16. If nPCF^{tdpe} ⊢ ⊳E : σ^{𝔡}, then nPCF^{2} ⊢▶ NF (E) : ◯^{nf} (σ).

Corollary 2.17 (Syntactic correctness of TDPE). For nPCF^{tdpe} ⊢ ⊳E : σ^{𝔡}, if nPCF^{2} ⊢ NF (E) ⇓ V, then V ≡ O for some O and nPCF ⊢ Δ ⊳^{nf} |O| : σ.

It appears possible to give a general treatment for refining the dynamic part of the typing judgment, and establish once and for all that such typing judgments come equipped with the refined type preservation, using Plotkin’s notion of binding signature to specify the syntax of the object language [14, 47]. However, since the object language is typed, we need to use a binding signature with dependent types, which could be complicated. We therefore leave this general treatment to a future work.

3 The general framework

In Section 2, we have seen how several properties of the language nPCF^{2} aid in reasoning about code-generation programs and their native implementation in one-level languages. Before moving on, let us identify the general conceptual structure underlying the development.

The aim is to facilitate writing and reasoning about code-generation algorithms through the support of a two-level language over a specific object language. Following the code-type view, we do not insist, from the outset, that the static language and the dynamic language should be the same. But to accommodate the staging view, we collapse the two-level language, say L^{2} (e.g., nPCF^{2}), into a corresponding one-level language, say L (e.g., nPCF), for which a more conventional axiomatic semantics (an equational theory in this article) can be used for reasoning.

Using a high-level operational semantics of L^{2}, we identify and prove properties of L^{2} that support the following two proof obligations:

Syntactic correctness of the generated code, i.e., it satisfies certain intensional, syntactic constraints, specified as typing rules I. We show that the code-type view is fruitful here: to start with, the values of a code type already represent well-typed terms in the object language (which can be modeled as a free binding algebra [14]). By establishing the type preservation theorem for the type system, we further have that code-typed programs generate only well-typed terms.

Similarly, for specific applications that require generated code to be Itypable, we can refine the code type, much like we do with an algebraic data type, by changing the dynamic typing rules according to I, so that code-typed values correspond only to I-typable terms. Subsequently, a refined type preservation theorem further ensures that the code-typed programs typable in the refined type system generate only I-typable terms. The original proof obligation is thus reduced to showing that the original two-level term type-checks in the refined type system. Semantic correctness of the generated code, i.e., it satisfies a certain extensional property P. We use the annotation-erasure property from the staging view. Formulated using the equational theory of the object language L, this property states that if a two-level program E generates a term g, then g and the erasure |E| of E must be equivalent: L ⊢ g = |E|. The original proof obligation is reduced to showing that P holds for |E|. Implementation efficiency of the code-generation program, i.e., it can be efficiently implemented in a conventional one-level language, without actually carrying out symbolic reduction. By establishing a native embedding of L^{2} into a conventional one-level language, we equip the two-level language with an efficient implementation that exploits the potentially optimized implementation of the one-level language.

In Section 2, the call-by-name, effect-free setting of nPCF^{2} has made the proofs of the aforementioned properties relatively easy. It is reasonable to ask how applicable this technique is in other, probably more “realistic” settings. In the next section, we offer some initial positive answer: These properties should be taken into account in the design of new two-level languages to facilitate simple reasoning.

4 The call-by-value two-level language vPCF^{2}

In this section we design a two-level language vPCF^{2} with Moggi’s computational λ-calculus λ_{c} [35] as its object language in such a way that the language has the desired properties that we identified in Section 3 (Section 4.1). These properties are used to give a clean account of call-by-value TDPE (Section 4.3).

4.1 Design considerations

Since we aim at some form of erasure argument, the static part of the language should have a semantics compatible with the object language. We can consider a call-by-value (CBV) language for the static part and term construction for the dynamic part. Can we use the standard evaluation semantics of CBV languages for the static part as well?

The problematic rule is that of static function applications:

\frac{E_{1} ⇓ λx.E′ E_{2} ⇓ V′ E′\{V′/x\} ⇓ V}{E_{1} E_{2} ⇓ V} .

Even though the argument is evaluated to a value V′, its erasure might still be an effectful computation (I/O, side effect, etc.): This happens when the argument E_{2} is of some code type, so that V′ is of the form O. The evaluation rule then becomes unsound with respect to its erasure in the λ_{c}-theory. For example, let E_{2} ≜ \underline{print}\underline{@}($_{int}(2 + 2)), where \underline{print} : ◯(int → bool) is a dynamic constant. Then the code generated by the program (λx.\underline{let} y ⇐ x \underline{in} x) E_{2} after erasure would be let y ⇐ (print 4) in (print 4), which incorrectly duplicates the computation print 4.

This problem can be solved by using the canonical technique of let-insertion in partial evaluation [3]: When V′ is of the form O that represents an effectful computation, a let-binding x = O will be inserted at the enclosing residual binding (λ-abstraction or let-binding) and the variable x will be used in place of O. But since we want vPCF^{2} to be natively implementable in a conventional language, we should not change the evaluation rule for static applications. Our solution is to introduce a new code type v ◯σ whose values correspond to syntactical values, i.e., literals, variables, λ-abstractions, and constants. Only terms of such code type can appear at the argument position of an application. The usual code type, now denoted by e ◯σ to indicate possible computational effects, can be coerced into type v ◯σ with a “trivialization” operator #, which performs let-insertion.

4.2 Syntax, semantics, and properties

The syntax and evaluation semantics of vPCF^{2} are shown in Figure 8 and 9. Again, the languages are parameterized over a signature of typed constants. Due to the differences between call-by-name and call-by-value languages, the type of many important constants might differ: For example, for the conditional construct, we should have object-level constants if_{σ} : bool → (unit → σ) → (unit→σ) (where unit is the standard unit type, which we omit from our language specification for the sake of brevity).

Note that the type θ of a function argument must be “substitution-safe”, i.e., it cannot take the form e ◯σ. The corresponding one-level language vPCF is an instance of the λ_{c}-calculus: Its syntax is the same as nPCF of Figure 3, except for an extra let-construct of the form let x⇐E_{1} in E_{2} with the standard typing rule; its equational theory, an instance of Moggi’s λ_{c}, includes β_{v} and η_{v} (the value-restricted version of the usual β and η rule), and conversion rules that commute let and other constructs.

In the evaluation semantics of vPCF^{2}, the accumulated bindings B are explicit; furthermore, the dynamic environment Δ is necessary, because the gen-

Types  τ ::= θ | e ◯σ
θ ::= b | v ◯σ | θ → τ (substitution-safe types)
σ ::= b | σ_{1} → σ_{2}  (object-code types)
Contexts Γ ::= · | Γ, x : θ
Raw terms E ::= ℓ | x | λx.E | E_{1} E_{2} | fix E | if E_{1} E_{2} E_{3}
| E_{1} ⊗ E_{2} | $_{b}E | \underline{λ}x.E | E_{1}\underline{@}E_{2} | \underline{d}
| \underline{let} x ⇐ E_{1} \underline{in} E_{2} | #E
Typing Judgment  vPCF^{2} ⊢ Γ ⊳ E : τ

(Static) [lit] \frac{ℓ ∈ 𝕃(b)}{Γ ⊳ ℓ : b} [var] \frac{x: θ ∈ Γ}{Γ ⊳ x : θ} [lam] \frac{Γ, x: θ_{1} ⊳ E : τ_{2}}{Γ ⊳ λx.E : θ_{1} → τ_{2}}

[app] \frac{Γ ⊳ E_{1} : θ_{2} → τ Γ ⊳ E_{2} : θ_{2}}{Γ ⊳ E_{1} E_{2} : τ} [fix] \frac{Γ ⊳ E : (θ_{1} → τ_{2}) → (θ_{1} → τ_{2})}{Γ ⊳ fix E : θ_{1} → τ_{2}}
[if ] \frac{Γ ⊳ E_{1} : bool Γ ⊳ E_{2} : τ Γ ⊳ E_{3} : τ}{Γ ⊳ if E_{1} E_{2} E_{3} : τ}

[bop] \frac{Γ ⊳ E_{1} : b_{1} Γ ⊳ E_{2} : b_{2}}{Γ ⊳ E_{1} ⊗ E_{2} : b} (⊗ : b_{1} × b_{2} → b)

(Dynamic)

[\underline{lift}] \frac{Γ ⊳ E : b}{Γ ⊳ $_{b}E : v ◯b} [\underline{cst}] \frac{Sg(d) = σ}{Γ ⊳ \underline{d} : v ◯σ} [\underline{lam}] \frac{Γ, x: v ◯σ_{1} ⊳ E : e ◯σ_{2}}{Γ ⊳ \underline{λ}x.E : v ◯(σ_{1} → σ_{2})}

[\underline{app}] \frac{Γ ⊳ E_{1} : e ◯(σ_{2} → σ) Γ ⊳ E_{2} : e ◯σ_{2}}{Γ ⊳ E_{1}\underline{@}E_{2} : e ◯σ} [\underline{val}] \frac{Γ ⊳ E : v ◯σ}{Γ ⊳ E : e ◯σ}

[\underline{let}] \frac{Γ, x: v ◯σ_{1} ⊳ E_{2} : e ◯σ_{2} Γ ⊳ E_{1} : e ◯σ_{1}}{Γ ⊳ \underline{let} x ⇐ E_{1} \underline{in} E_{2} : e ◯σ_{2}} [\underline{triv}] \frac{Γ ⊳ E : e ◯σ}{Γ ⊳ #E : v ◯σ}

Figure 8: The type system of vPCF^{2}

eration of new names is explicit in the semantics. The only rules that involve explicit manipulation of the bindings are those for the evaluation of dynamic lambda abstraction and dynamic let-expression (both of which initialize a local accumulator in the beginning, and insert the accumulated bindings at the end), and for the trivialization operator # (which inserts a binding to the accumulator).

In the following, by an abuse of notation, B also also stands for its own context part.

Let us examine the desired properties.

Values  V ::= ℓ | λx.E | O
O ::= $_{b}ℓ | x | \underline{λ}x.O | O_{1}\underline{@}O_{2} | \underline{d} | \underline{let} x ⇐ O_{1} \underline{in} O_{2}
Bindings B ::= · | B, x : σ = O
Judgment form  vPCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V

We use the following abbreviations.

\frac{E_{1} ⇓ V_{1} ⋯ E_{n} ⇓ V_{n}}{E ⇓ V}

≡ \frac{Δ ⊳ [B_{1}]E_{1} ⇓ [B_{2}]V_{1} ⋯ Δ ⊳ [B_{n}]E_{n} ⇓ [B_{n+1}]V_{n}}{Δ ⊳ [B_{1}]E ⇓ [B_{n+1}]V}

\underline{let}^{∗} x_{1}:σ_{1}=O_{1}, ⋯, x_{n}:σ_{n}=O_{n} \underline{in} O ≡ \underline{let} x_{1} ⇐ O_{1} \underline{in} (⋯ (\underline{let} x_{n} ⇐ O_{n} \underline{in} O) ⋯)

(Static)

[lit] \overline{ℓ ⇓ ℓ} [lam] \overline{λx.E ⇓ λx.E} [app] \frac{E_{1} ⇓ λx.E′ E_{2} ⇓ V′ E′\{V′/x\} ⇓ V}{E_{1} E_{2} ⇓ V}
[fix] \frac{E ⇓ λx.E′ E′\{fix (λx.E′)/x\} ⇓ V}{fix E ⇓ V} [if-tt] \frac{E_{1} ⇓ tt E_{2} ⇓ V}{if E_{1} E_{2} E_{3} ⇓ V}

[if-ff] \frac{E_{1} ⇓ ff E_{3} ⇓ V}{if E_{1} E_{2} E_{3} ⇓ V} [⊗] \frac{E_{1} ⇓ V_{1} E_{2} ⇓ V_{2}}{E_{1} ⊗ E_{2} ⇓ V} (V_{1} ⊗ V_{2} = V)

(Dynamic)

[\underline{lift}] \frac{E ⇓ ℓ}{$_{b}E ⇓ $_{b}ℓ} [\underline{var}] \overline{x ⇓ x} [\underline{cst}] \overline{\underline{d} ⇓ \underline{d}} [\underline{app}] \frac{E_{1} ⇓ O_{1} E_{2} ⇓ O_{2}}{E_{1}\underline{@}E_{2} ⇓ O_{1}\underline{@}O_{2}}

[\underline{lam}] \frac{Δ, y : σ, B ⊳ [·]E\{y/x\} ⇓ [B′]O y ∉ dom B ∪ dom Δ}{Δ ⊳ [B]\underline{λ}x.E ⇓ [B]\underline{λ}y.\underline{let}^{∗} B′ \underline{in} O}

[\underline{let}] \frac{\begin{matrix}Δ ⊳ [B]E_{1} ⇓ [B′]O_{1} Δ, y : σ, B ⊳ [·]E_{2}\{y/x\} ⇓ [B′′]O_{2} \\ y ∉ dom B′ ∪ dom Δ \end{matrix}}{Δ ⊳ [B]\underline{let} y ⇐ E_{1} \underline{in} E_{2} ⇓ [B′]\underline{let} x ⇐ O_{1} \underline{in} (\underline{let}^{∗} B′′ \underline{in} O_{2})}

[#] \frac{Δ ⊳ [B]E ⇓ [B′]O x ∉ dom B′ ∪ dom Δ}{Δ ⊳ [B]#E ⇓ [B′, x : σ = O]x}

Figure 9: The evaluation semantics of vPCF^{2}

Type Preservation: During the evaluation, the generated bindings B hold context information of the term E. The type preservation, therefore, uses a notion of typable binder-term-in-context, which extends the notion of typable term-in-context. A similar notion to binder-term-in-context has been used by Hatcliff and Danvy to formalize continuation-based partial evaluation [20].

Definition 4.1 (Binder-term-in-context). For a binder B ≡ (x_{1} : σ_{1} = O_{1}, …, x_{n}: σ_{n} = O_{n}), we write Γ ⊳ [B]E : τ if Γ, x_{1} : v ◯σ_{1}, …, x_{i−1} : v ◯σ_{i−1} ⊳ O_{i} : e ◯σ_{i} for all 1 ≤ i ≤ n, and Γ, x_{1} : v ◯σ_{1}, …, x_{n} : v ◯σ_{n} ⊳ E : τ.

Theorem 4.2 (Type preservation). If v ◯Δ⊳[B]E : τ and Δ⊳[B]E ⇓ [B′]V, then v ◯Δ ⊳ [B′]V : τ.

The evaluation of a complete program inserts the bindings accumulated at the top level.

Definition 4.3 (Observation of complete program). For a complete program ⊳E : e ◯σ, we write E ↘ \underline{let}^{∗} B \underline{in} O if ⊳[·]E ⇓ [B]O.

Corollary 4.4 (Type preservation for complete programs). If ⊳E : e ◯σ and E ↘ O, then ⊳O : e ◯σ.

Semantic Correctness: The definition of erasure is straightforward and similar to the CBN case, and is thus omitted; the only important extra case is the erasure of trivialization: |#E| = |E|.

Lemma 4.5 (Annotation erasure). If vPCF^{2} ⊢ v ◯Δ ⊳ [B]E : τ and vPCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V, then vPCF ⊢ Δ ⊳ let^{∗} |B| in |E| = let^{∗} |B′| in |V | : |τ|.

Theorem 4.6 (Annotation erasure for complete programs). If vPCF^{2} ⊢ ⊳E : e ◯σ and vPCF^{2} ⊢ E ↘ O, then vPCF ⊢ ⊳ |E| = |O| : σ.

Native embedding: Without going into detail, we remark that vPCF^{2} has a simple native embedding {|−|}_{vϵ} into vPCF^{Λ,𝔰𝔱}, a CBV language with a term type and a state that consists of two references cells: We use one to hold the bindings and the other to hold a counter for generating fresh variables. As such, the language vPCF^{Λ,𝔰𝔱} is a subset of ML; the language vPCF^{2} can thus be embedded into ML, with dynamic constructs defined as functions.^{9} The correctness proof for the embedding is by directly relating the derivation of the evaluation from a term E, in vPCF^{2}, and the derivation of the evaluation from its translation {|E|}_{vϵ}, in vPCF^{Λ,𝔰𝔱}. The details of the native embedding and the accompanying correctness proof, again, are available in Appendix C.

4.3 Example: call-by-value type-directed partial evaluation

The problem specification of CBV TDPE is similar to the CBN TDPE, where the semantics is given by a translation into vPCF instead of nPCF. We only need to slightly modify the original formulation by inserting the trivialization operators # at appropriate places, so that the two-level program NF (E) type checks in vPCF^{2}. The call-by-value TDPE algorithm thus formulated is shown in Figure 10. We establish its semantic correctness, with respect to vPCF-equality this time, using a simple annotation erasure argument again; the proof is very similar to that of Theorem 2.12. Composing with the native embedding {|−|}_{vϵ}, we have an efficient implementation of this formulation—which is essentially the call-by-value TDPE algorithm that uses state-based let-insertion [49]; see also Filinski’s formal treatment [13].

9The ML source code, with the following example of CBV TDPE, is available at the URL www.brics.dk/~zheyang/programs/vPCF2.

a. The language of CBV TDPE: vPCF^{tdpe} The syntax is the same as that of CBN TDPE, with the addition of a let-construct.

[let] \frac{Δ, x: σ_{1} ⊳ E_{2} : σ_{2} Δ ⊳ E_{1} : σ_{1}}{Δ ⊳ let x ⇐ E_{1} in E_{2} : σ_{2}}

b. Standard instantiation (TDPE-erasure) vPCF^{tdpe} ⊢ Γ ⊳ E : φ ⟹ vPCF ⊢ |Γ| ⊳ |E| : |φ|

|b^{𝔡}| = b; |$_{b}E| = |E|, |d^{𝔡}| = d

c. Extraction functions ↓^{σ} and ↑_{σ}:

We write σ v ◯for the type σ{v ◯b/b : b ∈ 𝔹}.

\{ \begin{matrix}vPCF^{2} ⊢ ⊳↓^{σ} : σ v ◯→ v ◯σ \\ ↓^{b} = λx.x \\ ↓^{σ_{1}→σ_{2}} = λf.\underline{λ}x.↓^{σ_{2}}(f (↑_{σ_{1}}x)) \end{matrix}

\{ \begin{matrix}vPCF^{2} ⊢ ⊳↑_{σ} : v ◯σ → σ v ◯ \\ ↑_{b} = λx.x \\ ↑_{σ_{1}→σ_{2}} = λe.λx.↑_{σ_{2}}#(e\underline{@}(↓^{σ_{1}}x)) \end{matrix}

d. Residualizing instantiation

vPCF^{tdpe} ⊢ Γ ⊳ E : φ ⇒ vPCF^{2} ⊢ {|Γ|}_{ri} ⊳ {|E|}_{ri} : {|φ|}_{ri}

{|b^{𝔡}|}_{ri} = v ◯b; {|$_{b}E|}_{ri} = $_{b}{|E|}_{ri}, {|d^{𝔡} : σ^{𝔡}|}_{ri} = ↑_{σ}d^{𝔡}

e. The static normalization function

NF (⊳E : σ^{𝔡}) = ↓^{σ}{|E|}_{ri} : e ◯σ

Figure 10: Call-by-value type-directed partial evaluation Syntactic correctness: The let-insertions slightly complicate the reasoning about which terms can be generated, since the point where the operator # is used does not lexically relate to the insertion point, where a residual binder is introduced. The refinement of the type system thus should also cover the types of the binders.

Figure 11 shows the refined type system; it is easy to prove that the codetyped values correspond to the object-level terms typable with the rules in Figure 12, which specify the λ_{c}-normal forms [13]. A term in λ_{c}-normal form can be either a normal value (nv) or a normal computation (nc). The other two syntactic categories that we use are atomic values (av; i.e., variables, literals, constants) and binders (bd, which must be an application of an atomic value to a normal value). Intuitively, evaluating terms in the refined type system can only introduce binding expressions whose types are of the form e ◯^{bd}(σ).

Definition 4.7 (Refined binder-term-in-context). For a binder B ≡ (x_{1} : σ_{1} = O_{1}, ⋯, x_{n}: σ_{n} = O_{n}), we write Γ ▶ [B]E : τ if Γ, x_{1} : v ◯^{var}(σ_{1}), …, x_{i−1} : v ◯^{var}(σ_{i−1}) ▶ O_{i} : e ◯^{bd}(σ_{i}) for all 1 ≤ i ≤ n, and Γ, x_{1} : v ◯^{var}(σ_{1}), …, x_{n} : v ◯^{var}(σ_{n}) ▶ E : τ.

Theorem 4.8 (Refined type preservation). If vPCF^{2} ⊢ v ◯^{var}(Δ) ▶ [B]E : τ and vPCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V, then vPCF^{2} ⊢ v ◯^{var}(Δ) ▶ [B′]V : τ.

Corollary 4.9 (Refined type preservation for complete programs). If ▶ E : e ◯^{nc}(σ) and E ↘ O, then ▶ O : e ◯^{nc}(σ).

Theorem 4.10 (Normal-form code types). If V is an vPCF^{2}-value (Figure 8), and vPCF^{2} ⊢ v ◯^{var}(Δ) ▶ V : v ◯^{X}(σ) where X is av, nv, bd, or nc, then V ≡ O for some O and Δ ⊳^{X} |O| : σ.

To show that the CBV TDPE algorithm only generates term in λ_{c}-normal form, it suffices to show its typability with respect to the refined type system.

Lemma 4.11. (1) The extraction functions (Figure 10c) have the following normal-form types (writing σ^{◯nv} for σ{v ◯^{nv}(b)/b : b ∈ 𝔹}.)

▶ ↓^{σ} : σ^{◯nv} → v ◯^{nv}(σ), ▶ ↑_{σ} : v ◯^{av}(σ) → σ^{◯nv}.

(2) If vPCF^{tdpe} ⊢ Γ ⊳ E : φ, then vPCF^{2} ⊢ {|Γ|}_{ri}^{nv} ▶ {|E|}_{ri} : {|φ|}_{ri}^{nv}, where {|φ|}_{ri}^{nv} = φ{v ◯^{nv}(b)/b^{𝔡} : b ∈ 𝔹}.

Theorem 4.12. If vPCF^{tdpe} ⊢ ⊳E : σ^{𝔡}, then vPCF^{2} ⊢▶ NF (E) : v ◯^{nv}(σ).

5 Related work

The introduction (Section 1) of this article has already touched upon some related work, which forms the general background of this work. Here we examine other related work in the rich literature of two-level languages, and put the current work in perspective.

Types τ ::= θ | e ◯^{bd}(σ) | e ◯^{nc}(σ)
θ ::= b | v ◯^{var}(σ) | v ◯^{nv}(σ) | v ◯^{av}(σ) | θ → τ
σ ::= b | σ_{1} → σ_{2}
Typing Judgment  vPCF^{2} ⊢ Γ ▶ E : τ

(Static) same as the static rules for vPCF^{2} ⊢ Γ ⊳ E : τ

(Dynamic)

\frac{Γ ▶ E : v ◯^{var}(σ)}{Γ ▶ E : v ◯^{av}(σ)} \frac{Sg(d) = σ}{Γ ▶ \underline{d} : v ◯^{av}(σ)} \frac{Γ ▶ E : b}{Γ ▶ $_{b}E : v ◯^{av}(b)}
\frac{Γ ▶ E : v ◯^{av}(b)}{Γ ▶ E : v ◯^{nv}(b)} \frac{Γ, x : v ◯^{var}(σ_{1}) ▶ E : e ◯^{nc}(σ_{2})}{Γ ▶ \underline{λ}x.E : v ◯^{nv}(σ_{1} → σ_{2})}
\frac{Γ ▶ E_{1} : v ◯^{av}(σ_{2} → σ) Γ ▶ E_{2} : v ◯^{nv}(σ_{2})}{Γ ▶ E_{1}\underline{@}E_{2} : e ◯^{bd}(σ)} \frac{Γ ▶ E : v ◯^{nv}(σ)}{Γ ▶ E : e ◯^{nc}(σ)}

\frac{Γ, x: v ◯^{var}(σ_{1}) ▶ E_{2} : e ◯^{nc}(σ_{2}) Γ ▶ E_{1} : e ◯^{bd}(σ_{1})}{Γ ▶ \underline{let} x ⇐ E_{1} \underline{in} E_{2} : e ◯^{nc}(σ_{2})}

\frac{Γ ▶ E : e ◯^{bd}(σ)}{Γ ▶ #E : v ◯^{var}(σ)}

Figure 11: vPCF^{2}-terms that generate code in λ_{c}-normal form

\frac{x: σ ∈ Δ}{Δ ⊳^{av} x : σ} \frac{Sg(d) = σ}{Δ ⊳^{av} d : σ} \frac{ℓ ∈ 𝕃(b)}{Δ ⊳^{av} ℓ : b} \frac{Δ ⊳^{av} E : b}{Δ ⊳^{nv} E : b}
\frac{Δ, x : σ_{1} ⊳^{nc} E : σ_{2}}{Δ ⊳^{nv} λx.E : σ_{1} → σ_{2}}  \frac{Δ ⊳^{av} E_{1} : σ_{2} → σ Δ ⊳^{nv} E_{2} : σ_{2}}{Δ ⊳^{bd} E_{1} E_{2} : σ}

\frac{Δ ⊳^{nv} E : σ}{Δ ⊳^{nc} E : σ} \frac{Δ, x : σ_{1} ⊳^{nc} E_{2} : σ_{2} Δ ⊳^{bd} E_{1} : σ_{1}}{Δ ⊳^{nc} let x ⇐ E_{1} in E_{2} : σ_{2}}

Figure 12: Inference rules for terms in λ_{c}-normal form

5.1 Two-level formalisms for compiler construction

While Jones et al. [23, 24, 25] studied two-level languages mainly as metalanguages for expressing partial evaluators and proving them correct, Nielson and Nielson’s work explored various other aspects and applications of two-level languages, such as the following ones.

• A formalism for components of compiler backend, in particular code generation and abstract interpretation, and associated analysis algorithms [40]. These two-level languages embrace a traditional view of code objects—as closed program fragments of function type; name capturing is therefore not an issue in such a setting. By design, these two-level languages are intended as meta-languages for combinator-based code generators, as have been used, e.g., by Wand [51]. In contrast, in meta-languages for partial evaluators and higher-order code generators (such as the examples studied in the present article), it is essential to be able to manipulate open code, i.e., code with free variables: Without this ability, basic transformations such as unfolding (a.k.a. inlining) would rarely be applicable.

• A general framework for the type systems of two-level and multi-level languages, which, on the descriptive side [41], provides a setting for comparing and relating such languages, and, on the prescriptive side [42], offers guidelines for designing new such languages. Their investigation, however, stopped short at the type systems, which are not related to any semantics. Equipping their framework of two-level types systems with some general form of semantics in the spirit of this article, if possible, seems a promising step towards practicality.

To accommodate such a wide range of applications, Nielson and Nielson developed two-level languages syntactically and used parameterized semantics. In contrast, the framework in the present article generalizes the two-level languages of Jones et al., where specific semantic properties such as annotation erasure are essential to the applications. These two lines of studies complement each other.

Beyond the study of two-level languages, two-level formalisms abound in the literature of semantics-based compiler construction. Morris showed how to refine Landin’s semantics [29], viewed as an interpreter, into a compiler [38]. Mosses developed action semantics [39] as an alternative to denotational semantics. An action semantics defines a compositional translation of programs into actions, which are primitives whose semantics can be concisely defined. The translation can be roughly viewed as a two-level program, the dynamic part of which is composed of actions. Lee successfully demonstrated how this idea can be used to construct realistic compilers [31].

5.2 Correctness of partial evaluators

As mentioned in the introduction, annotation erasure has long been used to formalize the correctness of partial evaluation, but existing work on proving annotation erasure while modeling the actual, name-generation-based implementation, used denotational semantics and stayed clear of operational semantics. Along this line, Gomard used a domain-theoretical logical relation to prove annotation erasure [16], but he treated fresh name generation informally. Moggi gave a formal proof, using a functor category semantics to model name generation [36]. Filinski established a similar result as a corollary of the correctness of type-directed partial evaluation, the proof of which, in turn, used an ω-admissible Kripke logical relation in a domain-theoretical semantics [12, Section 5.1]. The present work, in contrast, factors the realistic namegeneration-based implementations through native embeddings from high-level, substitution-based operational semantics. In the high-level operational semantics, simple elementary reasoning often suffices for establishing semantics properties such as annotation erasure, as demonstrated in this article.

Wand proved the correctness of Mogensen’s compact partial evaluator for pure λ-calculus using a logical relation that, at the base type, amounts to an equational formulation of annotation erasure [52, Theorem 2]. Mogensen’s partial evaluator encodes two-level terms as λ-terms, employing higher-order abstract syntax for representing bindings. In this λ-calculus-based formulation, the generation of residual code is modeled using symbolic normalization in the λ-calculus.

Palsberg [43] presented another correctness result for partial evaluation, using a reduction semantics for the two-level λ-calculus. Briefly, his result states that static reduction does not go wrong and generates a static normal form. In the pure λ-calculus, where reductions are confluent, this correctness result implies annotation erasure.

5.3 Macros and syntactic abstractions

The code-type view of two-level languages, in its most rudimentary form, can be traced back to the S-expressions of Lisp [21]. Since S-expressions serve as a representation for both programs and data, they popularized Lisp as an ideal test bed for experimenting program analysis and synthesis. One step further, the quasiquote/unquote mechanism [1] offers a succinct and intuitive notation for code synthesis, one that makes the staging information explicit.

The ability of expressing program manipulation concisely then led to introducing the mechanism of macros in Lisp, which can be informally understood as the compile-time execution of two-level programs. Practice, soon, revealed the problem of name-capturing in the generated code. A proper solution of this problem, namely hygienic macro expansion [27, 28], gained popularity in various Scheme dialects. Having been widely used to build language extensions of Scheme, and even domain-specific languages on top of Scheme, hygienic macros have evolved into syntactic abstractions, now part of the Scheme standard [26].

The studies of two-level languages could pave the way to a future generation of macro languages. The most prominent issue of using macros in Scheme is the problem of debugging. It divides into debugging the syntax of the macroexpanded program (to make it well-formed) and debugging the semantics of macro-expanded programs (to ensure that it runs correctly). These two tasks are complicated by the non-intuitive control flow introduced by the staging. In the light of two-level languages, these two tasks correspond to the syntactic and semantic correctness of generated code. Therefore, if we use two-level languages equipped with the properties studied in this article, then we can address these two tasks:

• for the syntax of macro-expanded programs, type checking in the two-level language provides static debugging; and • for the semantics of macro-expanded programs, we can reduce debugging

the macro (a two-level function) to debugging a normal function—its erasure.

To make two-level languages useful as syntactic-abstraction languages in the style of Scheme, the key extensions seem to be multiple syntactic categories and suitable concrete syntax.

5.4 Multi-level languages

Many possible extensions and variations of two-level languages exist. Going beyond the two-level stratification, we have the natural generalization of multilevel languages. While this generalization, by itself, accommodates few extra practical applications,^{10} its combination with a run construct holds a greater potential. The run construct allows immediate execution of the generated code; therefore, code generation and code execution could happen during a single evaluation phase—this ability, often called run-time code generation, has a growing number of applications in system areas [53].

Davies and Pfenning investigated multi-level languages through the Curry-Howard correspondence with modal logics: λ^{□} , which corresponds to intuitionistic modal logic S4, has the run construct, but it can only manipulates closed code fragment [11]; λ^{◯}, which corresponds to linear temporal logic, can manipulate open code fragment, but does not have the run construct [10]. Naively combining the two languages would result in an unsound type system, due to the execution of program fragments with unbound variables. Moggi et al.’s Idealized MetaML [37] combines λ^{□} and λ^{◯}, by ensuring that the argument to the run-construct be properly closed. Calcagno et al. further studied how side effects can be added to Idealized MetaML while retaining type soundness [4].

While the development of various multi-level languages has been centered on the conflicts of expressiveness and type soundness, other important aspects of multi-level languages, such as efficient code generation and formal reasoning, have not been much explored. Wickline et al. formalized an efficient implementation of λ^{□} in terms of an abstract machine [53]. Taha axiomatized a fragment of Idealized MetaML, which can be used for equational reasoning [50].

For a practical multi-level language, both efficient code generation and formal support of reasoning and debugging would be crucial. It is interesting to see whether the work in this article can be extended to multi-level languages similar to Idealized MetaML in expressiveness, yet equipped with an efficient implementation for code generation, and the erasure property (probably for restricted fragments of the languages).

10It would be, however, interesting to see whether real-life applications like the automake suite in Unix can be described as three-level programs.

5.5 Applications

Two-level languages originate as a formalism of partial evaluation, while erasure property captures the correctness of partial evaluation. Consequently, many standard applications of partial evaluation can be modeled as two-level programs: For example, automatic compilation by specializing an interpreter (which is known as the first Futamura projection [15]) can be achieved with a two-level program—the staged interpreter. The erasure property reduces the correctness of automatic compilation to that of the interpreter.

Some applications are explained and analyzed using the technique of partial evaluation, but not realized through a dedicated partial evaluator. The onepass CPS transformer of Danvy and Filinski is one such example. In this case, it is not a whole program, but the output of a transformation (Plotkin’s CPS translformation), to be binding-time analyzed. The explicit staging of twolevel languages makes them the ideal candidate for describing such algorithms. The technique of Section 2.2, for example, can be used for constructing other one-pass CPS transformations and proving them correct: e.g., call-by-name CPS transformation (see Appendix A) and CPS transformation of programs after strictness analysis [8]. We have also applied this technique to stage other monadic transformations (such as a state-passing-style transformation) into onepass versions that avoid the generation of administrative redexes.

The two-level language vPCF^{2} (and similarly, nPCF^{2}) can also be used to account for the self application of partial evaluators. Under the embedding translation, a vPCF^{2}-program becomes a one-level program in vPCF^{Λ,𝔰𝔱}, which is a language with computational effects, and an instance of the object language vPCF of vPCF^{2}. With some care, it is not difficult to derive a self application based on this idea and prove it correct. In fact, such a process has been developed in detail (though without using the two-level language formalism of this article) for self-applying TDPE to produce efficient generating extensions [17], which is known as the second Futamura projection.

In recent years, type systems have been used to capture, in a syntactic fashion, a wide range of language notions, such as security and mobility. It seems possible to apply the code-type-refinement technique (Sections 2.6 and 4.3) to guarantee that code generated by a certain (possibly third-party) program is typable in such a type system; this could lead to the addition of a code-generating dimension to the area of trusted computing.

6 Conclusions

6.1 Summary of contributions

We have pinpointed several properties of two-level languages that are useful for reasoning about semantic and syntactic properties of code generated by twolevel programs, and for providing them with efficient implementations. More specifically, we have made the following technical contributions.

• We have proved annotation erasure for both languages, using elementary equational reasoning, and the proofs are simpler than those in previous works, which use denotational formulations and logical relations directly (i.e., which do not factor out a native embedding from a two-level language). On the technical side, our proofs take advantage of the fact that the substitution operations used in the operational semantics of the twolevel languages do not capture dynamic bound variables.

• We have constructed native embeddings of both languages into conventional languages and proved them correct, thereby equipping the twolevel semantics with efficient, substitution-free implementations. To our knowledge, such a formal connection between the symbolic semantics and its implementation has not been established for other two-level languages [10, 37, 40].

• We have formulated the one-pass call-by-value CPS transformation, callby-name TDPE, and call-by-value TDPE in these two-level languages. Through the native embeddings, they match Danvy and Filinski’s original work. We also have formulated other one-pass CPS transformations and one-pass transformations into monadic style, for given monads. We use annotation erasure to prove the semantic correctness of these algorithms.

To our knowledge, the present paper is the first to formally use annotation erasure to prove properties of hand-written programs—as opposed to two-level programs used internally by partial evaluation. Previously, annotation erasure has been informally used to motivate and reason about such programs.

The formulation of TDPE as translations from the special two-level languages for TDPE to conventional two-level languages also clarifies the relationship between TDPE and traditional two-level formulations of partial evaluation, which was an open problem. In practice, this formal connection implies that it is sound to use TDPE in a conventional two-level framework for partial evaluation, e.g., to perform higher-order lifting—one of the original motivations of TDPE [5].

• We have proved the syntactic correctness of both call-by-name TDPE and call-by-value TDPE—i.e., that they generate terms in long βη-normal form and terms in λ_{c}-normal form, respectively—by showing type preservation for refined type systems where code-typed values are such terms, and that the corresponding TDPE algorithms are typable in the refined type systems.

The semantic and syntactic correctness results about TDPE match Filinski’s results [12, 13], which have been proved from scratch using denotational methods.

6.2 Direction for future work

It would be interesting to see whether and how far our general framework (Section 3) can apply to other scenarios, e.g., where the object language is a concurrent calculus, equationally specified. As we have seen in Section 5, it seems promising to combine our framework with the related work, and to find applications in it.

For the specific two-level languages developed in this article, immediate future work could include:

• to establish a general theorem for refined type preservation;

• to find and prove other general properties: For example, an adequacy theorem for two-level evaluation with respect to the one-level equational theory could complete our account of TDPE with a completeness result, which says that if there is a normal form, TDPE will terminate and find it; and,

• to further explore the design space of two-level languages by adding an online dimension to them (in the sense of “online partial evaluation”): For example, we could consider adding interpreted object-level constants to the two-level language, which are expressed through equations in the type theory of the one-level language. The extra information makes it possible to generate code of a higher quality.

A Call-by-name CPS translation

Danvy and Filinski [7] also presented a one-pass version for Plotkin’s call-by-name CPS transformation. Figure 13 shows both transformations. The erasure argument applies here, too.

Other one-pass CPS transformations [19] can be similarly described and proven correct.

a. Source syntax: the pure simply typed λ-calculus nΛ Types σ ::= b | σ_{1} → σ_{2} Raw terms E ::= x | λx.E | E_{1} E_{2} Typing judgment nΛ ⊢ Δ ⊳ E : σ (omitted)

b. Plotkin’s original transformation:

nΛ ⊢ Δ ⊳ E : σ ⟹ nPCF ⊢ K{|Δ|}_{pκ} ⊳ {|E|}_{pκ} : K{|σ|}_{pκ} .

Here, Kσ = (σ → Ans) → Ans for an answer type Ans. Types: {|b|}_{pκ} = b,

{|σ_{1} → σ_{2}|}_{pκ} = K{|σ_{1}|}_{pκ} → K{|σ_{2}|}_{pκ} Terms: {|x|}_{pκ} = λk.x k,

{|λx.E|}_{pκ} = λk.k λx.{|E|}_{pκ}

{|E_{1} E_{2}|}_{pκ} = λk.{|E_{1}|}_{pκ}λr_{1}.r_{1} {|E_{2}|}_{pκ} k.

c. Danvy and Filinski’s one-pass transformation: The transformation is specified as a pair of mutually recursive translations.

1. The (higher-order) auxiliary translation

nΛ ⊢ Δ ⊳ E : σ ⟹ nPCF^{2} ⊢ ◯(K{|Δ|}_{pκ}) ⊳ {|E|}_{df^{2}κ} : K^{◯}(◯{|σ|}_{pκ})

Here, K^{◯}σ = (σ → ◯Ans) → ◯Ans.

\{|x|\}_{df^{2}κ} = λk.x\underline{@} \underline{λ}y.k y
\{|λx.E|\}_{df^{2}κ} = λk.k \underline{λ}x.\{|E|\}_{dfκ}
\{|E_{1} E_{2}|\}_{df^{2}κ} = λk.\{|E_{1}|\}_{df^{2}κ} λr_{1}.r_{1}\underline{@}\{|E_{2}|\}_{dfκ}\underline{@} \underline{λ}x.k x

2. The complete translation ⟹ nPCF^{2} ⊢ ◯(K{|Δ|}_{pκ}) ⊳ {|E|}_{dfκ} : ◯(K{|σ|}_{pκ})

{|x|}_{dfκ} = x
\{|λx.E|\}_{dfκ} = \underline{λ}k.k\underline{@} \underline{λ}x.\{|E|\}_{dfκ}
\{|E_{1} E_{2}|\}_{dfκ} = \underline{λ}k.\{|E_{1}|\}_{df^{2}κ} λr_{1}.r_{1}\underline{@}\{|E_{2}|\}_{dfκ}\underline{@}k

Figure 13: Call-by-name CPS transformation

B Expanded proofs for nPCF^{2}

B.1 Type preservation and annotation erasure

Theorem 2.1 (Type preservation). If ◯Δ⊳E : τ and E ⇓ V, then ◯Δ⊳V : τ.

Proof. Induction on E ⇓ V. For the only non-straightforward case, where E ≡ E_{1} E_{2}, we use a Substitution Lemma of the typing rules: if Γ, x : τ_{1} ⊳ E : τ_{2} and Γ ⊳ E′ : τ_{1}, then Γ ⊳ E{E′/x} : τ_{2}.

Theorem 2.3 (Annotation erasure). If nPCF^{2} ⊢ ◯Δ ⊳ E : τ and nPCF^{2} ⊢ E ⇓ V, then nPCF ⊢ Δ ⊳ |E| = |V | : |τ|.

Its proof uses the following Substitution Lemma for erasure.

Lemma B.1 (Substitution lemma for | − |). If nPCF^{2} ⊢ Γ, x : τ′ ⊳ E : τ and nPCF^{2} ⊢ Γ ⊳ E′ : τ′, then |E{E′/x}| ∼_{α} |E|{|E′|/x}.

Proof. By a simple induction on the size of term E.

Proof of Theorem 2.3. By rule induction on E ⇓ V. We show a few cases.

Case [app]: \begin{aligned}& |E_{1} E_{2}| ≡ |E_{1}| |E_{2}| \\ =^{i.h.} & (λx.|E′|) |E_{2}| = |E′|\{|E_{2}|/x\} \\ ∼_{α} & |E′\{E_{2}/x\}| & (Lemma B.1) \\ =^{i.h.} & |V |. \end{aligned}

Case [fix]: |fix E| ≡ fix |E| = |E|(fix |E|) ≡ |E(fix E)| =^{i.h.} |V |.

Case [\underline{lam}]: |\underline{λ}x.E| ≡ λx.|E| =^{i.h.} λx.|O| ≡ |\underline{λ}x.O|.

B.2 Native embedding

We first present the standard denotational semantics of the language nPCF^{Λ}.

Definition B.2. (Denotational semantics of nPCF^{Λ}) Let Z and B denote the sets (discrete cpos) of integers and of booleans, respectively. Let Cst denote the set used to represent constants. Let E be the inductive set given as the smallest solution to the equation X = Z + Z + B + Cst + Z × X + X × X, with injection functions inVar, inLit_{int}, inLit_{bool}, inCst, inLam, and inApp into the components of the sum.

The standard domain-theoretical semantics maps nPCF^{Λ}-types to domains as follows.

[[int]] = Z_{⊥}, [[bool]] = B_{⊥}, [[Λ]] = E_{⊥}, [[σ_{1} → σ_{2}]] = [[σ_{1}]] → [[σ_{2}]]

This mapping extends to provide the meaning of contexts Δ by taking the product: [[Δ]] = ∏_{x∈dom Δ} [[Δ(x)]]. The meaning of a term-in-context Δ ⊳ E : σ is a continuous function [[E]] : [[Δ]] → [[σ]]:

[[ℓ]]ρ = val^{⊥} ℓ
[[x]]ρ = ρx
[[λx.E]]ρ = λy.[[E]]ρ[x ↦ y]
[[E_{1} E_{2}]]ρ = [[E_{1}]]ρ ([[E_{2}]]ρ)
[[fix E]]ρ = ⨆_{i≥0} ([[E]]ρ)^{i}(⊥)
[[if E_{1} E_{2} E_{3}]]ρ = let^{⊥} b ⇐ [[E_{1}]]ρ in if b ([[E_{2}]]ρ) ([[E_{3}]]ρ)
[[E_{1} ⊗ E_{2}]]ρ = let^{⊥} m ⇐ [[E_{1}]]ρ in let^{⊥} n ⇐ [[E_{2}]]ρ in val^{⊥} (m ⊗ n)
[[VAR(E)]]ρ = let^{⊥} i ⇐ [[E]]ρ in val^{⊥} (inVar(i))
[[LIT_{b}(E)]]ρ = let^{⊥} l ⇐ [[E]]ρ in val^{⊥} (inLit_{b}(l))
[[CST(E)]]ρ = let^{⊥} c ⇐ [[E]]ρ in val^{⊥} (inCst(c))
[[LAM(E_{1}, E_{2})]]ρ = let^{⊥} x ⇐ [[E_{1}]]ρ in let^{⊥} e ⇐ [[E_{2}]]ρ in val^{⊥} (inLam(x, e))
[[VAR(E_{1}, E_{2})]]ρ = let^{⊥} e_{1} ⇐ [[E_{1}]]ρ in let^{⊥} e_{2} ⇐ [[E_{2}]]ρ in val^{⊥} (inApp(e_{1}, e_{2}))

It is straightforward to show that the equational theory is sound with respect to this denotational semantics.

Theorem B.3 (Soundness of the equational theory). If nPCF^{Λ} ⊢ Δ⊳E_{1} = E_{2} : σ, then [[E_{1}]] = [[E_{2}]].

We now prove the correctness of the embedding translation, i.e., that evaluating complete programs of code type in nPCF^{2} is precisely simulated by evaluating their embedding translations in nPCF^{Λ}. We proceed in two steps. First, we show that if nPCF^{2}-evaluation of a term E generates certain object term as the result, then [[{|E|}_{nϵ}(1)]] should give the encoding of this term, modulo αconversion. Second, we show that conversely, if [[{|E|}_{nϵ}(1)]] ≠ ⊥, then evaluation of term E terminates.

Lemma 2.6 (Substitution lemma for {|−|}_{nϵ}). If nPCF^{2} ⊢ Γ, x : τ′ ⊳ E : τ and nPCF^{2} ⊢ Γ ⊳ E′ : τ′, then {|E{E′/x}|}_{nϵ} ∼_{α} {|E|}_{nϵ}{{|E′|}_{nϵ}/x}.

Proof. By induction on the size of term E. The most non-trivial case is the following one.

Case E ≡ \underline{λ}y.E_{1}: There are two sub-cases: Either x ≡ y or x ≢ y. If x ≡ y, then

\{|(\underline{λ}y.E_{1})\{E′/y\}|\}_{nϵ} ≡ \{|(\underline{λ}y.E_{1})|\}_{nϵ} ≡ \underline{λ}^{nϵ}(λy.\{|E_{1}|\}_{nϵ})
≡ (\underline{λ}^{nϵ}(λy.\{|E_{1}|\}_{nϵ}))\{\{|E′|\}_{nϵ}/y\} ≡ \{|(\underline{λ}y.E_{1})|\}_{nϵ}\{\{|E′|\}_{nϵ}/y\}

If x ≢ y, then let z be a variable such that z ∉ fv(E′) ∪ {x}

\{|(\underline{λ}y.E_{1})\{E′/x\}|\}_{nϵ}
∼_{α} \{|\underline{λ}z.E_{1}\{z/y\}\{E′/x\}|\}_{nϵ}
≡ \underline{λ}^{nϵ}(λz.\{|E_{1}\{z/y\}\{E′/x\}|\}_{nϵ})
∼_{α} \underline{λ}^{nϵ}(λz.(\{|E_{1}\{z/y\}|\}_{nϵ}\{E′/x\}))  (ind. hyp. on E_{1}\{z/y\})
≡ (\underline{λ}^{nϵ}(λz.\{|E_{1}\{z/y\}|\}_{nϵ}))\{\{|E′|\}_{nϵ}/x\} (z ∉ fv(E′) = fv(\{|E′|\}_{nϵ}))
∼_{α} \{|(\underline{λ}y.E_{1})|\}_{nϵ}\{\{|E′|\}_{nϵ}/x\}

Lemma 2.7 (Evaluation preserves translation). If nPCF^{2} ⊢ ◯Δ ⊳ E : τ and nPCF^{2} ⊢ E ⇓ V, then nPCF^{Λ} ⊢ {|◯Δ|}_{nϵ} ⊳ {|E|}_{nϵ} = {|V |}_{nϵ} : {|τ|}_{nϵ}.

Proof. By rule induction on nPCF^{2} ⊢ E ⇓ V. We show a few cases.

Case [app]: {|E_{1} E_{2}|}_{nϵ} ≡ {|E_{1}|}_{nϵ} {|E_{2}|}_{nϵ} =^{i.h.} {|λx.E′|}_{nϵ}{|E_{2}|}_{nϵ} ≡(λx.{|E′|}_{nϵ}) {|E_{2}|}_{nϵ} = {|E′|}_{nϵ}{{|E_{2}|}_{nϵ}/x}  (β) ∼_{α} {|E′{E_{2}/x}|}_{nϵ}  (Lemma 2.6) =^{i.h.} {|V |}_{nϵ}.

Case [fix]: {|fix E|}_{nϵ} ≡ fix {|E|}_{nϵ} = {|E|}_{nϵ} (fix {|E|}_{nϵ}) (equational rule for fix ) ≡ {|E (fix E)|}_{nϵ} =^{i.h.} {|V |}_{nϵ}.

The term-building evaluation of the dynamic parts preserves translation, because the translation of the dynamic constructs is compositional.

Case [\underline{lam}]: \{|\underline{λ}x.E|\}_{nϵ} ≡ \underline{λ}^{nϵ}(λx.\{|E|\}_{nϵ}) =^{i.h.} \underline{λ}^{nϵ}(λx.\{|O|\}_{nϵ}) ≡ \{|\underline{λ}x.O|\}_{nϵ}.

Lemma 2.8 (Translation of code-typed value). If nPCF^{2} ⊢ v_{1}:◯σ_{1}, …, v_{n}: ◯σ_{n} ⊳ O : ◯σ, then there is a value t : Λ such that

• nPCF^{Λ} ⊢ ⊳ ({|O|}_{nϵ}(n + 1)){λi.VAR(1)/v_{1}, …, λi.VAR(n)/v_{n}} = t : Λ,

• nPCF ⊢ v_{1} : σ_{1}, …, v_{n} : σ_{n} ⊳ D(t) : σ, and

• |O| ∼_{α} D(t).

Proof. By induction on the size of term O. We write θ_{n} for the substitution {λi.VAR(1)/v_{1}, …, λi.VAR(n)/v_{n}}.

Case O ≡ $_{b}ℓ: lhs ≡ (($_{b}^{nϵ}ℓ)(n+1)){θ_{n}} = LIT_{b}(ℓ). We have that D(LIT_{b}(ℓ)) ≡ ℓ ≡ |O|.

Case O ≡ v_{i}: lhs ≡ (v_{i}(n + 1)){θ_{n}} = VAR(i). We have that D(VAR(i)) ≡ v_{i} ≡ |O|.

Case O ≡ \underline{λ}x.O_{1}:

lhs ≡ (\underline{λ}^{nϵ}(λx.\{|O_{1}|\}_{nϵ})(n + 1))\{θ_{n}\}
= LAM(n + 1, ({|O_{1}|}_{nϵ}{λi′.VAR(n + 1)/x}((n + 1) + 1))){θ_{n}}
= LAM(n + 1, ({|O_{1}{v_{n+1}/x}|}_{nϵ}((n + 1) + 1)){θ; λi′.VAR(n + 1)/v_{n+1}})
=^{i.h.} LAM(n + 1, t_{1})

where D(t_{1}) ∼_{α} |O_{1}|{v_{n+1}/x}. Here we use the induction hypothesis on term O{v_{n+1}/x}, which is typed as v_{1} : ◯σ_{1}, ⋯, v_{n+1} : ◯σ_{n+1}⊳O{v_{n+1}/x} : ◯σ_{n+2}, where σ = σ_{n+1} → σ_{n+2}. We have that D(LAM(n + 1, t_{1})) ≡ λv_{n+1}.D(t_{1}) ∼_{α} λx.|O_{1}| ≡ |O|.

Case O ≡ O_{1}\underline{@}O_{2}:

lhs ≡ (\underline{@}^{nϵ}\{|O_{1}|\}_{nϵ}\{|O_{2}|\}_{nϵ}(n + 1))\{θ_{n}\}
= APP({|O_{1}|}_{nϵ}n + 1{θ_{n}}){|O_{2}|}_{nϵ}n + 1{θ_{n}}
=^{i.h.} APP(t_{1}, t_{2})

where D(t_{1}) ∼_{α} |O_{1}| and D(t_{2}) ∼_{α} |O_{2}|. We have that D(APP(t_{1}, t_{2})) = D(t_{1}) D(t_{2}) ∼_{α} |O_{1}| |O_{2}| ∼_{α} |O|

Case O ≡ \underline{d}: lhs ≡ ((λi.CST(⟅d⟆))(n + 1))\{θ_{n}\} = ⟅d⟆.

Lemma 2.9 (Computational adequacy). If nPCF^{2} ⊢ ⊳E : ◯σ, and there is a nPCF^{Λ}-value t : Λ such that [[{|E|}_{nϵ}(1)]] = [[t]], then ∃O.E ⇓ O.

In the following, we write E ⇓ for ∃V.E ⇓ V; that is, evaluation of E terminates.

We prove Lemma 2.9 using a Kripke logical relation between the denotation of translated terms and the original two-level terms.

Definition B.4 (Logical relation, ≺_{τ}^{Δ}). For an object-type typing context Δ, we define, by induction on an nPCF^{2}-type τ, a family of relations v ≺_{τ}^{Δ} E, where v ∈ [[{|τ|}_{nϵ}]], and E ∈ Expr_{τ}^{Δ} = {E | nPCF^{2} ⊢ ◯Δ ⊳ E : τ}, by

v ≺_{b}^{Δ} E ⟺ v = ⊥ ∨ ∃ℓ.(v = val^{⊥} ℓ ∧ E ⇓ ℓ)
f ≺_{◯σ}^{Δ} E ⟺ ∀n.(f(val^{⊥} n) = ⊥ ∨ E ⇓)
f ≺_{τ_{1}→τ_{2}}^{Δ} E ⟺ ∀a ∈ [[{|τ_{1}|}_{nϵ}]], Δ′ ≥ Δ, E′ ∈ Expr_{τ_{1}}^{Δ′}.
(a ≺_{τ_{1}}^{Δ′} E′ ⇒ f(a) ≺_{τ_{2}}^{Δ′} EE′)

Note that the logical relation at the code types ◯σ only requires the termination of the evaluation of E. This requirement is enough for the proof, because programs cannot perform intensional analysis on values of types ◯σ. In fact, it is essential for the correctness of the simple native embedding here that intensional analysis on code is absent from the language.

Before proceeding to prove a “Basic Lemma” for the logical relation, we first establish some of its properties.

“Weakening” holds for ≺_{τ}^{−} (Lemma B.5) Note that the object-type context Δ is used in the definition of the logical relation only to ensure that the term E is well-typed. Naturally we expect a weakening property; and indeed this property is used in several cases of the proof. It is this property that “forces” us to use a Kripke-style logical relation.

≺_{τ}^{Δ} is ω-admissible (Lemma B.6) This lemma is necessary for the proof in the case of a fixed-point operator.

Kleene equivalence respects ≺_{τ}^{Δ} (Lemma B.7) At a few places, the operational semantics and the denotational semantics clash in a technical sense. The call-by-name denotational semantics, for example, does not use a lifted function space; the bottom element at type σ_{1} → σ_{2} is not distinguished from a function value whose image (of type σ_{2}) is constantly bottom. In the operational semantics, the function needs to be evaluated to a value before the substitution. At base types, however, the two semantics agree.

The denotational semantics forces us to take a standard call-by-name form of logical relation at the function type in the definition. Another problem then appears: since we do not evaluate the expression form in the operational semantics, what we can infer from the induction hypothesis does not directly give the conclusion. In particular, for the case λx.E, using the induction hypothesis, we can relate the denotation to the expression E{θ; E′/x}, but instead we need to relate it to the expression ((λx.E){θ})E′. The two expressions evaluate to the same value in the operational semantics, i.e., they are Kleene-equivalent. Therefore, we need to show that the logical relation can be transferred between Kleene-equivalent terms.^{11}

Lemma B.5 (Weakening of ≺_{τ}^{−}). If Δ ≤ Δ′ and v ≺_{τ}^{Δ} E, then v ≺_{τ}^{Δ′} E.

Proof. By a case analysis on type τ.

Case τ = b or τ = ◯σ: Use the weakening property of the nPCF^{2} typing rules: Expr_{τ}^{Δ} ⊆ Expr_{τ}^{Δ′}.

Case τ = τ_{1} →τ_{2}: Let f ≺_{τ_{1}→τ_{2}}^{Δ} E. First, we have that E ∈ Expr_{τ}^{Δ} ⊆ Expr_{τ}^{Δ′}. Second, let a, Δ′′ ≥ Δ′ (which implies Δ′′ ≥ Δ), and E′ ∈ Expr_{τ_{1}}^{Δ′′} be such that a ≺_{τ_{1}}^{Δ′′} E′. Then, by the definition of ≺_{τ_{1}→τ_{2}}^{Δ}, we have that f(a) ≺_{τ_{2}}^{Δ′′} EE′. This shows that f ≺_{τ_{1}→τ_{2}}^{Δ′} E by definition.

11In the literature, this mismatch problem is resolved by using a different formulation of the logical relation, usually called computability: the relation at higher types is defined by means of full applications (e.g., Plotkin’s proof of adequacy [46] and Gunter’s proof [18, Section 4.3]), which reduces the definition at higher-type directly to ground type. The Kleene-equivalence formulation used in the present article has the same effect, but it seems to scale better with respect to other types such as product and sum; the definition of full applications becomes hairy in the presence of these types.

Lemma B.6 (≺_{τ}^{Δ} is ω-admissible). For all E ∈ Expr_{τ}^{Δ}, the predicate − ≺_{τ}^{Δ} E is admissible, i.e., (1) it is chain-complete: If a_{0} ⊑ … ⊑ a_{i} ⊑ … is a countable chain in [[{|τ|}_{nϵ}]], such that ∀i.a_{i} ≺_{τ}^{Δ} E, then ⨆_{i≥0} a_{i} ≺_{τ}^{Δ} E; (2) it is pointed: ⊥ ≺_{τ}^{Δ} E.

Proof. By induction on type τ.

Case τ = b: Since {|b|}_{nϵ} = b, and base types are interpreted by flat domains, the chain must be constant after a certain position, and the upper bound equals this constant. Pointedness follows from the definition of the logical relation.

Case τ = ◯σ: Let f_{0} ⊑ … ⊑ f_{i} ⊑ … be a chain in [[{|τ|}_{nϵ}]] = Z_{⊥}→E_{⊥}. For a number n, if (⨆_{i≥0} f_{i})(val^{⊥} n) = ⨆_{i≥0}(f_{i}(val^{⊥} n)) ≠ ⊥, then ∃m.f_{m}(val^{⊥} n) ≠ ⊥. This implies E ⇓, by the definition of f_{m} ≺_{◯σ}^{Δ} E.

If f = ⊥, the implication in the definition of the logical relation holds vacuously.

Case τ = τ_{1} → τ_{2}: The predicate is given by

P (f) = ⋀_{(Δ′,a,E′)|Δ≤Δ′,a≺_{τ_{1}}^{Δ′} E′}(λϕ.ϕa)f ≺_{τ_{2}}^{Δ′} EE′.

It is admissible since all the − ≺_{τ_{2}}^{Δ} EE′ are admissible by induction hypothesis, and admissibility is closed under taking pre-image under strict continuous function and arbitrary intersection [54].

Lemma B.7 (Kleene equivalence respects ≺_{τ}^{Δ}). If v ≺_{τ}^{Δ} E, and E =^{kl} E′, i.e., ∀V.(E ⇓ V ⇔ E′ ⇓ V), then v ≺_{τ}^{Δ} E′.

Proof. By induction on type τ.

Case τ = b or τ = ◯σ: Immediate.

Case τ = τ_{1} → τ_{2}: Let a, Δ′ ≥ Δ, and E′′ ∈ Expr_{τ_{1}}^{Δ′} be such that a ≺_{τ_{1}}^{Δ′} E′′. Then we have

(1) v(a) ≺_{τ_{2}}^{Δ′} EE′′ (by the definition of v ≺_{τ}^{Δ} E);

(2) EE′′ =^{kl} E′E′′ (following from E =^{kl} E′).

Applying the induction hypothesis for τ_{2} to (1) and (2), we have that v(a) ≺_{τ_{2}}^{Δ′} E′E′′. This shows that v ≺_{τ_{1}→τ_{2}}^{Δ′} E′.

The logical relation extends naturally from types to typing contexts. Let Γ be a nPCF^{2}-typing context (x_{1} : τ_{1}, …, x_{n} : τ_{n}), Δ an object-type typing context, and θ a substitution (from ◯Δ to Γ) {E_{1}/x_{1}, …, E_{n}/x_{n}}, where nPCF^{2} ⊢ ◯Δ⊳ E_{i} : τ_{i}. We define the relation ≺_{Γ}^{Δ} between environments and substitutions as follows:

ρ ≺_{Γ}^{Δ} θ ⟺ ∀x ∈ dom Γ.ρx ≺_{Γ(x)}^{Δ} x{θ}

Now we are ready to prove our version of the “Basic Lemma”.

Lemma B.8. Let nPCF^{2} ⊢ Γ ⊳ E : τ, then for all Δ, ρ, and θ, ρ ≺_{Γ}^{Δ} θ implies that [[{|E|}_{nϵ}]]ρ ≺_{τ}^{Δ} E{θ} (it should be clear that ◯Δ ⊳ E{θ} : τ).

Proof. By induction on the size of the derivation for Γ ⊳ E : τ.

The static term formations have fairly standard sub-proofs.

Case ℓ: Trivial.

Case x: We need to show: ρx ≺_{τ}^{Δ} E{θ}. It follows from the definition of ρ ≺_{Γ}^{Δ} θ.

Case λx.E: We need to show: [[λx.{|E|}_{nϵ}]]ρ ≺_{τ_{1}→τ_{2}}^{Δ} (λx.E){θ}. For all Δ′ ≥ Δ and a ≺_{τ_{1}}^{Δ′} E′, we have ρ ≺_{Γ}^{Δ′} θ by Lemma B.5, and therefore ρ[x ↦ a] ≺_{Γ,x:τ_{1}}^{Δ′} (θ; E′/x). By induction hypothesis, we have

([[λx.{|E|}_{nϵ}]]ρ)a = [[{|E|}_{nϵ}]](ρ[x ↦ a]) ≺_{τ_{2}}^{Δ′} E{θ; E′/x}

Since ((λx.E){θ})E′ =^{kl} E{θ; E′/x}, we can apply Lemma B.7 to conclude that

([[λx.{|E|}_{nϵ}]]ρ)a ≺_{τ_{2}}^{Δ} ((λx.E){θ})E′.

Case E_{1} E_{2}: We need to show: [[{|E_{1}|}_{nϵ} {|E_{2}|}_{nϵ}]]ρ ≺_{τ}^{Δ} (E_{1} E_{2}){θ}. The induction hypotheses imply that [[{|E_{1}|}_{nϵ}]]ρ ≺_{τ_{2}→τ}^{Δ} E_{1}{θ} and that [[{|E_{2}|}_{nϵ}]]ρ ≺_{τ_{2}}^{Δ} E_{2}{θ}. By definition of ≺_{τ_{2}→τ}^{Δ} (taking Δ′ = Δ), we have

[[{|E_{1}|}_{nϵ} {|E_{2}|}_{nϵ}]]ρ = [[{|E_{1}|}_{nϵ}ρ]][[{|E_{2}|}_{nϵ}ρ]] ≺_{τ}^{Δ} (E_{1}{θ})(E_{2}{θ}) ≡ (E_{1} E_{2}){θ}

Case fix E: We need to show: ⨆_{i≥0} ([[{|E|}_{nϵ}]]ρ)^{i}(⊥) ≺_{τ}^{Δ} (fix E){θ}. We have

⊥ ≺_{τ}^{Δ} (fix E){θ}  (pointedness)
([[{|E|}_{nϵ}]]ρ)(⊥) ≺_{τ}^{Δ} E{θ}((fix E){θ}) =^{kl} (fix E){θ} (ind. hyp.)
⋮

By induction, for all i ≥ 0, ([[{|E|}_{nϵ}]]ρ)^{i}(⊥) ≺_{τ}^{Δ} (fix E){θ}. Finally, chaincompleteness (Lemma B.6) implies the conclusion.

Case if E_{1} E_{2} E_{3}: We need to show:

[[if {|E_{1}|}_{nϵ} {|E_{2}|}_{nϵ} {|E_{3}|}_{nϵ}]]ρ ≺_{τ}^{Δ} if E_{1} E_{2} E_{3}.

There are three sub-cases:

• [[{|E_{1}|}_{nϵ}]]ρ = ⊥: trivial.

• [[{|E_{1}|}_{nϵ}]]ρ = val^{⊥} tt: the induction hypotheses imply that (1) [[if {|E_{1}|}_{nϵ} {|E_{2}|}_{nϵ} {|E_{3}|}_{nϵ}]]ρ = [[{|E_{2}|}_{nϵ}]]ρ ≺_{τ}^{Δ} E_{2}{θ}, and

(2) E_{1}{θ} ⇓ tt, and henceforth E_{2}{θ} =^{kl} (if E_{1} E_{2} E_{3}){θ}. Applying Lemma B.7 to (1) and (2), we have the conclusion.

• [[{|E_{1}|}_{nϵ}]]ρ = val^{⊥} ff: similar to the previous case.

Case E_{1} ⊗ E_{2}: Simple.

The sub-proofs for dynamic term formations are intuitively very simple: the denotational semantics of various constructs are strict in the sub-terms, which, by induction hypotheses, implies that the evaluation of the subterms terminates. However, in the case of a dynamic λ-abstraction \underline{λ}x.E, the change of typing context requires special attention to ensure that the term we use is well-typed. For other cases, we only show the proof for $_{b}E.

Case $_{b}E: We need to show: [[$_{b}^{nϵ}{|E|}_{nϵ}]]ρ ≺_{◯b}^{Δ} ($_{b}E){θ}. For n ∈ Z, if ⊥ ≠ [[$_{b}^{nϵ}{|E|}_{nϵ}]]ρ(val^{⊥} n) = [[LIT_{b}({|E|}_{nϵ})]]ρ = let^{⊥} l ⇐ [[{|E|}_{nϵ}]]ρ in val^{⊥} (inLit_{b}(l)), then [[{|E|}_{nϵ}]]ρ ≠ ⊥. By induction hypothesis, we have [[{|E|}_{nϵ}]]ρ ≺_{b}^{Δ} E{θ}, which implies that E{θ} ⇓, and consequently ($_{b}E){θ} ⇓.

Case \underline{λ}x.E: Recall that the typing rule is

\frac{Γ, x: ◯σ_{1} ⊳ E : ◯σ_{2}}{Γ ⊳ \underline{λ}x.E : ◯(σ_{1} → σ_{2})}

We need to show: [[\underline{λ}^{nϵ}(λx.\{|E|\}_{nϵ})]]ρ ≺_{◯(σ_{1}→σ_{2})}^{Δ} (\underline{λ}x.E)\{θ\}. Without loss of generality, we assume x ∉ dom Δ; otherwise we can rename the bound variable using α-conversion. Now for any n ∈ Z, if [[\underline{λ}^{nϵ}(λx.\{|E|\}_{nϵ})]]ρ(val^{⊥} n) ≠ ⊥, then it is easy to show that [[{|E|}_{nϵ}]]ρ[x ↦ λw.val^{⊥} (inVar(n))] ≠ ⊥.

Since x ∉ dom Δ, the context Δ, x : σ_{1} is well-formed. It is easy to check that λw.val^{⊥} (inVar(n)) ≺_{◯σ_{1}}^{Δ,x:σ_{1}} x; furthermore, since ≺ is Kripke, we also have that ρ ≺_{Γ}^{Δ,x:σ_{1}} θ. Putting them together, we have that

ρ[x ↦ λw.val^{⊥} (inVar(n))] ≺_{Γ,x:◯σ_{1}}^{Δ,x:σ_{1}} {θ; x/x}.

Then, by the induction hypothesis, we get

[[{|E|}_{nϵ}]](ρ[x ↦ λw.val^{⊥} (inVar(n))]) ≺_{◯σ_{2}}^{Δ,x:σ_{1}} E{θ; x/x} ≡ E{θ}

Since lhs ≠ ⊥, we have, by the definition of the logical relation, that E{θ} ⇓. Consequently \underline{λ}x.(E\{θ\}) ⇓.

Finally, Lemma 2.9 is an easy corollary.

Proof of Lemma 2.9. Let ρ be the empty environment, and θ the empty substitution. We have that [[{|E|}_{nϵ}(1)]]ρ = [[t]]ρ. Since t is a value, [[t]]ρ ≠ ⊥. Thus [[{|E|}_{nϵ}]]ρ(val^{⊥} 1) = [[{|E|}_{nϵ}(1)]]ρ ≠ ⊥. By Lemma B.8, [[{|E|}_{nϵ}]]ρ ≺_{◯σ}^{·} E{θ} ≡ E. The definition of the logical relation at the type ◯σ implies that E ⇓.

Theorem 2.10 (Correctness of embedding). If nPCF^{2} ⊢ ⊳E : ◯σ, then the following statements are equivalent.

(a) There is a value O : ◯σ such that nPCF^{2} ⊢ E ⇓ O.

(b) There is a value t : Λ such that [[{|E|}_{nϵ}(1)]] = [[t]]. When these statements hold, we further have that

(c) nPCF ⊢ ⊳D(t) : σ and |O| ∼_{α} D(t).

Proof. (a) ⇒ (b),(c) Assume (a). By Lemma 2.7, nPCF^{Λ} ⊢ {|E|}_{nϵ} = {|O|}_{nϵ}. By Lemma 2.8, there is a value t such that nPCF^{Λ} ⊢ {|O|}_{nϵ}1 = t, with which (c) also holds. By the transitivity rule, we have that nPCF^{Λ} ⊢ {|E|}_{nϵ}1 = t. The conclusion now follows by an application of Theorem B.3.

(b) ⇒ (a),(c) Assume (a). By Lemma 2.9, E ⇓. Since ⊳E : ◯σ, we have E ⇓ O for some value O : ◯σ. By the first part of this proof, we further have an nPCF^{Λ}-value t′ : Λ that satisfies (c) (with t replaced by t′) and validates [[{|E|}_{nϵ}(1)]] = [[t′]]. It remains to show that t ≡ t′.

Because [[t]] = [[{|E|}_{nϵ}(1)]] = [[t′]], and the semantic function of Λ-typed values is injective (easy structural induction), we have that t ≡ t′.

B.3 Call-by-name type-directed partial evaluation

Lemma 2.11. For all types σ, nPCF ⊢ ⊳ |↓^{σ}| = λx.x : σ → σ and nPCF ⊢ ⊳ |↑_{σ}| = λx.x : σ → σ.

Proof. By a straightforward induction on type τ.

Theorem 2.12 (Semantic correctness of TDPE). If nPCF^{tdpe} ⊢ ⊳E : σ^{𝔡} and nPCF^{2} ⊢ NF (E) ⇓ O, then nPCF ⊢ ⊳ |O| = |E| : σ.

(Note that the two erasures are different: one operates on nPCF^{2}-terms, the other on nPCF^{tdpe}-terms.)

Proof. First, we prove by induction on nPCF^{tdpe} ⊢ ⊳E : φ that nPCF ⊢ ⊳ |{|E|}_{ri}| = |E| : |φ|. The proofs for the static part, for which both translations are homomorphic, are straightforward and omitted. The only remaining cases are the following ones.

Case $_{b}E: We have |{|$_{b}E|}_{ri}| ≡ |$_{b}{|E|}_{ri}| ≡ |{|E|}_{ri}| =^{i.h.} |E| ≡ |$_{b}E|.

Case d^{𝔡} : σ^{𝔡}: We have |\{|d^{𝔡}|\}_{ri}| ≡ |↑_{σ}||\underline{d}| =^{∗} d ≡ |d^{𝔡}|, where =^{∗} uses Lemma 2.11 and the definition of erasure for nPCF^{2}-terms.

From this, we can infer that |NF (E)| ≡ |↓^{σ}| |{|E|}_{ri}| = |E|, again using Lemma 2.11. Now, applying Theorem 2.3 to nPCF^{2} ⊢ NF (E) ⇓ O, we can conclude that |O| = |NF (E)| = |E|.

Theorem 2.13 (Refined type preservation). If nPCF^{2} ⊢ ◯^{var}(Δ) ▶ E : τ and nPCF^{2} ⊢ E ⇓ V, then nPCF^{2} ⊢ ◯^{var}(Δ) ▶ V : τ.

Like in the proof of Theorem 2.1, the most interesting case is when E ≡ E_{1} E_{2}, for which we need a Substitution Lemma.

Lemma B.9 (▶-substitutivity). If nPCF^{2} ⊢ Γ, y : τ_{1} ▶ E : τ_{2} and nPCF^{2} ⊢ Γ ▶ E′ : τ_{1}, then nPCF^{2} ⊢ Γ ▶ E{E′/y} : τ_{2}.

Proof. By a straightforward induction on the derivation of the typing judgment nPCF^{2} ⊢ Γ, x : τ_{1} ▶ E : τ_{2}.

Proof of Theorem 2.13. By induction on E ⇓ V. The only non-straightforward case in the static part is the rule ([app]), i.e., the evaluation of an application; for this rule we use Lemma B.9. For the dynamic part, all the rules simply evaluate the subterms while keeping the top-level constructs; combining the induction hypotheses suffices to give the same typing for the result values V as for the original terms E.

Theorem 2.14 (Normal-form code types). If V is an nPCF^{2}-value (Figure 2), then

(1) if nPCF^{2} ⊢ ◯^{var}(Δ) ▶ V : ◯^{at}(σ), then V ≡ O for some O and Δ ⊳^{at} |O| : σ;

(2) if nPCF^{2} ⊢ ◯^{var}(Δ) ▶ V : ◯^{nf} (σ), then V ≡ O for some O and Δ⊳^{nf} |O| : σ.

Proof. First of all, if a value V is of any code type ◯^{var}(σ), ◯^{at}(σ), or ◯^{nf} (σ), then a simple examination of the rules shows that V can be neither of the form ℓ nor of the form λx.E, and thus it must be of the form O. Furthermore, if nPCF^{2} ⊢ ◯^{var}(Δ) ▶ O : ◯^{var}(σ), then O must be a variable x such that x : σ ∈ Δ, since in all other cases of O, the type could not be ◯^{var}(σ).

According to the BNF for a code-typed value O, the only rules that can be used in the derivation of O’s typing are the rules in the (new) dynamic part plus the rules for literals and variables. Now, a simple rule induction proves (1) and (2).

Lemma 2.15. (1) The extraction functions (Figure 5c) have the following normal-form types (writing σ^{◯nf} for σ{◯^{nf} (b)/b : b ∈ 𝔹}).

▶ ↓^{σ} : σ^{◯nf} → ◯^{nf} (σ), ▶ ↑_{σ} : ◯^{at}(σ) → σ^{◯nf}.

(2) If nPCF^{tdpe} ⊢ Γ ⊳ E : φ, then nPCF^{2} ⊢ {|Γ|}_{ri}^{nf} ▶ {|E|}_{ri} : {|φ|}_{ri}^{nf}, where {|φ|}_{ri}^{nf} = φ{◯^{nf} (b)/b^{𝔡} : b ∈ 𝔹}

Proof.

(1) By induction on type σ.

Case σ = b: Because at the base type, b^{◯nf} = ◯^{nf} (b), we just need to show: ▶ λx.x : ◯^{nf} (b) → ◯^{nf} (b). This is simple.

Case σ = σ_{1} → σ_{2}: Noting that (σ_{1} → σ_{2})^{◯nf} = σ_{1}^{◯nf} → σ_{2}^{◯nf}, we give the following typing derivation for ↓^{σ_{1}→σ_{2}} based on the induction hypotheses (we use weakening freely and implicitly, write Γ_{1} for the context f : σ_{1}^{◯nf} →σ_{2}^{◯nf}, x : ◯^{var}(σ_{1}), and omit the typing of ↑_{σ_{1}} and ↓^{σ_{2}} from the induction hypotheses):

\frac{\frac{\frac{\frac{Γ_{1} ▶ f : σ_{1}^{◯nf} → σ_{2}^{◯nf} \frac{\frac{Γ_{1} ▶ x : ◯^{var}(σ_{1})}{Γ_{1} ▶ x : ◯^{at}(σ_{1})}}{Γ_{1} ▶ ↑_{σ_{1}}x : σ_{1}^{◯nf}}}{Γ_{1} ▶ f (↑_{σ_{1}}x) : σ_{2}^{◯nf}}}{Γ_{1} ▶ ↓^{σ_{2}}(f (↑_{σ_{1}}x)) : ◯^{nf} (σ_{2})}}{f : σ_{1}^{◯nf} → σ_{2}^{◯nf} ▶ \underline{λ}x.↓^{σ_{2}}(f (↑_{σ_{1}}x)) : ◯^{nf} (σ_{1} → σ_{2})}}{▶ λf.\underline{λ}x.↓^{σ_{2}}(f (↑_{σ_{1}}x)) : (σ_{1}^{◯nf} → σ_{2}^{◯nf}) → ◯^{nf} (σ_{1} → σ_{2})}

A similar derivation works for ↑_{σ_{1}→σ_{2}}, which is compactly described as the following:

e : ◯^{at}(σ_{1} → σ_{2}), x : σ_{1}^{◯nf} ▶ ↑_{σ_{2}}(\overbrace{e\underline{@}( \underbrace{↓^{σ_{1}}x}_{◯^{nf} (σ_{1})})}^{◯^{at} (σ_{2})}) : σ_{2}^{◯nf}

(2) By a simple induction on nPCF^{tdpe} ⊢ Γ ⊳ E : φ. For the case when E ≡ d^{𝔡} with Sg(d) = σ, we use the typing of ↑_{σ} from part (1) and the fact that {|σ^{𝔡}|}_{ri}^{nf} ≡ {|σ{b^{𝔡}/b : b ∈ 𝔹}|}_{ri}^{nf} ≡ σ{◯^{nf} (b)/b : b ∈ 𝔹} ≡ σ^{◯nf}.

Theorem 2.16. If nPCF^{tdpe} ⊢ ⊳E : σ^{𝔡}, then nPCF^{2} ⊢▶ NF (E) : ◯^{nf} (σ).

Proof. By Lemma 2.15(2), we have nPCF^{2} ⊢▶ {|E|}_{ri} : {|σ^{𝔡}|}_{ri}^{nf}. Since {|σ^{𝔡}|}_{ri}^{nf} ≡ σ^{◯nf}, applying ↓^{σ} : σ^{◯nf} → ◯^{nf} (σ) (Lemma 2.15(1)) to {|E|}_{ri} yields the conclusion.

Corollary 2.17 (Syntactic correctness of TDPE). For nPCF^{tdpe} ⊢ ⊳E : σ^{𝔡}, if nPCF^{2} ⊢ NF (E) ⇓ V, then V ≡ O for some O and nPCF ⊢ Δ ⊳^{nf} |O| : σ.

Proof. We use Theorem 2.16, Theorem 2.13, and Theorem 2.14.

C Call-by-value two-level language vPCF^{2}: detailed development

Since we are working with vPCF^{2} in this section, we leave vPCF^{2} ⊢ implicit.

C.1 Type preservation

Lemma C.1 (Substitution Lemma for vPCF^{2}-typing). If Γ, y : τ_{1} ⊳ E : τ_{2} and Γ ⊳ E′ : τ_{1}, then Γ ⊳ E{E′/y} : τ_{2}.

For a concise presentation, we introduce the following notations.

Definition C.2 (Binder-in-context). For a binder B ≡ (x_{1}:σ_{1} = O_{1}, …, x_{n}: σ_{n} = O_{n}), we write Γ ⊳ [B] if Γ, x_{1} : v ◯σ_{1}, …, x_{i−1} : v ◯σ_{i−1} ⊳ O_{i} : e ◯σ_{i} for all 1 ≤ i ≤ n. In this case, we also write Γ, v ◯B for the context Γ, v ◯σ_{1}, …, v ◯σ_{n}.

Definition C.3 (Binder extension and difference). We write Γ ⊳ [B] ≥ [B′], if binder B′ is a prefix of binder B, and Γ ⊳ [B]. In this case, it makes sense to write B − B′ to denote the difference of the two binders, and we have that Γ, v ◯B ⊳ [B − B′].

We can restate Definition 4.1 using the preceding notions.

Definition 4.1 (Binder-term-in-context). We write Γ ⊳ [B]E : τ if Γ ⊳ [B] and Γ, v ◯B ⊳ E : τ.

To ease analyses of binder-terms-in-context, we prove an “inversion” lemma. Informally, it states that one can apply inversion to a binder-term-in-context as if to a term-in-context,

Lemma C.4 (“Inversion” holds for binder-terms-in-context). Let Γ ⊳ [B]E : τ.

• If E = λx.E′, then τ = τ_{1} →τ_{2} and Γ, x : τ_{1} ⊳[B]E′ : τ_{2}. This corresponds to the typing rule [lam].

• If E = E_{1} E_{2}, then ∃τ_{2} such that Γ ⊳ [B]E_{1} : τ_{2} → τ and Γ ⊳ [B]E_{2} : τ_{2}. This corresponds to the typing rule [app].

• ⋮ (similar inversion principles for all the other typing rules, except the rule [var], which uses the context explicitly.)

Corollary C.5. (Substitution for binder-term-in-context) If Γ, y : τ_{1}⊳[B]E : τ_{2} and Γ ⊳ [B]E′ : τ_{1}, then Γ ⊳ [B]E{E′/x} : τ_{2}.

Proof. The provability of binder-term-in-context Γ ⊳ [B]E′ : τ_{1}, by definition, implies the following.

(1.a) Γ ⊳ [B].

(1.b) Γ, v ◯B ⊳ E′ : τ_{1}.

From (1.a) and Γ, y : τ_{1} ⊳ [B]E : τ_{2} we have

(2) (Γ, v ◯B), y : τ_{1} ⊳ E : τ_{2}.

Applying Lemma C.1 to (1.b) and (2) yields the conclusion.

Lemma C.6. If Γ ⊳ [B]E : τ and Γ ⊳ [B′] ≥ [B], then Γ ⊳ [B′]E : τ. Proof. The definition of Γ ⊳ [B]E : τ implies

(1) Γ, v ◯B ⊳ E : τ. The definition of Γ ⊳ [B′] ≥ [B] implies (2.a) Γ ⊳ [B′]. (2.b) Γ, v ◯B ⊆ Γ, v ◯B′. Weakening (1) with respect to (2.b) yields Γ, v ◯B′ ⊳ E : τ, which, along with (2.a), is exactly the definition of Γ ⊳ [B′]E : τ.

If a binder-term-in-context has a code type e ◯τ, then we can convert it into a term-in-context using the let-construct. This observation is manifested in the following lemma. Lemma C.7. If Γ ⊳ [B]O : e ◯τ, then Γ ⊳ let^{∗} B in O : e ◯τ.

We slightly strengthen the type preservation theorem 4.2, so as to make the induction go through. Theorem 4.2 (Type preservation). If v ◯Δ⊳[B]E : τ and Δ⊳[B]E ⇓ [B′]V, then (1) v ◯Δ ⊳ [B′]V : τ, and (2) v ◯Δ ⊳ [B′] ≥ [B]. Proof. By induction on Δ⊳[B]E ⇓ [B′]V. For (2), note that, for all the implicit rules, Δ ⊳ [B_{n+1}] ≥ … ≥ [B_{1}] follows immediately from transitivity of “≥” and the induction hypotheses; for the three rules where binders are explicitly mentioned, it is also clear that (2) holds.

For (1), we show a few cases. Case [lit], [lam]: There is nothing to prove. Case [app]: The rule in its full from is

\frac{Δ ⊳ [B_{1}]E_{1} ⇓ [B_{2}]λx.E′ Δ ⊳ [B_{2}]E_{2} ⇓ [B_{3}]V′ Δ ⊳ [B_{3}]E′\{V′/x\} ⇓ [B_{4}]V}{Δ ⊳ [B_{1}]E_{1} E_{2} ⇓ [B_{4}]V}

for which we reason as follows:

(1) By assumption, v ◯Δ ⊳ [B_{1}]E_{1} E_{2} : τ.

(2) Inverting (Lemma C.4) (1) gives a. v ◯Δ ⊳ [B_{1}]E_{1} : θ_{2} → τ, and b. v ◯Δ ⊳ [B_{1}]E_{2} : θ_{2}.

(3) From (2.a), by induction hypothesis 1 (counting from left to right), a. v ◯Δ ⊳ [B_{2}]λx.E′ : θ_{2} → τ, and b. v ◯Δ ⊳ [B_{2}] ≥ [B_{1}].

(4) Applying Lemma C.6 to (2.b) and (3.b) yields

v ◯Δ ⊳ [B_{2}]E_{2} : θ_{2} By induction hypothesis 2, a. v ◯Δ ⊳ [B_{3}]V′ : θ_{2} b. v ◯Δ ⊳ [B_{3}] ≥ [B_{2}].

(5) Applying Lemma C.6 to (4.b) and (3.a), and then inversion yields v ◯Δ, x : θ_{2} ⊳ [B_{3}]E′ : τ

(6) Applying Substitution (Corollary C.5) to (5) and (4.a) yields

v ◯Δ ⊳ [B_{3}]E′{V′/x} : τ. By induction hypothesis 3, v ◯Δ ⊳ [B_{4}]V : τ.

Case [fix]: The rule in its full form is

\frac{Δ ⊳ [B_{1}]E ⇓ [B_{2}]λx.E′ Δ ⊳ [B_{2}]E′\{fix (λx.E′)/x\} ⇓ [B_{3}]V}{Δ ⊳ [B_{1}]fix E ⇓ [B_{3}]V}

for which we reason as follows:

(1) By assumption, v ◯Δ ⊳ [B_{1}]fix E : τ (where τ = θ_{1} → τ_{2} for some θ_{1} and τ_{2}).

(2) Inverting (1) gives v ◯Δ ⊳ [B_{1}]E : τ → τ.

(3) Applying induction hypothesis 1 to (2) yields v ◯Δ ⊳ [B_{2}]λx.E′ : τ → τ.

(4) Inverting (3) gives

a. v ◯Δ, x : τ ⊳ [B_{2}]E′ : τ An application of the typing rule ([fix]) to (3) gives

b. v ◯Δ ⊳ [B_{2}]fix λx.E′ : τ

(5) Applying Substitution to (4.a) and (4.b) yields v ◯Δ ⊳ [B_{2}]E′{fix (λx.E′)/x} : τ.

(6) Applying induction hypothesis 2 to (5) yields v ◯Δ ⊳ [B_{3}]V : τ.

Case [\underline{lam}]: The rule is

\frac{Δ, y : σ, B ⊳ [·]E\{y/x\} ⇓ [B′]O y ∉ dom B ∪ dom Δ}{Δ ⊳ [B]\underline{λ}x.E ⇓ [B]\underline{λ}y.\underline{let}^{∗} B′ \underline{in} O}

for which we reason as follows:

(1) By assumption, v ◯Δ ⊳ [B]\underline{λ}x.E : e ◯(σ_{1} → σ_{2})

(2) Inverting (1) gives

v ◯Δ, x : v ◯σ_{1} ⊳ [B]E : e ◯σ_{2} from which it follows that v ◯Δ, y : v ◯σ_{1}⊳[B]E{y/x} : e ◯σ_{2}. That is (noting that v ◯Δ, y : v ◯σ_{1} ≡ v ◯(Δ, y : σ_{1})) a. v ◯(Δ, y : σ_{1}) ⊳ [B], and b. v ◯(Δ, y : σ_{1}, B) ⊳ E{y/x} : e ◯σ_{2}.

(3) Use the induction hypothesis on (2.b) (noting that Γ⊳E : τ ⇔ Γ⊳[·]E : τ),

we have

v ◯(Δ, y : σ_{1}, B) ⊳ [B′]O : e ◯σ_{2}

(4) Apply Lemma C.7 to (3) yields

v ◯(Δ, y : σ_{1}, B) ⊳ let^{∗} B′ in O : e ◯σ_{2} Finally, applying the typing rule for dynamic lambda \underline{λ}y.E, [\underline{lam}], yields v ◯Δ, v ◯B ⊳ \underline{λ}y.let^{∗} B′ in O : e ◯(σ_{1} → σ_{2}).

Case [\underline{let}]: Similar to the case of rule [\underline{lam}]. Case [#]: The rule is

\frac{Δ ⊳ [B]E ⇓ [B′]O x ∉ dom B′ ∪ dom Δ}{Δ ⊳ [B]#E ⇓ [B′, x : σ = O]x}

for which we reason as follows:

(1) By assumption, v ◯Δ ⊳ [B]#E : τ. Without loss of generality, we can assume that τ = v ◯σ; the other case, where τ = e ◯σ, can be reduced to this case using one inversion. Therefore, we have,

v ◯Δ ⊳ [B]#E : v ◯σ.

(2) Inverting (1) gives v ◯Δ ⊳ [B]E : e ◯σ

(3) Use induction hypothesis on (2) gives

v ◯Δ ⊳ [B′]O : e ◯σ.

Because x ∉ dom B′ ∪ dom Δ, we have v ◯Δ ⊳ [B′, x : σ = O] by definition. We also have v ◯(Δ, B), x : v ◯σ ⊳ x : v ◯σ. Therefore, by definition, we have

v ◯Δ ⊳ [B′, x : σ = O]x : v ◯σ.

Recall that the observation of a complete program is defined to be that of code type.

Definition 4.3 (Observation of complete program). For a complete program ⊳E : e ◯σ, we write E ↘ \underline{let}^{∗} B \underline{in} O if ⊳[·]E ⇓ [B]O.

In accordance with this understanding of complete-program semantics, the following corollary of the Type Preservation theorem (Theorem 4.2) provides type preservation for a complete program.

Corollary 4.4 (Type preservation for complete programs). If ⊳E : e ◯σ and E ↘ O, then ⊳O : e ◯σ.

Proof. Assume ⊳[·]E ⇓ [B]O′ where O ≡ let^{∗} B in O′. We have

⊳E : e ◯σ
⟹ ⊳[·]E : e ◯σ
⟹^{(∗)} ⊳[B]O′ : e ◯σ
⟹^{(∗∗)} ⊳let^{∗} B in O′ : e ◯σ

where (∗) follows from Theorem 4.2 and (∗∗) follows from Lemma C.7.

C.2 Determinacy

Next, we would like to show that the operational semantics of vPCF^{2} is deterministic. At the top level, determinacy can be easily phrased as “evaluating a whole program gives a unique result, modulo α-equivalence”. Going into the inductive steps for the proof, however, requires an extension of the notion of αequivalence to take into account of binders, and in turn, of contexts. This extra conceptual complexity is induced, in particular, by the explicit name generations and context manipulation in rules such as [\underline{lam}].

Definition C.8 (Name substitution). A name substitution is a substitution that maps variable names to variable names. Applying a name substitution θ to a context Γ substitutes the variable names in Γ:

Γ{θ} ≜ {(x{θ} : τ)|(x : τ) ∈ Γ}

Definition C.9 (α-equivalence for terms-in-context). Let Γ ⊳ E : τ and Γ′ ⊳ E′ : τ be two valid terms-in-context. We say that they are α-equivalent, noted as (Γ ⊳ E) ∼_{α} (Γ′ ⊳ E′), if there exists a name substitution θ such that

\begin{aligned}Γ′ & ≡ & Γ\{θ\} \\ E′ & ∼_{α} & E\{θ\} \end{aligned}

We then define the corresponding notion of α-equivalence for binders-in-context (omitted, cf. Definition C.2), and the subsequent notion of α-equivalence for binder-terms-in-context.

Definition C.10 (α-equivalence for binder-terms-in-context). Let Γ ⊳ [B]E : τ and Γ′ ⊳ [B′]E′ : τ. We say that they are α-equivalent if (Γ ⊳ [B]) ∼_{α} (Γ′ ⊳ [B′]) and (Γ, v ◯B ⊳ E) ∼_{α} (Γ′, v ◯B′ ⊳ E′).

All the above notions of α-equivalences define equivalence relations. This follows immediately from the fact that the usual α-equivalence defines a equivalence relation.

Lemma C.11 (Collecting binders preserves α-equivalence). Let Γ ⊳ [B]E : ◯σ and Γ′⊳[B′]E′ : ◯σ be two valid terms-in-contexts. If (Γ ⊳ [B]E) ∼_{α} (Γ′ ⊳ [B′]E′), then (Γ ⊳ \underline{let}^{∗} B \underline{in} E) ∼_{α} (Γ′ ⊳ \underline{let}^{∗} B′ \underline{in} E′).

Proof. Immediate.

Lemma C.12. Let (Γ ⊳ [B]λx.E) ∼_{α} (Γ′ ⊳ [B′]λx′.E′) and (Γ ⊳ [B]E_{1}) ∼_{α} (Γ′ ⊳ [B′]E′_{1}). Then, (Γ ⊳ [B]E{E_{1}/x}) ∼_{α} (Γ′ ⊳ [B′]E′{E′_{1}/x}).

Theorem C.13 (Determinacy modulo α-conversion). Let v ◯Δ⊳[B_{1}]E_{1} : τ and v ◯Δ′ ⊳ [B′_{1}]E′_{1} : τ be valid terms-in-contexts such that (v ◯Δ ⊳ [B_{1}]E_{1}) ∼_{α} (v ◯Δ′ ⊳ [B′_{1}]E′_{1}). If Δ ⊳ [B_{1}]E_{1} ⇓ [B_{2}]E_{2}, then (1) for all B′_{2} and E′_{2} such that Δ′ ⊳ [B′_{1}]E′_{1} ⇓ [B′_{2}]E′_{2}, we have (v ◯Δ ⊳ [B_{2}]E_{2}) ∼_{α} (v ◯Δ′ ⊳ [B′_{2}]E′_{2}); and (2) such B′_{2} and E′_{2} exist.

Furthermore, the derivation trees for Δ ⊳ [B_{1}]E_{1} ⇓ [B_{2}]E_{2} and for Δ′ ⊳ [B′_{1}]E′_{1} ⇓ [B′_{2}]E′_{2} have exactly the same shape.

Proof. By induction on Δ ⊳ [B_{1}]E_{1} ⇓ [B_{2}]E_{2}, we prove that for all such Δ′, B′_{1}, E′_{1}, B′_{2}, E′_{2} that satisfy the rest of the premises, it holds that (v ◯Δ_{1} ⊳ [B′_{1}]E′_{1}) ∼_{α} (v ◯Δ_{2} ⊳ [B′_{2}]E′_{2}). The proof for (2) is easy, so we concentrate on (1).

We demonstrate two cases. For the expression forms E′ that have a unique inversions (i.e., those that are not if-expressions), we omit the inversion of E′.

Case [app]: The derivations end with

\frac{Δ ⊳ [B_{1}]E_{1} ⇓ [B_{2}]λx.E_{3} Δ ⊳ [B_{2}]E_{2} ⇓ [B_{3}]V_{1} Δ ⊳ [B_{3}]E_{3}\{V_{1}/x\} ⇓ [B_{4}]V}{Δ ⊳ [B_{1}]E_{1} E_{2} ⇓ [B_{4}]V}

for which we have the following reasoning:

(1) The assumption (v ◯Δ ⊳ [B_{1}]E_{1} E_{2}) ∼_{α} (v ◯Δ′ ⊳ [B′_{1}]E′_{1} E′_{2}) implies a. (v ◯Δ ⊳ [B_{1}]E_{1}) ∼_{α} (v ◯Δ′ ⊳ [B′_{1}]E′_{1}), and

b. (v ◯Δ ⊳ [B_{1}]E_{2}) ∼_{α} (v ◯Δ′ ⊳ [B′_{1}]E′_{2}).

(2) From (1.a), by induction hypothesis 1:

(v ◯Δ ⊳ [B_{2}]λx.E_{3}) ∼_{α} (v ◯Δ′ ⊳ [B′_{2}]λx.E′_{3}).

(3) From (1.b) and that binders B_{2} and B′_{2} extend B_{1} and B′_{1}, by induction hypothesis 2:

(v ◯Δ ⊳ [B_{3}]V_{1}) ∼_{α} (v ◯Δ′ ⊳ [B′_{3}]V′_{1})

(4) An application of Lemma C.12 to (2) and (3) (with binders properly extended), followed by an application of hypothesis 3, gives the conclusion.

Case [\underline{lam}]: The derivations end with

\frac{Δ, y : σ; B_{1} ⊳ [·]E\{y/x\} ⇓ [B_{2}]O y ∉ dom B_{1} ∪ dom Δ}{Δ ⊳ [B_{1}]\underline{λ}x.E ⇓ [B_{1}]\underline{λ}y.\underline{let}^{∗} B_{2} \underline{in} O}

for which we have the following reasoning:

(1) The assumption (v ◯Δ ⊳ [B_{1}]λx.E) ∼_{α} (v ◯Δ′ ⊳ [B′_{1}]λx′.E′) implies that

(v ◯Δ, v ◯B_{1} ⊳ λx.E) ∼_{α} (v ◯Δ′, v ◯B′_{1} ⊳ λx′.E′)

which, by definition, implies that

(v ◯(Δ, y : σ_{1}), v ◯B_{1} ⊳ E{y/x}) ∼_{α} (v ◯(Δ′, y′ : σ_{1}), v ◯B′_{1} ⊳ E′{y′/x′}).

(2) An application of the induction hypothesis to (1) yields

(v ◯(Δ, y : σ_{1}), v ◯B_{1} ⊳ [B_{2}]O) ∼_{α} (v ◯(Δ′, y′ : σ_{1}), v ◯B′_{1} ⊳ [B′_{2}]O′)

By Lemma C.11, we have

(v ◯(Δ, y : σ_{1}), v ◯B_{1} ⊳ \underline{let}^{∗} B_{2} \underline{in} O)
∼_{α}
(v ◯(Δ′, y′ : σ′_{1}), v ◯B′_{1} ⊳ \underline{let}^{∗} B′_{2} \underline{in} O′)

This implies the conclusion.

Types  σ ::= b | σ_{1} → σ_{2}
Raw terms E ::= ℓ | x | d | λx.E | E_{1} E_{2} | fix E
| if E_{1} E_{2} E_{3} | E_{1} ⊗ E_{2} | let x ⇐ E_{1} in E_{2}
Typing Judgment  vPCF ⊢ Δ ⊳ E : σ

The typing rules are very close to that of nPCF. For the convenience of the reader, we display the complete rules here.

[lit] \frac{ℓ ∈ 𝕃(b)}{Δ ⊳ ℓ : b} [var] \frac{x: σ ∈ Δ}{Δ ⊳ x : σ} [cst] \frac{Sg(d) = σ}{Δ ⊳ d : σ} [lam] \frac{Δ, x: σ_{1} ⊳ E : σ_{2}}{Δ ⊳ λx.E : σ_{1} → σ_{2}}
[app] \frac{Δ ⊳ E_{1} : σ_{2} → σ Δ ⊳ E_{2} : σ_{2}}{Δ ⊳ E_{1} E_{2} : σ} [fix] \frac{Δ ⊳ E : (σ_{1} → σ_{2}) → (σ_{1} → σ_{2})}{Δ ⊳ fix E : σ_{1} → σ_{2}}
[if ] \frac{Δ ⊳ E_{1} : bool Δ ⊳ E_{2} : σ Δ ⊳ E_{3} : σ}{Δ ⊳ if E_{1} E_{2} E_{3} : σ}

[bop] \frac{Δ ⊳ E_{1} : b_{1} Δ ⊳ E_{2} : b_{2}}{Δ ⊳ E_{1} ⊗ E_{2} : b} (⊗ : b_{1} × b_{2} → b)

[let] \frac{Δ, x: σ_{1} ⊳ E_{2} : σ_{2} Δ ⊳ E_{1} : σ_{1}}{Δ ⊳ let x ⇐ E_{1} in E_{2} : σ_{2}}
Equational Rules  vPCF ⊢ Δ ⊳ E_{1} = E_{2} : σ

The equational rules distinguish a subset of (possibly non-closed) terms, called values, ranged over by meta-variable V. Values V ::= ℓ | x | λx.E | d

Let x, f, and g range over variables in the rules.

Congruence rules: = is a congruence. (Detailed rules omitted) Equations for let-expressions

[unit] Δ ⊳ let x ⇐ E in x = E : σ [assoc]

Δ⊳ let x_{2} ⇐ (let x_{1} ⇐ E_{1} in E_{2}) in E
= let x_{1} ⇐ E_{1} in let x_{2} ⇐ E_{2} in E : σ

[let.β] Δ ⊳ let x ⇐ V in E = E{V/x} : σ [let.app] Δ ⊳ E_{1} E_{2} = let x_{1} ⇐ E_{1} in let x_{2} ⇐ E_{2} in x_{1} x_{2} : σ [let.fix] Δ ⊳ fix E = let x ⇐ E in fix x : σ_{1} → σ_{2} [let.if ] Δ ⊳ if E_{1} E_{2} E_{3} = let x_{1} ⇐ E_{1} in if x E_{2} E_{3} : σ [let.⊗] Δ ⊳ E_{1} ⊗ E_{2} = let x_{1} ⇐ E_{1} in let x_{2} ⇐ E_{2} in x_{1} ⊗ x_{2} : b

Other rules [β_{v}] Δ ⊳ (λx.E)V = E{V/x} : σ [η_{v}] Δ ⊳ (λx.f x) = f : σ_{1} → σ_{2} [fix-dinat] Δ ⊳ fix (f ∘ g) = f(fix (g ∘ f)) : σ_{1} → σ_{2} [if-tt] Δ ⊳ if tt E_{2} E_{3} = E_{2} : σ [if-ff] Δ ⊳ if ff E_{2} E_{3} = E_{3} : σ [if-η] Δ ⊳ if x E E = E : σ [⊗] Δ ⊳ ℓ_{1} ⊗ ℓ_{2} = ℓ : b (ℓ_{1} ⊗ ℓ_{2} = ℓ)

Figure 14: One-level call-by-value language vPCF

C.3 Annotation erasure

First, we display the equational rules of vPCF in Figure 14. As mentioned in Section 4, vPCF is an instance of Moggi’s computational λ-calculus [35].

Lemma C.14 (Erasure of θ-typed values). Let V be a vPCF^{2}-value (see Figure 9). If Γ ⊳ V : θ (i.e., V is of a substitution-safe type), then |V | is a vPCF-value.

Lemma 4.5 (Annotation erasure). If vPCF^{2} ⊢ v ◯Δ ⊳ [B]E : τ and vPCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V, then vPCF ⊢ Δ ⊳ let^{∗} |B| in |E| = let^{∗} |B′| in |V | : |τ|.

Proof. We prove by induction on Δ ⊳ [B]E ⇓ [B′]V that

Δ; B ⊳ |E| = let^{∗} |B′ − B| in V : |τ|,

from which the conclusion follows using the congruence rule for let. We write δ_{i,j}B (j ≥ i) for B_{j} − B_{i}.

Case [lit], [lam]: There is nothing to prove.

Case [app]: Applying Theorem 4.2 to E_{2} ⇓ V′, and then using Lemma C.14, we have that |V′| is a vPCF-value. Now we have

|E_{1} E_{2}| ≡ |E_{1}| |E_{2}|
=^{i.h.} (let^{∗} |δ_{1,2}B| in |λx.E′|) (let^{∗} |δ_{2,3}B| in |V′|)
= let^{∗} |δ_{1,2}B| in let^{∗} |δ_{2,3}B| in (λx.|E′|) |V′|
=^{[β_{v}]} let^{∗} |δ_{1,3}B| in |E′|{V′/x}
=^{i.h.} let^{∗} |δ_{1,3}B| in let^{∗} |δ_{3,4}B| in V ≡ let^{∗} |δ_{1,4}B| in V.

Case [if-tt]: |if E_{1} E_{2} E_{3}| ≡ if |E_{1}| |E_{2}| |E_{3}| =^{i.h.} if (let^{∗} |δ_{1,2}B| in tt) |E_{2}| |E_{3}| = let^{∗} |δ_{1,2}B| in (if tt |E_{2}| |E_{3}|) = let^{∗} |δ_{1,2}B| in |E_{2}| =^{i.h.} let^{∗} |δ_{1,2}B| in let^{∗} |δ_{2,3}B| in |V | ≡ let^{∗} |δ_{1,3}B| in |V |.

Case [fix]: |fix E| ≡ fix |E| =^{i.h.} fix (let^{∗} |δ_{1,2}B| in |λx.E′|) = let^{∗} |δ_{1,2}B| in fix (λx.|E′|) = let^{∗} |δ_{1,2}B| in |E′|{fix (λx.|E′|)/x} =^{i.h.} let^{∗} |δ_{1,2}B| in let^{∗} |δ_{2,3}B| in |V | ≡ let^{∗} |δ_{1,3}B| in |V |.

Case [if-ff],[⊗]: Simple; similar to the case of Rule ([if-tt]).

Case [\underline{lift}],[\underline{var}],[\underline{cst}]: Trivial.

Case [\underline{lam}]: Δ; B ⊳ |\underline{λ}x.E| ≡ λx.|E| ∼_{α} λy.|E\{y/x\}| =^{i.h.} λy.(let^{∗} |B′| in |O|) ≡ let^{∗} |[B − B]| in |λy.(let^{∗} B′ in O)|.

For this step we use the induction hypothesis; we also apply the congruence for λ-abstractions.

Case [\underline{app}]: |E_{1}\underline{@}E_{2}| ≡ |E_{1}| |E_{2}| =^{i.h.} (let^{∗} |δ_{1,2}B| in |O_{1}|) (let^{∗} |δ_{2,3}B| in |O_{2}|) = let^{∗} |δ_{1,2}B| in let^{∗} |δ_{2,3}B| in |O_{1}| |O_{2}| ≡ let^{∗} |δ_{1,3}B| in |O_{1}\underline{@}O_{2}|.

Case [\underline{let}]: |\underline{let} x ⇐ E_{1} \underline{in} E_{2}| ≡ let x ⇐ |E_{1}| in |E_{2}| ∼_{α} let y ⇐ |E_{1}| in |E_{2}\{y/x\}| =^{i.h.} let y ⇐ (let^{∗} |B′ − B| in |O_{1}|) in (let^{∗} |B′′| in |O_{2}|) = let^{∗} |B′ − B| in let y ⇐ |O_{1}| in (let^{∗} |B′′| in |O_{2}|).

Case [#]: |#E| = |E| =^{i.h.} let^{∗} |B′ − B| in |O| = let^{∗} |B′ − B| in let x ⇐ |O| in x = let^{∗} |[B′, x : σ = O] − B| in |x|.

Lemma 4.5 has the following immediate corollary for complete programs.

Theorem 4.6 (Annotation erasure for complete programs). If vPCF^{2} ⊢ ⊳E : e ◯σ and vPCF^{2} ⊢ E ↘ O, then vPCF ⊢ ⊳ |E| = |O| : σ.

Proof. Assume that ⊳E : e ◯σ and E ↘ O. That is, ⊳[·]E ⇓ [B]O′ where O ≡ let^{∗} B in O′). By Lemma 4.5, we have ⊳ |E| = let^{∗} |B| in |O′| ≡ |O| : σ.

C.4 Native implementation

C.4.1 A more “realistic” language: ⟨v⟩PCF^{2}

The semantics of vPCF^{2} could re-evaluate values of code types—though such reevaluation does not change the result. Consider, for example, the evaluation of the term (λx.x) (\underline{print}\underline{@}($_{int}1 + 2)). The semantics first evaluates the argument to the code value \underline{print}\underline{@}($_{int}3), then proceeds to evaluate x\{\underline{print}\underline{@}($_{int}3)/x\} ≡ \underline{print}\underline{@}($_{int}3), which needs a complete recursive descent though it is already a value. Such re-evaluation does not change the semantics, but it nevertheless is less efficient, and does not model the actual implementation.

To establish a native implementation, we thus consider a variant of vPCF^{2}, ⟨v⟩PCF^{2}, which marks evaluated terms with angle brackets and prevents them from re-evaluation.^{12} The detailed changes of ⟨v⟩PCF^{2} over vPCF^{2} are given in Syntax

12The reader might notice that angle brackets here have a similar functionality to quote in Lisp and Scheme. But they serve two different purposes: angle brackets here prevent re-evaluation at the semantics level, thereby removing an artifact of the substitution-based semantics and bringing the semantics closer to the actual implementation; quote in Lisp

Raw terms E ::= ... | ⟨O⟩
Values  V ::= ℓ | λx.E | ⟨O⟩

Typing Judgment Add the following rule

(Dynamic)

[eval’d] \frac{Γ ⊳ O : τ}{Γ ⊳ ⟨O⟩ : τ}

Evaluation Semantics The dynamic part is replaced by the following rules.

[eval’d] \overline{⟨O⟩ ⇓ ⟨O⟩} [\underline{lift}] \frac{E ⇓ ℓ}{$_{b}E ⇓ ⟨$_{b}ℓ⟩} [\underline{var}] \overline{x ⇓ ⟨x⟩} [\underline{cst}] \overline{\underline{d} ⇓ ⟨\underline{d}⟩}

[\underline{lam}] \frac{Δ, y : σ; B ⊳ [·]E\{y/x\} ⇓ [B′]⟨O⟩ y ∉ dom B ∪ dom Δ}{Δ ⊳ [B]\underline{λ}x.E ⇓ [B]⟨\underline{λ}y.\underline{let}^{∗} B′ \underline{in} O⟩}

[\underline{app}] \frac{E_{1} ⇓ ⟨O_{1}⟩ E_{2} ⇓ ⟨O_{2}⟩}{E_{1}\underline{@}E_{2} ⇓ ⟨O_{1}\underline{@}O_{2}⟩}

[\underline{let}] \frac{\begin{matrix}Δ ⊳ [B]E_{1} ⇓ [B′]⟨O_{1}⟩ Δ, y : σ; B ⊳ [·]E_{2}\{y/x\} ⇓ [B′′]⟨O_{2}⟩ \\ y ∉ dom B′ ∪ dom Δ \end{matrix}}{Δ ⊳ [B]\underline{let} y ⇐ E_{1} \underline{in} E_{2} ⇓ [B′]⟨\underline{let} x ⇐ O_{1} \underline{in} (\underline{let}^{∗} B′′ \underline{in} O_{2})⟩}

[#] \frac{Δ ⊳ [B]E ⇓ [B′]⟨O⟩ x ∉ dom B′ ∪ dom Δ}{Δ ⊳ [B]#E ⇓ [B′, x : σ = O]⟨x⟩}

Figure 15: Changes of ⟨v⟩PCF^{2} over vPCF^{2}

Figure 15. Note that binders consist of only already evaluated terms, so there is no need to mark them with angle brackets.

The two languages vPCF^{2} and ⟨v⟩PCF^{2} are effectively equivalent, through the following operation to remove the angle brackets in ⟨v⟩PCF^{2}-terms:

Definition C.15 (Unbracketing). The unbracketing of an ⟨v⟩PCF^{2}-term E, noted as unbr(E), is the vPCF^{2}-term resulted from E by removing all the angle brackets in it, i.e., unbr(⟨E⟩) ≡ E and all other constructs are translated homomorphically. We have that ⟨v⟩PCF^{2} ⊢ Γ ⊳ E : τ implies ⟨v⟩PCF^{2} ⊢ Γ ⊳ unbr(E) : τ.

Theorem C.16 (Equivalence of vPCF^{2} and ⟨v⟩PCF^{2}).

1. If vPCF^{2} ⊢ Δ ⊳ [B]unbr(E) ⇓ [B′]V′, then there exists a ⟨v⟩PCF^{2}-value V such that ⟨v⟩PCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V and unbr(V) ≡ V′.

allows programmers to distinguish data from the surrounding programs. A similar concern arises when implementing, e.g., syntactic theories.

2. If ⟨v⟩PCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V, then it also holds that vPCF^{2} ⊢ Δ ⊳ [B]unbr(E) ⇓ [B′]unbr(V).

Proof. Simple induction.

Corollary C.17. If ⟨v⟩PCF^{2} ⊢ Δ ⊳ E : e ◯σ, and ⟨v⟩PCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V, then V is of the form ⟨O⟩.

Proof. By Theorem C.16, we have vPCF^{2} ⊢ Δ ⊳ [B]unbr(E) ⇓ [B′]unbr(V). Using the type preservation of vPCF^{2}, we have unbr(V) is of the form O. Since V is a ⟨v⟩PCF^{2}-value, it must be ⟨O⟩.

Note that every vPCF^{2}-term E is also a ⟨v⟩PCF^{2}-term, and unbr(E) ≡ E. Thus, to evaluate a closed vPCF^{2}-term E of type e ◯σ (i.e., vPCF^{2} ⊢ ⊳E : e ◯σ), we can evaluate E using ⟨v⟩PCF^{2} semantics. Either the evaluation does not terminate, which implies, by Theorem C.16(1), that the evaluation E in vPCF^{2} semantics does not terminate. Or ⟨v⟩PCF^{2} ⊢ E ↘ ⟨O⟩ (defined appropriately using Corollary C.17), which, by Theorem C.16(2), implies that vPCF^{2} ⊢ E ↘ O.

Now that we have established the equivalence of vPCF^{2} and ⟨v⟩PCF^{2}, it suffices to give a native implementation of ⟨v⟩PCF^{2}. In the rest of the section, we will only work with ⟨v⟩PCF^{2} and leave it (instead of vPCF^{2}) implicit whenever possible.

C.4.2 The implementation language: vPCF^{Λ,𝔰𝔱}

Here we present the implementation language vPCF^{Λ,𝔰𝔱}, which can be viewed as a subset of Standard ML [33]. In detail, vPCF^{Λ,𝔰𝔱} is vPCF with dynamic constants removed, and enriched with a global state and an inductive type Λ for representing ⟨v⟩PCF^{2} code types.

Λ = VAR of int | LIT_{b} of b | CST of const | LAM of int × Λ
| APP of Λ × Λ | LET of int × Λ × Λ

For the state, we only model the part in which we are interested. A state S thus consists of a cell n for keeping the counter of name generation, and a cell B for keeping the accumulated bindings: S = ⟨n, B⟩. We also use three specialized primitives (they can be implemented using SML operations := (set) and ! (get), as shown in Figure 16): genvar() generates a new variable name using the counter; addBind(E : Λ) : Λ adds a binding x = E to the accumulated bindings such that x is a newly generated name, and returns the variable x; finally letBind(E : Λ) creates a dynamic local scope for accumulating bindings during the evaluation of term E, and inserts the accumulated bindings after the evaluation of E. The three primitives are governed by the following typing rules. The evaluation semantics of vPCF^{Λ,𝔰𝔱} is given in Figure 17.

Γ ⊳ genvar() : int \frac{Γ ⊳ E : Λ}{Γ ⊳ addBind(E) : Λ}

\frac{Γ ⊳ E : Λ}{Γ ⊳ letBind(E) : Λ}

val n : int ref = ref 0 (∗ name generation counter ∗)

   val B : (int * exp) list ref = ref []  (∗ accumulated bindings ∗)

fun init () = n := 0 (∗ reset the counter ∗)

   fun genvar () =  (∗ genvar() ∗)
       !n  before n := ! n + 1
   fun letBind e_thunk =  (∗ letBind(E) ≡letBind (fn () => E) ∗)
       let val b = ! B  before B := []
           val r = e_thunk ()
           fun genLet [] body =
               body
             | genLet ((x, e) :: rest) body =
               genLet rest (LET(x, e, body))
       in
           genLet (! B) r  before B := b
       end
   fun addBind e =  (∗ addBind(E) ≡addBind(E) ∗)
       let val name = genvar () in
           (B := (name, e) :: ! B); (VAR name)
       end

Figure 16: ML implementation of vPCF^{Λ,𝔰𝔱}-primitives

C.4.3 Native embedding

Definition C.18 (Embedding translation {|−|}_{vϵ} of ⟨v⟩PCF^{2} into vPCF^{Λ,𝔰𝔱}).

⟨v⟩PCF^{2} ⊢ Γ ⊳ E : τ ⟹ vPCF^{Λ,𝔰𝔱} ⊢ {|Γ|}_{vϵ} ⊳ {|E|}_{vϵ} : {|τ|}_{vϵ}

Types : {|e ◯σ|}_{vϵ} = {|v ◯σ|}_{vϵ} = Λ, {|b|}_{vϵ} = b, {|τ_{1} → τ_{2}|}_{vϵ} = {|τ_{1}|}_{vϵ} → {|τ_{2}|}_{vϵ}
Terms : \{|$_{b}E|\}_{vϵ} = LIT_{b}(\{|E|\}_{vϵ}), \{|\underline{d}|\}_{vϵ} = CST(⟅d⟆), \{|\underline{λ}x.E|\}_{vϵ} = \underline{λ}^{vϵ}λx.\{|E|\}_{vϵ},
\{|E_{1}\underline{@}E_{2}|\}_{vϵ} = APP(\{|E_{1}|\}_{vϵ}, \{|E_{2}|\}_{vϵ}), \{|#E|\}_{vϵ} = \underline{#}^{vϵ}(\{|E|\}_{vϵ}),
\{|\underline{let} x ⇐ E_{1} \underline{in} E_{2}|\}_{vϵ} = \underline{let}^{vϵ}\{|E_{1}|\}_{vϵ}λx.\{|E_{2}|\}_{vϵ}, \{|⟨O⟩|\}_{vϵ} = \{|O|\}_{⟨⟩ϵ}

“Evaluated” terms:

\{|$_{b}ℓ|\}_{⟨⟩ϵ} = LIT_{b}(ℓ), \{|v_{i}|\}_{⟨⟩ϵ} = VAR(i), \{|\underline{λ}v_{i}.O|\}_{⟨⟩ϵ} = LAM(i, \{|O|\}_{⟨⟩ϵ}),

\{|O_{1}\underline{@}O_{2}|\}_{⟨⟩ϵ} = APP(\{|O_{1}|\}_{⟨⟩ϵ}, \{|O_{2}|\}_{⟨⟩ϵ}), \{|\underline{d}|\}_{⟨⟩ϵ} = CST(⟅d⟆),
\{|\underline{let} v_{i} ⇐ O_{1} \underline{in} O_{2}|\}_{⟨⟩ϵ} = LET(i, \{|O_{1}|\}_{⟨⟩ϵ}, \{|O_{2}|\}_{⟨⟩ϵ})

Bindings:

{|·|}_{vϵ} = nil
{|B, v_{i} : σ = O|}_{vϵ} = (i, {|O|}_{⟨⟩ϵ}) :: {|B|}_{vϵ}

where we use the following terms:

\underline{λ}^{vϵ} ≡ λf.let i ⇐ genvar() in LAM(i, letBind(f (VAR(i))))
\underline{let}^{vϵ} ≡ λe.λf.let i ⇐ genvar() in LET(i, e, letBind(f (VAR(i))))
\underline{#}^{vϵ} ≡ λe.addBind(e)

Note that the embedding translation is partial: among “evaluated” terms

State  S ::= ⟨n, B⟩  (n ∈ ℕ)
Bindings B ::= nil | (n, V) :: B  (n ∈ ℕ)

Judgment Form vPCF^{Λ,𝔰𝔱} ⊢ E, S ⇓ V, S′ We use the following abbreviations.

\frac{E_{1} ⇓ V_{1} … E_{n} ⇓ V_{n}}{E ⇓ V}

≡ \frac{E_{1}, S_{1} ⇓ V_{1}, S_{2} … E_{n}, S_{n} ⇓ V_{n}, S_{n+1}}{E, S_{1} ⇓ V, S_{n+1}}

\underline{LET}^{∗} (n_{1}, V_{1}) :: …:: (n_{m}, V_{m}) :: nil \underline{in} V ≡ LET(n_{m}, V_{m}, … LET(n_{1}, V_{1}, V) …)

(Core)

[app] \frac{E_{1} ⇓ λx.E′ E_{2} ⇓ V′ E′\{V′/x\} ⇓ V}{E_{1} E_{2} ⇓ V} [if-tt] \frac{E_{1} ⇓ tt E_{2} ⇓ V}{if E_{1} E_{2} E_{3} ⇓ V}
[if-ff] \frac{E_{1} ⇓ ff E_{3} ⇓ V}{if E_{1} E_{2} E_{3} ⇓ V} [fix] \frac{E ⇓ λx.E′ E′\{fix (λx.E′)/x\} ⇓ V}{fix E ⇓ V}

[⊗] \frac{E_{1} ⇓ V_{1} E_{2} ⇓ V_{2}}{E_{1} ⊗ E_{2} ⇓ V} (V_{1} ⊗ V_{2} = V)

(Term and State)

[cons] \frac{E_{1} ⇓ V_{1} … E_{n} ⇓ V_{n}}{c(E_{1}, …, E_{n}) ⇓ c(V_{1}, …, V_{n})}(c ∈ \{VAR, LIT_{b}, CST, LAM, APP, LET\})

[genvar] \overline{genvar(), ⟨n, B⟩ ⇓ n, ⟨n + 1, B⟩}
[addBind] \frac{E, S ⇓ V, ⟨n, B⟩}{addBind(E), S ⇓ VAR(n), ⟨n + 1, (n, V) :: B⟩}
[letbind] \frac{E, ⟨n, nil⟩ ⇓ V, ⟨n′, B′⟩}{letBind(E), ⟨n, B⟩ ⇓ \underline{LET}^{∗} B′ \underline{in} V, ⟨n′, B⟩}

Figure 17: The evaluation semantics of vPCF^{Λ,𝔰𝔱} (i.e., those enclosed in angle brackets), only those whose variables (both free and bound) range in the set {v_{i} : i ∈ Z} have a translation. A ⟨v⟩PCF^{2}-term is vϵ-embeddable if all its “evaluated” subterms satisfy this condition. Clearly, all vPCF^{2}-terms, viewed as ⟨v⟩PCF^{2}-terms, are without “evaluated” subterms and thus vϵ-embeddable. In the following, when we write {|E|}_{vϵ}, we implicitly state that E is vϵ-embeddable.

Note also that α-conversion is not preserved by the embedding translation: bound variables v_{i} are translated to integer i under the translation for the “evaluated” terms. As a consequence, a general substitution lemma of the following form fails for this translation.

{|E{E′/x}|}_{vϵ} ∼_{α} {|E|}_{vϵ}{{|E′|}_{vϵ}/x}

The problem occurs when the capture-free substitution goes under a dynamic λabstraction inside an “evaluated” term, which possibly requires the renaming of the bound variable. For example, the substitution ⟨\underline{λ}v_{1}.x\underline{@}v_{1}⟩\{⟨v_{1}⟩/x\} should rename the bound variable v_{1} and yield ⟨\underline{λ}v_{2}.v_{1}\underline{@}v_{2}⟩: the substitution of the translated terms, \{|⟨\underline{λ}v_{1}.x\underline{@}v_{1}⟩|\}_{vϵ}\{\{|⟨v_{1}⟩|\}_{vϵ}/x\} ≡ LAM(1, APP(VAR(1), VAR(1))), is different from the translation of the substitution LAM(2, APP(VAR(1), VAR(2))).

Fortunately, such problematic substitutions do not actually occur in an evaluation. Intuitively, all variables occurring inside an evaluated term are already generated, and thus not amenable to substitution. This intuition is captured by the following well-formedness condition.

Definition C.19 (Well-formed ⟨v⟩PCF^{2}-terms). A ⟨v⟩PCF^{2}-term E is wellformed, if for all its “evaluated” subterms ⟨O⟩, no free variable in O is bound by a static or dynamic λ-abstraction.

The class of well-formed terms is closed under evaluation. It includes all the vPCF^{2}-terms.

Lemma C.20. If λx.E and E′ are both well-formed, then so is E{E′/x}.

Lemma C.21. If E is well formed and [B]E ⇓ [B′]E′, then all terms occurring in its derivation, which include E′, are well formed.

Proof. By induction on the derivation. We use the previous lemma for function application.

For well-formed terms, capture-free substitution used in the β-reduction has a substitution lemma.

Lemma C.22 (Substitution lemma for well-formed terms). If λx.E is well-formed, then {|E{E′/x}|}_{vϵ} ≡ {|E|}_{vϵ}{{|E′|}_{vϵ}/x}.^{13} Proof. By the definition of a well-form term, x does not appear inside any “evaluated” subterms of E. Now we proceed by induction. In particular, for the case of ⟨O⟩, we have ⟨O⟩{E′/x} ≡ ⟨O⟩; and for the case of λy.E′, renaming y does not affect variable names that appear inside the evaluated terms, again by the definition of a well-formed term.

13Here, strict syntactic equality is possible, because we are free to pick a representative from the α-equivalent class formed by the possible results of the substitution.

The correctness proof of the native embedding also uses a few other notations.

• We write V_{I} for the set of variable names indexed by set I, where I is a subset of the integer set Z, i.e., V_{I} = {v_{i} : i ∈ I}.

• We write [n] for the set {0, 1, …, n − 1}.

• For ⟨v⟩PCF^{2} ⊢ v ◯Δ ⊳ E : τ where dom Δ ⊆ V_{Z}, we write {|E|}_{vϵ}^{C} (“closed embedding translation”) for the term {|E|}_{vϵ}{Φ^{C}} where the substitution Φ^{C} = {VAR(i)/v_{i} : i ∈ Z}. It is clear that the resulting term must be closed.

We are ready to prove the correctness of the native embedding. We first prove the soundness of the implementation (that its evaluation gives a correct result whenever it terminates), and then prove the completeness of the implementation (that its evaluation must terminate if the source program terminates according to the ⟨v⟩PCF^{2}-semantics). As for the notation, we write iV for the iimplementation of a value V.

Lemma C.23 (Soundness of the Implementation). If

(a) v ◯Δ ⊳ [B]E : τ where dom Δ ∪ dom B ⊆ V_{[n]},

(b) E is well-formed, and

(c) vPCF^{Λ,𝔰𝔱} ⊢ {|E|}_{vϵ}^{C}, S ⇓ iV , S′ where S = ⟨n, {|B|}_{vϵ}^{C}⟩,

then there exist a ⟨v⟩PCF^{2}-value V, a ⟨v⟩PCF^{2}-binding B′, and an integer n′ ≥ n such that

• ⟨v⟩PCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V,

• S′ = ⟨n′, {|B′|}_{vϵ}^{C}⟩, iV = {|V |}_{vϵ}^{C}, and

• dom Δ ∪ dom B′ ⊆ V_{[n′]}.

Proof. By induction on the derivation of vPCF^{Λ,𝔰𝔱} ⊢ {|E|}_{vϵ}^{C}, S ⇓ iV , S′ (Condition (c)). It is a routine task to ensure Condition (a) during the induction. To ensure Condition (b) during the induction, we use Lemma C.21.

We perform a case analysis on E.

Case E ≡ ℓ: Simple.

Case E ≡ ⟨O⟩: Since {|⟨O⟩|}_{vϵ}^{C} must be a value already (a simple inductive proof), we have, by inversion, that iV ≡ {|⟨O⟩|}_{vϵ}^{C} and S′ = S. Therefore, we put B′ = B, V = ⟨O⟩ and n′ = n: ⟨O⟩ ⇓ ⟨O⟩.

Case E ≡ v_{i}: Since {|v_{i}|}_{vϵ}^{C} ≡ VAR(i) is a value, we have that iV ≡ VAR(i) and S′ = S. We can put B′ = B, V = ⟨v_{i}⟩, and n′ = n: v_{i} ⇓ ⟨v_{i}⟩.

Case E ≡ λx.E′: Since {|λx.E′|}_{vϵ}^{C} ≡ λx.{|E′|}_{vϵ}^{C} is a value, we have that iV ≡ λx.{|E′|}_{vϵ}^{C} and S′ = S. We can put B′ = B, V = λx.E′, and n′ = n: λx.E′ ⇓ λx.E′.

Case E ≡ E_{1} E_{2}: We have that {|E_{1} E_{2}|}_{vϵ}^{C} ≡ {|E_{1}|}_{vϵ}^{C} {|E_{2}|}_{vϵ}^{C}. By inversion, the last step in the derivation of vPCF^{Λ,𝔰𝔱} ⊢ {|E_{1}|}_{vϵ}^{C} {|E_{2}|}_{vϵ}^{C}, S ⇓ iV , S′ must be of the following form (let S_{1} = S and S_{4} = S′).

\frac{\{|E_{1}|\}_{vϵ}^{C}, S_{1} ⇓ λx.iE′, S_{2} \{|E_{2}|\}_{vϵ}^{C}, S_{2} ⇓ iV′, S_{3} iE′\{iV′/x\}, S_{3} ⇓ iV , S_{4}}{\{|E_{1}|\}_{vϵ}^{C} \{|E_{2}|\}_{vϵ}^{C}, S_{1} ⇓ iV , S_{4}}

where S_{1} = ⟨n, {|B|}_{vϵ}^{C}⟩. We have the following reasoning:

(1) By induction hypothesis 1 (and by the fact that only λ-abstractions translates to λ-abstractions under the vϵ-translation), there exist B_{2}, E′, and n_{2} such that

a. Δ ⊳ [B]E_{1} ⇓ [B_{2}]λx.E′, {|E′|}_{vϵ}^{C} = iE′; and

b. n_{2} ≥ n, S_{2} = ⟨n_{2}, {|B_{2}|}_{vϵ}^{C}⟩, dom Δ ∪ dom B_{2} ⊆ V_{[n_{2}]}.

(2) By induction hypothesis 2 and (1.b), there exist B_{3}, V′, and n_{3} such that

a. Δ ⊳ [B_{2}]E_{2} ⇓ [B_{3}]V′, {|V′|}_{vϵ}^{C} = iV′; and

b. n_{3} ≥ n_{2}, S_{3} = ⟨n_{3}, {|B_{3}|}_{vϵ}^{C}⟩, dom Δ ∪ dom B_{3} ⊆ V_{[n_{3}]}.

(3) By Lemma C.21, λx.E′ is well-formed, thus by Lemma C.22, we have

\begin{aligned}iE′\{iV′/x\} & ≡ & \{|E′|\}_{vϵ}^{C}\{\{|V′|\}_{vϵ}^{C}/x\} \\ & ≡ & \{|E′\{V′/x\}|\}_{vϵ}^{C} \end{aligned}

(4) By (2), (3), and induction hypothesis 3, there exist B_{4}, V, and n_{4} such that

a. Δ ⊳ [B_{3}]E′{V′/x} ⇓ [B_{4}]V, {|V |}_{vϵ}^{C} = iV ; and

b. n_{4} ≥ n_{3}, S_{4} = ⟨n_{4}, {|B_{4}|}_{vϵ}^{C}⟩, dom Δ ∪ dom B_{4} ⊆ V_{[n_{4}]}.

Finally, one application of the ⟨v⟩PCF^{2} evaluation rule ([app]) to (1.a), (2.a), and (4.a) yields: Δ ⊳ [B_{1}]E_{1} E_{2} ⇓ [B_{4}]V.

Case E ≡ fix E_{1}: We have that {|fix E_{1}|}_{vϵ}^{C} ≡ fix {|E_{1}|}_{vϵ}^{C}. By inversion, the derivation ends with

\frac{\{|E_{1}|\}_{vϵ}^{C}, S_{1} ⇓ λx.iE′, S_{2} iE′\{fix λx.iE′/x\}, S_{2} ⇓ iV , S_{3}}{fix \{|E_{1}|\}_{vϵ}^{C}, S_{1} ⇓ iV , S_{3}}

where S_{1} = ⟨n, {|B|}_{vϵ}^{C}⟩. Then we reason as follows:

(1) By induction hypothesis 1 (and by the fact that only λ-abstractions translate to λ-abstractions under the vϵ-translation), there exist B_{2}, E′, and n_{2} such that

a. Δ ⊳ [B]E_{1} ⇓ [B_{2}]λx.E′, {|E′|}_{vϵ}^{C} = iE′; and

b. n_{2} ≥ n, S_{2} = ⟨n_{2}, {|B_{2}|}_{vϵ}^{C}⟩, dom Δ ∪ dom B_{2} ⊆ V_{[n_{2}]}.

(2) Applying Lemma C.21 to (1.a) gives that λx.E′ is well-formed, and thus by Lemma C.22, we have

iE′{fix λx.iE′/x} ≡ {|E′|}_{vϵ}^{C}{{|fix λx.E′|}_{vϵ}^{C}/x}
≡ {|E′{fix λx.E′/x}|}_{vϵ}^{C}

(3) By (2) and induction hypothesis 2, there exist B_{3}, V, and n_{3} such that

a. Δ ⊳ [B_{2}]E′{fix λx.E′/x} ⇓ [B_{3}]V, {|V |}_{vϵ}^{C} = iV ; and

b. n_{3} ≥ n_{2}, S_{3} = ⟨n_{3}, {|B_{3}|}_{vϵ}^{C}⟩, dom Δ ∪ dom B_{3} ⊆ V_{[n_{3}]}.

Finally, one application of the evaluation rule ([fix]) to (1.a) and (3.a) yields: Δ ⊳ [B_{1}]fix E_{1} ⇓ [B_{3}]V.

Case E ≡ if E_{1} E_{2} E_{3} or E ≡ E_{1} ⊗ E_{2}: Similar to the proofs for E_{1} E_{2} and for fix E_{1}, and only simpler, since these cases are free of the complication introduced by capture-free substitution.

Case E ≡ $_{b}E_{1}, E ≡ E_{1}\underline{@}E_{2}, or E ≡ \underline{d}: Simple.

Case E ≡ \underline{λ}x.E_{1}: We have \{|\underline{λ}x.E_{1}|\}_{vϵ}^{C} ≡ \underline{λ}^{vϵ} ((λx.\{|E_{1}|\}_{vϵ})\{Φ^{C}\}). By a few inversions from vPCF^{Λ,𝔰𝔱} ⊢ \{|\underline{λ}x.E_{1}|\}_{vϵ}^{C}, ⟨n, \{|B|\}_{vϵ}^{C}⟩ ⇓ iV , S′, we have the following two immediate subderivations (omitting some trivial branches)

genvar(), ⟨n, {|B|}_{vϵ}^{C}⟩ ⇓ n, ⟨n + 1, {|B|}_{vϵ}^{C}⟩

\frac{\frac{\frac{\{|E_{1}|\}_{vϵ}\{VAR(n)/x\}\{Φ^{C}\}, ⟨n + 1, nil⟩ ⇓ iV′, ⟨n′, iB′⟩}{((λx.\{|E_{1}|\}_{vϵ})\{Φ^{C}\}) (VAR(n)), ⟨n + 1, nil⟩ ⇓ iV′, ⟨n′, iB′⟩}}{L, ⟨n + 1, \{|B|\}_{vϵ}^{C}⟩ ⇓ \underline{LET}^{∗} iB′ \underline{in} iV′, ⟨n′, \{|B|\}_{vϵ}^{C}⟩}}{LAM(n, L), ⟨n + 1, \{|B|\}_{vϵ}^{C}⟩ ⇓ LAM(n, \underline{LET}^{∗} iB′ \underline{in} iV′), ⟨n′, \{|B|\}_{vϵ}^{C}⟩}

where L ≡ letBind(((λx.{|E_{1}|}_{vϵ}){Φ^{C}}) (VAR(n))).

Note that

{|E_{1}|}_{vϵ}{VAR(n)/x}{Φ^{C}} ≡ {|E_{1}{v_{n}/x}|}_{vϵ}{VAR(n)/v_{n}}{Φ^{C}} ≡ {|E_{1}{v_{n}/x}|}_{vϵ}{Φ^{C}}

(the second equality follows from the definition of Φ^{C}). From v ◯Δ ⊳ [B]\underline{λ}x.E_{1} : e ◯(σ_{1} → σ_{2}) and dom Δ ∪ dom B ⊆ V_{[n]}, it follows that v ◯{Δ, v_{n} : σ_{1}; B} ⊳ E_{1}{v_{n}/x} : v ◯σ_{2} and dom(Δ, v_{n} : σ_{1}) ∪ dom B ⊆ V_{[n+1]}. Furthermore, E_{1}{v_{n}/x} is clearly well-formed. Thus, by induction hypothesis, there exist B′′ and V′′ such that

a. Δ, v_{n} : σ_{1}; B⊳[·]E_{1}{v_{n}/x} ⇓ [B′]V′′ and {|V′′|}_{vϵ}^{C} = iV′. Type Preservation shows that V′′ ≡ ⟨O⟩ for some O; and

b. iB′ = {|B′|}_{vϵ}^{C}, dom Δ ∪ dom B′ ⊆ V_{[n′]}, and n′ ≥ n + 1.

Finally, put V = ⟨\underline{λ}v_{n}.\underline{let}^{∗} B′′ \underline{in} O⟩ and B′ = B, and apply the evaluation rule ([\underline{lam}]) to (a). Noting that v_{n} ∉ V_{[n]} ⊇ dom Δ ∪ dom B, we have that Δ ⊳ [B]E_{1} : [B]V. It is easy to check that \{|V |\}_{vϵ} ≡ LAM(n, \underline{LET}^{∗} iB′ \underline{in} iV′).

Case E ≡ \underline{let} x ⇐ E_{1} \underline{in} E_{2}: Similar to the case of \underline{λ}x.E_{1}.

Case E ≡ #E_{1}: By inversion on the assumption, the derivation ends with

\frac{\{|E_{1}|\}_{vϵ}^{C}, S_{1} ⇓ iV′, S_{2} addBind(iV′), S_{2} ⇓ iV , S′}{\underline{#}^{vϵ} \{|E_{1}|\}_{vϵ}^{C}, S_{1} ⇓ iV , S′}

where S_{1} = ⟨n, {|B|}_{vϵ}^{C}⟩. Then we reason as follows.

(1) By induction hypothesis 1, there exist B_{2}, V′, and n_{2} such that

a. Δ ⊳ [B]E_{1} ⇓ [B_{2}]V′ and {|V′|}_{vϵ}^{C} = iV′. By type preservation, V′ ≡ ⟨O⟩ for some O; and

b. n_{2} ≥ n, S_{2} = ⟨n_{2}, {|B_{2}|}_{vϵ}^{C}⟩, and dom Δ ∪ dom B_{2} ⊆ V_{[n_{2}]}.

(2) Inverting the second premise, we have that iV = VAR(n_{2}), and S′ = ⟨n_{2} + 1, (n_{2}, iV′) :: {|B_{2}|}_{vϵ}^{C}⟩. We can put V ≡ ⟨v_{n_{2}}⟩, B′ ≡ (B_{2}, v_{n_{2}+1} : σ = O), and n′ ≡ n_{2} +1; it is easy to check that {|V |}_{vϵ}^{C} = iV and ⟨n′, {|B′|}_{vϵ}^{C}⟩ = S′. Note also that v_{n_{2}} ∉ V_{[n_{2}]} ⊇ dom Δ ∪ dom B_{2}. Now we can apply the rule ([#]) to get the result.

Lemma C.24 (Completeness of the Implementation). If

(a) v ◯Δ ⊳ [B]E : τ where dom Δ ∪ dom B ⊆ V_{[n]},

(b) E is well-formed, and

(c) ⟨v⟩PCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B_{2}]V, then there exist B′_{2}, V′, and n′ ≥ n such that

• ⟨v⟩PCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′_{2}]V′,

• vPCF^{Λ,𝔰𝔱} ⊢ {|E|}_{vϵ}^{C}, ⟨n, {|B|}_{vϵ}^{C}⟩ ⇓ V′, ⟨n′, {|B′_{2}|}_{vϵ}^{C}⟩, and

• dom Δ ∪ dom B′ ⊆ V_{[n′]}.

Proof. By induction on the height of the derivation of ⟨v⟩PCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B_{2}]V (Condition (c)). It is a routine task to ensure Condition (a) during the induction. To ensure Condition (b) during the induction, we use Lemma C.21.

We perform case analysis on the last rule used in the derivation.

Case [lit], [lam]: Simple.

Case [app]: We combine the induction hypotheses and Lemma C.22.

Case [fix]: We combine the induction hypotheses and Lemma C.22.

Case [if-tt], [if-ff], [⊗]: We combine the induction hypotheses, and use the fact that constants of base types translate to themselves.

Case [eval’d], [\underline{lift}], [\underline{var}], [\underline{cst}], [\underline{app}]: Simple. See also the corresponding cases in the soundness proof (Lemma C.23).

Case [\underline{lam}]: The derivation tree takes the following form

\frac{\begin{matrix}D \\ Δ, y : σ; B ⊳ [·]E\{y/x\} ⇓ [B′]⟨O⟩ y ∉ dom B ∪ dom Δ \end{matrix}}{Δ ⊳ [B]\underline{λ}x.E ⇓ [B]⟨\underline{λ}y.\underline{let}^{∗} B′ \underline{in} O⟩}

Since v_{n} ∉ dom Δ ∪ dom B, we have

(Δ, y : σ; B ⊳ E{y/x}) ∼_{α} (Δ, v_{n} : σ; B ⊳ E{v_{n}/x}) .

By Theorem C.13, there exist B′′ and O′ such that (Δ, v_{n} : σ; B ⊳ [B′]O) ∼_{α} (Δ′, v_{n} : σ; B ⊳ [B′′]O′) and there is a a derivation for

Δ, v_{n} : σ; B ⊳ [·]E{v_{n}/x} ⇓ [B′′]⟨O′⟩

that has the same size as derivation D. Noting further that E{v_{n}/x} is wellformed, we can apply the induction hypothesis to conclude that ∃B′′′, O′′, n′ ≥ n + 1 such that the following hold.

(1) Δ, v_{n} : σ; B ⊳ [·]E{v_{n}/x} ⇓ [B′′′]⟨O′′⟩. Again, by Theorem C.13, we have that (Δ, v_{n} : σ; B ⊳ [B′′]O′) ∼_{α} (Δ, v_{n} : σ; B ⊳ [B′′′]O′′).

(2) vPCF^{Λ,𝔰𝔱} ⊢ {|E{v_{n}/x}|}_{vϵ}^{C}, ⟨n + 1, nil⟩ ⇓ {|⟨O′′⟩|}_{vϵ}^{C}, ⟨n′, {|B′′′|}_{vϵ}^{C}⟩.

(3) dom Δ ∪ {v_{n}} ∪ dom B′ ⊆ V_{[n′]}. We can then construct derivations for

• ⟨v⟩PCF^{2} ⊢ Δ ⊳ [B]E[B]⟨\underline{let}^{∗} B′′′ \underline{in} O′′⟩ ⇓ , by applying rule ([\underline{lam}]) to (1), and

• vPCF^{Λ,𝔰𝔱} ⊢ \{|\underline{λ}x.E|\}_{vϵ}^{C}, ⟨n, \{|B|\}_{vϵ}^{C}⟩ ⇓ \{|⟨\underline{λ}v_{n}.\underline{let}^{∗} B′′′ \underline{in} O′′⟩|\}_{vϵ}^{C}, ⟨n, \{|B|\}_{vϵ}^{C}⟩, using a derivation in the form appeared in the case E ≡ \underline{λ}x.E_{1} of the soundness proof (Lemma C.23)

The conclusion follows immediately. Case [\underline{let}]: Similar to the case of rule ([\underline{lam}]). Case [#]: We build the derivation from the induction hypothesis. See also the corresponding cases in the soundness proof (Lemma C.23). Definition C.25 (Simulating the evaluation in vPCF^{Λ,𝔰𝔱}). Let vPCF^{2} ⊢ ⊳E : ◯σ. We write simEval(E, t) for a vPCF^{Λ,𝔰𝔱}-term t : Λ, if ∃S′.vPCF^{Λ,𝔰𝔱} ⊢ letBind({|E|}_{vϵ}), ⟨0, nil⟩ ⇓ t, S′. Theorem C.26 (Total correctness). Let vPCF^{2} ⊢ ⊳E : ◯σ.

1. If vPCF^{2} ⊢ E ↘ O for some O, then there is a term O′ such that O′ ∼_{α} O and simEval(E, {|O′|}_{vϵ}).

2. If simEval(E, t) for some t : Λ, then there is a term O such that t ≡ {|O|}_{vϵ}

and vPCF^{2} ⊢ E ↘ O. Proof. We combine Theorem C.16, Lemma C.23, and Lemma C.24.

C.5 Call-by-value type-directed partial evaluation

C.5.1 Semantic correctness Lemma C.27. For all types σ, nPCF ⊢ ⊳ |↓^{σ}| = λx.x : σ → σ and nPCF ⊢ ⊳ |↑_{σ}| = λx.x : σ → σ. Proof. By a straightforward induction on type τ. Theorem C.28 (Semantic correctness of TDPE). If vPCF^{tdpe} ⊢ ⊳E : σ^{𝔡} and vPCF^{2} ⊢ NF (E) ⇓ O, then vPCF ⊢ ⊳ |O| = |E| : σ.

(Note that the two erasures are different: One operates on vPCF^{2}-terms, the other on vPCF^{tdpe}-terms.) Proof. Similar to the proof of the corresponding theorem in the call-by-name case, Theorem 2.12, but using Lemma C.27 and Theorem 4.6 instead.

C.5.2 Syntactic correctness

Theorem 4.8 (Refined type preservation). If vPCF^{2} ⊢ v ◯^{var}(Δ) ▶ [B]E : τ and vPCF^{2} ⊢ Δ ⊳ [B]E ⇓ [B′]V, then vPCF^{2} ⊢ v ◯^{var}(Δ) ▶ [B′]V : τ.

Proof. (Sketch) Similar to the proof of Theorem 4.2. As always, the most nontrivial case is the rule ([app]), for which we prove a substitution lemma for the refined type system (similar to Lemma B.9.)

Corollary 4.9 (Refined type preservation for complete programs). If ▶ E : e ◯^{nc}(σ) and E ↘ O, then ▶ O : e ◯^{nc}(σ).

Theorem 4.10 (Normal-form code types). If V is an vPCF^{2}-value (Figure 8), and vPCF^{2} ⊢ v ◯^{var}(Δ) ▶ V : v ◯^{X}(σ) where X is av, nv, bd, or nc, then V ≡ O for some O and Δ ⊳^{X} |O| : σ.

Proof. Similar to the proof of Theorem 2.14.

Lemma 4.11. (1) The extraction functions (Figure 10c) have the following normal-form types (writing σ^{◯nv} for σ{v ◯^{nv}(b)/b : b ∈ 𝔹}.)

▶ ↓^{σ} : σ^{◯nv} → v ◯^{nv}(σ), ▶ ↑_{σ} : v ◯^{av}(σ) → σ^{◯nv}.

(2) If vPCF^{tdpe} ⊢ Γ ⊳ E : φ, then vPCF^{2} ⊢ {|Γ|}_{ri}^{nv} ▶ {|E|}_{ri} : {|φ|}_{ri}^{nv}, where {|φ|}_{ri}^{nv} = φ{v ◯^{nv}(b)/b^{𝔡} : b ∈ 𝔹}.

Proof.

(1) By induction on type σ.

Case σ = b: Because at the base type, b^{◯nv} = v ◯^{nv}(b), we just need to show: ▶ λx.x : v ◯^{nv}(b) → v ◯^{nv}(b) for ↓^{b}, and ▶ λx.x : v ◯^{av}(b) → v ◯^{nv}(b) for ↑_{b}. This is simple.

Case σ = σ_{1} → σ_{2}: Noting that (σ_{1} → σ_{2})^{◯nv} = σ_{1}^{◯nv} → σ_{2}^{◯nv}, we give the following typing derivations, in the compact style used in the proof of Lemma 2.15.

• For ▶ ↓^{σ_{1}→σ_{2}} : (σ_{1}^{◯nv} → σ_{2}^{◯nv}) → v ◯^{nv}(σ_{1} → σ_{2}):

f : σ_{1}^{◯nv} → σ_{2}^{◯nv}, x : v ◯^{var}(σ_{1}) ▶ \underbrace{↓^{σ_{2}}(\overbrace{f (\underbrace{↑_{σ_{1}}x}_{σ_{1}^{◯nv}})}^{σ_{2}^{◯nv}})}_{v ◯^{nv} (σ_{2})} : e ◯^{nc}(σ_{2})

Note the use of implicit coercions for term x and for ↓^{σ_{2}}(f (↑_{σ_{1}}x)).

• For ▶ ↑_{σ_{1}→σ_{2}} : v ◯^{av}(σ_{1} → σ_{2}) → (σ_{1}^{◯nv} → σ_{2}^{◯nv}):

e : v ◯^{av}(σ_{1} → σ_{2}), x : σ_{1}^{◯nv} ▶ ↑_{σ_{2}}(\underbrace{#(\overbrace{e\underline{@}( \underbrace{↓^{σ_{1}}x}_{v ◯^{nv} (σ_{1})})}^{e ◯^{bd} (σ_{2})})}_{v ◯^{var} (σ_{2})}) : σ_{2}^{◯nv}

(2) By a simple induction on vPCF^{tdpe} ⊢ Γ ⊳ E : φ. For the case where E ≡ d^{𝔡} with Sg(d) = σ, we use the typing of ↑_{σ} from part (1) and the fact that {|σ^{𝔡}|}_{ri}^{nv} ≡ {|σ{b^{𝔡}/b : b ∈ 𝔹}|}_{ri}^{nv} ≡ σ{v ◯^{nv}(b)/b : b ∈ 𝔹} ≡ σ^{◯nv}.

Theorem 4.12. If vPCF^{tdpe} ⊢ ⊳E : σ^{𝔡}, then vPCF^{2} ⊢▶ NF (E) : v ◯^{nv}(σ).

Proof. By Lemma 4.11(2), we have vPCF^{2} ⊢▶ {|E|}_{ri} : {|σ^{𝔡}|}_{ri}^{nv}. Since {|σ^{𝔡}|}_{ri}^{nv} ≡ σ^{◯nv}, applying ↓^{σ} : σ^{◯nv} → v ◯^{nv}(σ) (Lemma 4.11(1)) to {|E|}_{ri} yields the conclusion.

Corollary C.29 (Syntactic correctness of TDPE). For vPCF^{tdpe} ⊢ ⊳E : σ^{𝔡}, if vPCF^{2} ⊢ NF (E) ↘ V, then V ≡ O for some O and vPCF ⊢ Δ⊳^{nc} |O| : σ.

Proof. We use Theorem 4.12, Corollary 4.9, and Theorem 4.10.

D Notation and symbols

Meta-variables and fonts

E  (one-level or two-level) terms
x, y, z  variables
τ (resp. σ)  two-level (resp. one-level) types  {8,9, \atop 22,53}
φ  two-level types in TDPE languages  16,25
θ  substitution-safe types (vPCF^{2})  22
Γ (resp. Δ)  two-level/one-level typing contexts  8,9
B  accumulated bindings  23
b  base types  7
ℓ  literals (constants of base types)  7
d  dynamic constants in signature Sg  8
V  values (canonical terms)  8,23
O  code-typed values  8,23
S  state  59
Sans serif (bool, CST) syntax
Underlined (\underline{λ}x., \underline{@}) dynamic constructs  8,22

d^{𝔡}, b^{𝔡} dynamic constants and base types in TDPE languages

16,25

Language and Judgments

L ⊢ J  judgment J holds in language L.

General judgments

Γ ⊳ E : τ term-in-context: “term E is of type τ

under context Γ”

Γ ⊳ E_{1} = E_{2} : τ equation-in-context: “E_{1} and E_{2} are equal terms of type τ under context Γ”

nPCF^{2}: call-by-name two-level language  8
E ⇓ V  evaluation of a statically closed term  8

Γ ▶ E : τ term-in-context with refined typing for βη-normal object terms

18

nPCF: call-by-name one-level language  9
\begin{matrix}Δ ⊳^{X} E : σ \\ (X ∈ \{at, nf \}) \end{matrix}  typing judgments for βη-normal forms  18

nPCF^{Λ}: CBN language with a term type  12
nPCF^{tdpe} and vPCF^{tdpe}: two-level languages for TDPE  16,25

vΛ and nΛ: pure simply typed λ-calculus  11,34
vPCF^{2} and ⟨v⟩PCF^{2}: call-by-value two-level languages  23,56
Γ ⊳ [B]E : τ  binder-term-in-context  24,46
Γ ⊳ [B]  binder-in-context  46
Γ ⊳ [B] ≥ [B′]  binder extension  46
B − B′  difference of binder B and its prefix B′  46
\begin{matrix}(Γ ⊳ E) ∼_{α} \\ (Γ′ ⊳ E′) \end{matrix}  α-equivalence for terms-in-context  51
\begin{matrix}(Γ ⊳ [B]E) ∼_{α} \\ (Γ′ ⊳ [B′]E′) \end{matrix}  α-equivalence for binder-terms-in-context 51
Γ ⊳ [B]E ⇓ [B′]V evaluation of a binder-term-in-context  23
E ↘ O evaluation of a complete program 24

Γ ▶ E : τ term-in-context with refined typing for λ_{c}-normal object terms

27

vPCF: call-by-value one-language with effects  53

Δ ⊳^{X} E : σ

X = av, nv, bd, nc typing judgments for λ_{c}-normal forms

27

vPCF^{Λ,𝔰𝔱}: CBV language with a term type and state  59
E, S ⇓ V, S′  evaluation  59

General notations

[[−]]  (denotational) meaning function  13,35
{|−|}  syntactic translation
{|−|}_{nϵ} native embedding of nPCF^{2} into nPCF^{Λ} 13
{|−|}_{vϵ}, {|−|}_{⟨⟩ϵ}  native embedding of ⟨v⟩PCF^{2} into vPCF^{Λ,𝔰𝔱} 58
{|−|}_{pκ} Plotkin’s CPS transformations 11,34

{|−|}_{df^{2}κ}, {|−|}_{dfκ} Danvy and Filinski’s one-pass CPS transformation

11,34

| − |  annotation erasure of two-level terms  10,16,24
≡  strict syntactic equality  7
∼_{α}  α-equivalence  7
◯σ, v ◯σ, ◯^{at}(σ), … code types  {8,18, \atop 23,27}
D(−)  decoding of a term representation  13
unbr(−)  unbracketing of ⟨v⟩PCF^{2}-terms  56
E{θ}  application of the substitution θ to E

TDPE-specific notations

↓^{σ}  reification function at type σ  16,25
↑_{σ}  reflection function at type σ  16,25
{|−|}_{ri}  residualizing instantiation  16,25
NF (−)  static normalization function  16,25

References

[1] Alan Bawden. Quasiquotation in Lisp. In Olivier Danvy, editor, Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 4–12, San Antonio, Texas, January 1999. ACM

Press. Available online at http://www.brics.dk/~pepm99/programme.html.

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

[3] Anders Bondorf and Olivier Danvy. Automatic autoprojection of recursive equations with global variables and abstract data types. Science of Computer Programming, 16:151–195, 1991.

[4] Cristiano Calcago, Eugenio Moggi, and Walid Taha. Closed types as a simple approach to safe imperative multi-stage programming. In Ugo Montanari, José D. P. Rolim, and Emo Welzl, editors, 27th International Colloquium on Automata, Languages, and Programming, volume 1853 of Lecture Notes in Computer Science, pages 25–36, Geneva, Switzerland, July 2000.

[5] Olivier Danvy. Type-directed partial evaluation. In Steele [48], pages 242–257.

[6] Olivier Danvy. Type-directed partial evaluation. In John Hatcliff, Torben Æ. Mogensen, and Peter Thiemann, editors, Partial Evaluation – Practice and Theory; Proceedings of the 1998 DIKU Summer School, LNCS 1706, pages 367–411, Copenhagen, Denmark, July 1998.

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

[8] Olivier Danvy and John Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3):195–212, 1993.

[9] Olivier Danvy and Morten Rhiger. A simple take on typed abstract syntax in Haskell-like languages. In Herbert Kuchen and Kazunori Ueda, editors, Fifth International Symposium on Functional and Logic Programming, number 2024 in Lecture Notes in Computer Science, pages 343–358, Tokyo, Japan, March 2001. Springer-Verlag. Extended version available as the technical report BRICS RS-00-34.

[10] Rowan Davies. A temporal-logic approach to binding-time analysis. In Edmund M. Clarke, editor, Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 184–195, New Brunswick, New Jersey, July 1996.

[11] Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Steele [48], pages 258–283. Extended version to appear in Journal of the ACM, and also available as CMU Technical Report number CMU-CS-99-153, August 1999.

[12] Andrzej Filinski. A semantic account of type-directed partial evaluation. In Gopalan Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, LNCS 1702, pages 378–395, Paris, France, September 1999.

[13] Andrzej Filinski. Normalization by evaluation for the computational lambdacalculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 151–165, Kraków, Poland, May 2001. Springer-Verlag.

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

[15] Yoshihiko Futamura. Partial evaluation of computation process – an approach to a compiler-compiler. Higher-Order and Symbolic Computation, 12(4):381–391, 1999. Reprinted from Systems · Computers · Controls 2(5), 1971.

[16] Carsten K. Gomard. A self-applicable partial evaluator for the lambda-calculus: Correctness and pragmatics. ACM Transactions on Programming Languages and Systems, 14(2):147–172, 1992.

[17] Bernd Grobauer and Zhe Yang. The second Futamura projection for type-directed partial evaluation. In Lawall [30], pages 22–32. Extended version to appear in the journal Higher-Order and Symbolic Computation, 14(2/3), 2001.

[18] Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. The MIT Press, Cambridge, Massachusetts, 1992.

[19] John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 458–471, Portland, Oregon, January 1994.

[20] John Hatcliff and Olivier Danvy. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, 7(5):507–541, 1997.

[21] John McCarthy et al. LISP 1.5 Programmer’s Manual. The MIT Press, Cambridge, Massachusetts, 1962.

[22] Neil D. Jones, editor. Special issue on Partial Evaluation, Journal of Functional Programming, Vol. 3, Part 3. Cambridge University Press, July 1993.

[23] Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, 1993. Available

online at http://www.dina.kvl.dk/~sestoft/pebook/pebook.html.

[24] Neil D. Jones and Steven S. Muchnick. TEMPO: A Unified Treatment of Binding Time and Parameter Passing Concepts in Programming Languages, volume 66 of Lecture Notes in Computer Science. Springer-Verlag, 1978.

[25] Neil D. Jones, Peter Sestoft, and Harald Søndergaard. MIX: A self-applicable partial evaluator for experiments in compiler generation. Lisp and Symbolic Computation, 2(1):9–50, 1989.

[26] Richard Kelsey, William Clinger, and Jonathan Rees, editors. Revised^{5} report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(1):7–105, 1998. Also appears in ACM SIGPLAN Notices 33(9), September

1998. Available online at http://www.brics.dk/~hosc/11-1/.

[27] Eugene E. Kohlbecker, Daniel P. Friedman, Matthias Felleisen, and Bruce Duba. Hygienic macro expansion. In William L. Scherlis and John H. Williams, editors, Proceedings of the 1986 ACM Conference on Lisp and Functional Programming, pages 151–161, Cambridge, Massachusetts, August 1986.

[28] Eugene E. Kohlbecker and Mitchell Wand. Macro-by-example: Deriving syntactic transformations from their specifications. In Michael J. O’Donnell, editor, Proceedings of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, pages 77–84, München, West Germany, January 1987.

[29] Peter J. Landin. The next 700 programming languages. Communications of the ACM, 9(3):157–166, 1966.

[30] Julia L. Lawall, editor. ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, SIGPLAN Notices, Vol. 34, No 11, Boston, Massachusetts, November 2000. ACM Press.

[31] Peter Lee. Realistic Compiler Generation. The MIT Press, 1989.

[32] Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambdacalculi (summary). In Rohit Parikh, editor, Logics of Programs – Proceedings, LNCS 193, pages 219–224, Brooklyn, New York, June 1985.

[33] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.

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

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

[36] Eugenio Moggi. Functor categories and two-level languages. In Maurice Nivat, editor, Foundations of Software Science and Computation Structure, First International Conference, LNCS 1378, pages 211–225, Lisbon, Portugal, 1998.

[37] Eugenio Moggi, Walid Taha, Zine El-Abidine Benaissa, and Tim Sheard. An Idealized MetaML: Simpler, and more expressive. In S. Doaitse Swierstra, editor, Proceedings of the Eighth European Symposium on Programming, LNCS 1576, pages 193–207, Amsterdam, Netherlands, March 1999.

[38] Lockwood Morris. The next 700 formal language descriptions. Lisp and Symbolic Computation, 6(3/4):249–258, 1993.

[39] Peter D. Mosses. Action Semantics, volume 26 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

[40] Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages. Cambridge University Press, 1992.

[41] Flemming Nielson and Hanne Riis Nielson. Multi-level lambda-calculi: an algebraic description. In Olivier Danvy, Robert Glück, and Peter Thiemann, editors, Partial Evaluation, number 1110 in Lecture Notes in Computer Science, pages 338–354, Dagstuhl, Germany, February 1996.

[42] Flemming Nielson and Hanne Riis Nielson. Prescriptive frameworks for multi-level lambda-calculi. In Charles Consel, editor, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 193–202, Amsterdam, The Netherlands, June 1997.

[43] Jens Palsberg. Correctness of binding-time analysis. In Jones [22], pages 347–363.

[44] Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Mayer D. Schwartz, editor, Proceedings of the ACM SIGPLAN’88 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 23, No 7, pages 199–208, Atlanta, Georgia, June 1988.

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

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

[47] Gordon D. Plotkin. An illative theory of relations. In Richard Cooper, K. Mukai, and John Perry, editors, Situation Theory and Its Applications (Vol. 1), pages 133–146. CSLI, Stanford, California, 1990.

[48] Guy L. Steele, editor. Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, January 1996.

[49] Eijiro Sumii and Naoki Kobayashi. Online-and-offline partial evaluation: A mixed approah. In Lawall [30], pages 12–21. Extended version titled “A hybrid approach to online and offline partial evaluation” to appear in the journal Higher-Order and Symbolic Computation, 14(2/3), 2001.

[50] Walid Taha. A sound reduction semantics for untyped CBN multi-stage computation. or, the theory of MetaML is non-trival (extended abstract). In Lawall [30], pages 34–43.

[51] Mitchell Wand. Deriving target code as a representation of continuation semantics. ACM Transactions on Programming Languages and Systems, 4(3):496–517, 1982.

[52] Mitchell Wand. Specifying the correctness of binding-time analysis. In Jones [22], pages 365–387.

[53] Philip Wickline, Peter Lee, and Frank Pfenning. Run-time code generation and Modal-ML. In Keith D. Cooper, editor, Proceedings of the ACM SIGPLAN’98 Conference on Programming Languages Design and Implementation, pages 224– 235, Montréal, Canada, June 1998.

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

Recent BRICS Report Series Publications

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

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. Appears in Higher-Order and Symbolic Computation 14(2–3):173– 219 (2001). 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. To appear in ACM Transactions on Internet Technology, 2002.

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