BRICS RS-01-54 Damian & Danvy: Syntactic Accidents in Program Analysis BRICS

Basic Research in Computer Science

Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation

Daniel Damian Olivier Danvy BRICS Report Series RS-01-54 ISSN 0909-0878 December 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Daniel Damian & Olivier Danvy.

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/01/54/

Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation ^{∗}

Daniel Damian^{†} and Olivier Danvy

BRICS ^{‡}

Department of Computer Science University of Aarhus ^{§}

December 2001

Abstract

We show that a non-duplicating transformation into continuation-passing style (CPS) has no effect on control-flow analysis, a positive effect on bindingtime analysis for traditional partial evaluation, and no effect on binding-time analysis for continuation-based partial evaluation: a monovariant control-flow analysis yields equivalent results on a direct-style program and on its CPS counterpart, a monovariant binding-time analysis yields less precise results on a direct-style program than on its CPS counterpart, and an enhanced monovariant binding-time analysis yields equivalent results on a direct-style program and on its CPS counterpart. Our proof technique amounts to constructing the CPS counterpart of flow information and of binding times.

Our results formalize and confirm a folklore theorem about traditional bindingtime analysis, namely that CPS has a positive effect on binding times. What may be more surprising is that the benefit does not arise from a standard refinement of program analysis, as, for instance, duplicating continuations.

The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effect of syntactic change.

∗Extended version of an article to appear in the Journal of Functional Programming.

† Current affiliation: LION Bioscience Ltd., Compass House, 80-82 Newmarket Road, Cambridge CB5 8DZ, UK.

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

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

E-mail: {damian,danvy}@brics.dk Home pages: http://www.brics.dk/~{damian,danvy}

Contents

1 Introduction 4 1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 A loophole: the let rule . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2 Constraint-based analyses for a computational metalanguage 8 2.1 The language Λ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 The computational metalanguage . . . . . . . . . . . . . . . . . . . . . 8 2.3 The monadic let reductions . . . . . . . . . . . . . . . . . . . . . . . . 9 2.4 Λ_{v}: a call-by-value subset of the computational metalanguage . . . . . 9 2.5 Control-flow analysis for Λ_{v} . . . . . . . . . . . . . . . . . . . . . . . . 10 2.6 Binding-time analysis for Λ_{v} and traditional partial evaluation …. 12 2.7 Binding-time analysis for Λ_{v} and continuation-based partial evaluation 13

3 Comparing analysis results across program transformations 15

4 Control-flow analysis, binding-time analysis and monadic let reductions 16 4.1 Linear let-reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

4.1.1 Linear let.β reduction and CFA . . . . . . . . . . . . . . . . . . 17 4.1.2 Linear let.β reduction and BTA . . . . . . . . . . . . . . . . . . 18 4.1.3 Linear let.β reduction and BTA^{⋆} . . . . . . . . . . . . . . . . . 19

4.2 Let flattening . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.2.1 Let flattening and CFA . . . . . . . . . . . . . . . . . . . . . . 20 4.2.2 Let flattening and BTA . . . . . . . . . . . . . . . . . . . . . . 20 4.2.3 Let flattening and BTA^{⋆} . . . . . . . . . . . . . . . . . . . . . . 21

4.3 Summary and conclusions . . . . . . . . . . . . . . . . . . . . . . . . . 21

5 Introducing continuations 22

6 Control-flow analysis and the introduction of continuations 23 6.1 CPS transformation of control flow . . . . . . . . . . . . . . . . . . . . 23 6.2 Correctness of the transformation . . . . . . . . . . . . . . . . . . . . . 24 6.3 Reversing the transformation . . . . . . . . . . . . . . . . . . . . . . . 26 6.4 Correctness of the reverse transformation . . . . . . . . . . . . . . . . 27 6.5 Equivalence of flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 6.6 Summary and conclusions . . . . . . . . . . . . . . . . . . . . . . . . . 28

7 Binding-time analysis and the introduction of continuations 28 7.1 CPS transformation of binding times . . . . . . . . . . . . . . . . . . . 29 7.2 Correctness of the transformation . . . . . . . . . . . . . . . . . . . . . 29 7.3 Reversing the transformation . . . . . . . . . . . . . . . . . . . . . . . 31 7.4 Continuation-based partial evaluation . . . . . . . . . . . . . . . . . . 32 7.5 Summary and conclusions . . . . . . . . . . . . . . . . . . . . . . . . . 32 8 Related work 33

8.1 Program analysis in general . . . . . . . . . . . . . . . . . . . . . . . . 33 8.1.1 Region inference and the CPS transformation . . . . . . . . . . 33 8.1.2 Data-flow analysis and the CPS transformation . . . . . . . . . 33 8.1.3 CPS transformation of flow information . . . . . . . . . . . . . 35

8.2 Binding-time analysis and the CPS transformation . . . . . . . . . . . 35

9 Conclusion and issues 35

A Proofs 36

List of Figures

1 Staged CPS transformation . . . . . . . . . . . . . . . . . . . . . . . . 7 2 The language Λ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3 Call-by-value encoding into the computational metalanguage . . . . . 9 4 The monadic let reductions . . . . . . . . . . . . . . . . . . . . . . . . 9 5 Λ_{v}: The call-by-value subset of the computational metalanguage … 10 6 CFA relation for a program p . . . . . . . . . . . . . . . . . . . . . . . 11 7 Control-flow analysis (CFA) . . . . . . . . . . . . . . . . . . . . . . . . 11 8 BTA relation for a program p . . . . . . . . . . . . . . . . . . . . . . . 13 9 Binding-time analysis for traditional partial evaluation (BTA) . . . . . 13 10 BTA^{⋆} relation for a program p . . . . . . . . . . . . . . . . . . . . . . 14 11 Binding-time analysis for continuation-based partial evaluation (BTA^{⋆}) 14 12 Comparing results of constraint-based analyses . . . . . . . . . . . . . 16 13 Λ_{mnf} : The subset of Λ_{v} normalized with respect to let.β and let.assoc 22 14 Introducing continuations . . . . . . . . . . . . . . . . . . . . . . . . . 22 15 Introducing continuations and embedding into the Λ_{v} language …. 23 16 Transformation of control flow from direct style to CPS . . . . . . . . 25 17 Transformation of control flow from CPS to direct style . . . . . . . . 27 18 Transformation of binding times from direct style to CPS . . . . . . . 30

1 Introduction

1.1 Motivation

Program analyses are vulnerable to syntactic accidents in source programs in that innocent-looking, meaning-preserving transformations may substantially alter the precision of an analysis.

For a simple example, binding-time analysis (BTA) is vulnerable to re-association: given two static expressions s_{1} and s_{2} and one dynamic expression d, it makes a difference whether the source program is expressed as (s_{1} + s_{2}) + d or as s_{1} + (s_{2} + d). In the former case, the inner addition is classified as static and the outer one is classified as dynamic. In the latter case, both additions are classified as dynamic.

With the exception of BTA (and of region inference, see Section 8.1.1), little is known about the effect of programming style on program analyses. BTA is an exception because its output critically determines the amount of specialization carried out by an offline partial evaluator [6, 22]. Therefore, the output of binding-time analyses has been intensively studied, especially in connection with syntactic changes in their input. As a result, “binding-time improvements” have been developed to milk out extra precision from binding-time analyses [22, Chapter 12], to the point that partial-evaluation users are encouraged to write programs in a particular style [21]. That said, binding-time-improvements are not specific to offline partial evaluation— they are also routine in staging transformations [23] and in the formal specification of programming languages for semantics-directed compiling [30, Section 8.2].

Since one of the most effective binding-time improvements is the transformation of source programs into continuation-passing style (CPS) [4, 42], people have wondered whether CPS may help program analysis in general. Nielson’s early work on data-flow analysis [29] suggests so, since it shows that for a non-distributive analysis, a continuation semantics yields more precise results than a direct semantics. The CPS transformation is therefore a Good Thing, since for a direct semantics, it gives the effect of a continuation semantics. In the early 1990’s, Muylaert-Filho and Burn’s work [28] was starting to provide further indication of the value of the CPS transformation for abstract interpretation when Sabry and Felleisen entered the scene.

In their stunning article “Is continuation-passing useful for data-flow analysis?” [39], Sabry and Felleisen showed that for constant propagation, analyzing a directstyle program and analyzing its CPS counterpart yields incomparable results. They showed that CPS might increase precision by duplicating continuations, and also that CPS might decrease precision by confusing return points. These results are essentially confirmed by Palsberg and Wand’s recent CPS transformation of flow information [37]. At any rate, except for continuation-based partial evaluation [16], there seems to have been no further work about the effect of CPS on the precision of program analysis in general.

The situation is therefore that the CPS transformation is known to have an unpredictable effect on constant propagation and is also believed to have a positive effect on binding-time analysis. Still, we do not know for sure whether this positive effect is truly positive, or whether it worsens binding times elsewhere in the source program. One may also wonder whether, besides distributive monotone frameworks, there exist other program analyses on which CPS has no effect.

In this article, we answer these two questions by studying the effect of a nonduplicating CPS transformation on two off-the-shelf constraint-based program analyses—control-flow analysis (CFA) and BTA. Using a uniform proof technique, we formally show that:

(1) CPS has no effect on CFA, i.e., analyzing a direct-style program and analyzing its CPS counterpart yields equivalent results.

(2) CPS does not make BTA yield less precise results, and for the class of examples for which continuation-based partial evaluation was developed, it makes BTA yield results that are strictly more precise.

(3) CPS has no effect on an enhanced BTA which takes into account continuationbased partial evaluation.

This increased precision entailed by CPS also concerns analyses that have been noticed to be structurally similar to BTA, such as security analysis, program slicing, and call tracking [1]. These analyses display a similar symptom: for example, we are told that, in practice, users tend to find security analyses too conservative, without quite knowing what to do to obtain more precise results. (Here, “more precise results” means that more parts of the source program can be classified as low security.)

In the next section, we point out how the dependency induced by let-expressions leads to a loss of precision.

1.2 A loophole: the let rule

Offline partial evaluation [22] is a staged technique for specializing programs. In a first phase, the binding times of a source program, i.e., which parts are static (and should be evaluated at partial-evaluation time) and which parts are dynamic (and should be part of the specialized program) are analyzed. In a second phase, specialization proper takes place (i.e., the static parts are evaluated and the dynamic parts are residualized). Binding-time analysis is thus a data-flow analysis and when source programs are higher-order, it is driven by control-flow information. Such information is in turn obtained by a control-flow analysis.

A partial evaluator is correct when the meaning of the residual program is the same as the meaning of the source program applied to the static input. In particular, if the source language includes computational effects (for instance non-termination), the specializer must ensure that all the dynamic side effects of the source program are identically exhibited by the residual program.

To ensure this contextual coherence, a binding-time analysis classifies a let expression to be dynamic if its header is dynamic, because of possible side effects in the header and regardless of the binding time of the body. (Similarly, if a let header is classified to be of high security, the whole let expression is also classified to be of high security, regardless of the security level of its body.) Therefore, the body of the following λ-abstraction is classified as dynamic if e is dynamic:

λx.let v = e in b

The CPS counterpart of this λ-abstraction reads as follows:

λx.λk.e′ (λv.b′ k)

where e′ and b′ are the CPS counterparts of e and b, respectively. Now, assume that b naturally yields a static result independently of x, but is coerced to be dynamic because of the let rule. In the CPS term, e′ also yields a dynamic result, i.e., intuitively, v is classified to be dynamic. (This intuition is formalized in the rest of this article.) Intuitively, b′ also yields a static result and sends it to its continuation k. Therefore, in direct style, b yields a dynamic result whereas in CPS, it yields a static result.

Two observations need to be made at this point:

(1) The paragraph above is the standard motivation for improving binding times by CPS transformation [4] (see Section 8.2 for further detail). Nevertheless, what this paragraph leaves unsaid—and what actually has always been left unsaid—is whether this local binding-time improvement corresponds to a global improvement as well, or whether it may make things worse elsewhere in the source program. (In Section 7, we prove that this local improvement actually is a global improvement as well.)

(2) In their core calculus of dependency [1], Abadi et al. make a point that any function classified as d → s (resp. h → l, etc.) is necessarily a constant function. Nevertheless, as argued above, given a direct-style function classified to be d → d because of the let rule, its CPS counterpart may very well be classified as d → (s → o) → o and not be a constant function in continuation-passing style (i.e., a function applying its continuation to a constant).

Together, these two observations tell us that the let rule is overly conservative in BTA, security analysis, etc. CPS makes it possible to exploit the untapped precision of this rule non-trivially by providing a local improvement which—and this is a point of this article—is also a global improvement.

This global improvement is distinct from the common method of improving precision of program analysis by duplicating the analysis over the same program points. Sabry and Felleisen, for example, said that any improvement in precision provided by CPS is solely due to continuation duplication [39]. This assessment is true for their analysis, but it does not hold in general, as we have just shown for binding-time analysis.

Other approaches to improving analysis results amount to refining the definition of the analysis by including more information, such as, for instance, context information [20, 31, 32, 41]. In contrast, CPS-transforming the source program naturally provides a representation of the context as a syntactic support for refinement to the (unchanged) analysis.

In his work on data-flow analysis [29], Nielson shows that duplicating the analysis over conditional branches improves the analysis results. Let us point out that the CPS transformation also leads to binding-time improvements for conditional expressions. Indeed, to ensure contextual coherence for conditionals, the binding-time analysis makes conditional branches dynamic if the test is dynamic. This approximation can be circumvented with a CPS transformation. Therefore, the improvement is not produced by duplicating the analysis, but merely by the context relocation induced by the CPS transformation. This point is developed further in Section 7.4.

[figure: Λ; Λ_{ml}; Λ_{mnf}; Λ_{cps}; call-by-value; encoding; normalization; let.assoc + let.β; introduction of; continuations]

Figure 1: Staged CPS transformation

1.3 Overview

In this work we use a staged CPS transformation. Several equivalent methods exist for performing a global CPS transformation of a program. For example, one can use a Plotkin-style CPS transformation with administrative reductions [38], or one can stage the CPS transformation as normalization to a monadic normal form followed by introduction of continuations [15]. Palsberg and Wand use the former method [37], which can be extended to account for administrative reductions [8, 9]. We use the latter method here.

Elsewhere [8, 10], we have connected Danvy and Nielsen’s CPS transformation [13] with program analysis. We have constructed the corresponding CPS transformation of control-flow information and confirmed the results reported in the present paper.

Therefore, we use a CPS transformation obtained as follows:

1. call-by-value embedding of the input program into Moggi’s computational metalanguage [15, 27],

2. normalization under let.assoc and let.β (as defined in Hatcliff and Danvy’s account of CPS [15]), and

3. introduction of continuations.

The staged transformation is visualized in the diagram of Figure 1.

The rest of this article is organized as follows: in Section 2 we define the input language, the transformation steps leading to CPS, and the program analyses. More specifically, in Section 2.1 we present the labeled language of input programs. In Section 2.2 we review the computational metalanguage and the corresponding callby-value encoding of the input language. In Section 2.3 we recall the monadic letreductions.

We continue by introducing the constraint-based analyses for the computational metalanguage. In Section 2.5 we specify the control-flow analysis. In Section 2.6 we specify the binding-time analysis corresponding to traditional partial evaluation. In Section 2.7 we specify the binding-time analysis corresponding to continuation-based partial evaluation.

In Section 3 we outline how to compare the results of a constraint-based program analysis across a program transformation.

In Section 4 we evaluate the effect on constraint-based analyses incurred by the normalization of the source program with respect to let-reductions: we investigate the effect of let.β (Section 4.1) and let.assoc (Section 4.2) reductions over each of the analyses. We conclude (Section 4.3) that linear let-reductions and let flattening do not change the result of the control-flow analysis, while they do improve the results of the traditional binding-time analysis.

In the remainder of the article, we evaluate the effect of introducing continuations (Section 5) over the result of control-flow analysis (Section 6), binding-time analysis

e ∈ Exp ::= x | n | λx.e | rec f(x).e | e_{0} e_{1} | op(e) | if0 e e_{0} e_{1}
x, f ∈ Ide  (identifiers)
n ∈ Int  (integers)
op ∈ (an unspecified set of base-type operators)

Figure 2: The language Λ

for traditional partial evaluation (Sections 7.1 to 7.3) and binding-time analysis for continuation-based partial evaluation (Section 7.4). In Section 8 we review related work. In Section 9 we conclude and discuss further issues.

2 Constraint-based analyses for a computational metalanguage

We introduce the language of input programs and the individual transformations performed by the CPS transformation. We then present the three program analyses: CFA, BTA and BTA^{⋆}.

2.1 The language Λ

We consider that programs are given in an untyped λ-language Λ. The terms of the language are expressions given by the grammar of Figure 2. The language includes literals, λ-abstractions, recursive function definitions, conditionals and base-type operators (for simplicity, we only consider unary operators here). We focus on call by value. Since the evaluation of terms in the language may not terminate, programs in Λ may exhibit non-termination as a computational effect.

A program p is a closed expression.

2.2 The computational metalanguage

The computational metalanguage Λ_{ml} [15] enforces the order of evaluation by introducing a let construct for naming intermediate computations and a unit construct for lifting a value into a computation.

e ::= … | let x = e_{1} in e_{2} | unit e

The computational metalanguage comes with a set of sound reasoning principles about programs which may have computational effects, such as non-termination. Such principles can be used to validate program transformations performed, for instance, inside a compiler. They can also be used to validate, for instance, a partial evaluator [16].

In order to make use of such principles, an input program in the language Λ is encoded into the computational metalanguage, enforcing its order of evaluation. For call by value, the encoding into the monadic metalanguage is defined in Figure 3.

Notice that, in addition to other known call-by-value encodings [2, 15, 40], we name the result of the application of two values (x_{1} and x_{2} in the translation of an application). This cosmetic change (indeed, it is only a let.η expansion in the

V[[x]] = unit x
V[[n]] = unit n
V[[λx.e]] = unit λx.V[[e]]
V[[rec f(x).e]] = unit rec f(x).e
V[[e_{0} e_{1}]] = let x_{0} = V[[e_{0}]]
in let x_{1} = V[[e_{1}]]
in let x_{2} = x_{0} x_{1}
in unit x_{2}
V[[op(e)]] = let x_{0} = V[[e]] in let x_{1} = op(x_{0}) in unit x_{1}
V[[if0 e e_{0} e_{1}]] = let x_{0} = V[[e]]
in let x_{1} = if0 x_{0} V[[e_{0}]] V[[e_{1}]]
in unit x_{1}

(where the x_{i} are fresh)

Figure 3: Call-by-value encoding into the computational metalanguage

let x = unit t in e →_{let.β} e[t/x]
let x = e in unit x →_{let.η} e
let x_{2} = let x_{1} = e_{1} in e_{2} in e →_{let.assoc} let x_{1} = e_{1} in let x_{2} = e_{2} in e

Figure 4: The monadic let reductions

computational metalanguage) is part of our development of the CPS transformation of flow information.

2.3 The monadic let reductions

The call-by-value encoding leads to a separation of terms into two categories: trivial terms (noted with t) and serious terms (noted with s). Trivial terms represent values: constants, variables, λ-abstractions and recursive function definitions. Serious terms represent computations: applications, basic operations, conditionals, nesting of computations by naming intermediate results.

We recall the monadic let-reductions. Normalization under the let-reductions is the first step in a staged CPS transformation [15]. The let-β reduction, let-η reduction and the let-flattening reduction are presented in Figure 4.

2.4 Λ_{v}: a call-by-value subset of the computational metalanguage

In this paper, we focus on the call-by-value embedding. Therefore, we restrict ourselves to the subset of Λ_{ml} that forms the image of the call-by-value embedding of Λ. The language Λ_{v} of labeled terms is defined in Figure 5. Indeed, the call-by-value embedding produces either trivial terms (t ∈ Triv) or let-expressions. All serious terms (s ∈ Step) are named. Since for the call-by-value embedding the occurrences of the unit construct can be deduced from the context, we omit them in Λ_{v} terms.

Note that the language is such that the final result of a computation is also named, since we no longer perform let.η reductions in Λ_{v} before introducing continuations.

p ∈ Pgm ::= e^{ℓ}
e ∈ Exp ::= t | let x = s in e^{ℓ}
s ∈ Step ::= t^{ℓ} | t_{0}^{ℓ_{0}} t_{1}^{ℓ_{1}} | op(t^{ℓ}) | if0 t^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} | (let x = s in e^{ℓ_{1}})^{ℓ_{2}}
t ∈ Triv ::= n | x | λ^{π}x.e^{ℓ} | rec^{π}f(x).e^{ℓ}
x ∈ Ide  (identifiers)
n ∈ Int  (integers)
ℓ ∈ Lab  (term labels)
π ∈ Lam  (λ-abstraction labels)
op ∈ an unspecified set of base-type operators

Figure 5: Λ_{v}: The call-by-value subset of the computational metalanguage

This aspect is part of our development of the CPS transformation of flow information, and will be illustrated further in Section 6.

For the purpose of program analysis, terms are labeled with labels ℓ taken from a countable set Lab. In addition, λ-abstractions and recursive functions are identified by labels π from another set Lam, so that, for example, in (λ^{π}x.e^{ℓ_{1}})^{ℓ_{0}}, ℓ_{0} and ℓ_{1} belong to Lab and π belongs to Lam.

Definition 1 A properly labeled expression is a labeled expression in which all labels are distinct and all variables are distinct.

We should note that, for the purpose of control-flow analysis or binding-time analysis, it is not essential that the input program is properly labeled. But the precision of the analysis is increased if distinct program points have distinct labels, and distinct variables have distinct names. Since we want to compare the absolute precision of an analysis before and after program transformation, we consider the best results that the analysis can give over the program. For this reason, we consider only properly labeled programs and only transformations that lead to properly labeled programs.

2.5 Control-flow analysis for Λ_{v}

We consider a constraint-based, monovariant control-flow analysis (CFA) over programs in Λ_{v}. The constraint-based version [14, 20, 31, 34] is known to be equivalent to other versions, based on different methods such as set-based analysis [17] and type inference [35]; it is also known to be an instance of abstract interpretation [7]. For uniformity, we adopt the same definition and notation as in Nielson, Nielson and Hankin’s recent textbook on program analysis [32].^{1}

The flow information computed by the analysis is a pair consisting of an abstract cache Ĉ_{cf} mapping terms to abstract values and an abstract environment ρ̂_{cf} mapping variables to abstract values. Abstract values are sets of labels of λ-abstractions to which a term can be reduced and a variable can be bound. The constraint-based control-flow analysis is specified as a relation ⊨_{cf} on caches, environments and terms.

1Nielson, Nielson and Hankin’s CFA is developed for a call-by-value language with recursion and let-constructs. It is thus compatible with the language subset considered here.

Lam^{p}  The set of λ-abstraction labels in p
Var^{p}  The set of identifiers in p
Lab^{p}  The set of term labels in p
Val_{cf}^{p} = P(Lam^{p})  Abstract values
Ĉ_{cf} ∈ Cache_{cf}^{p} = Lab^{p} → Val_{cf}^{p} Abstract cache
ρ̂_{cf} ∈ Env_{cf}^{p} = Var^{p} → Val_{cf}^{p} Abstract environment

⊨_{cf}^{p} ⊆ (Cache_{cf}^{p} × Env_{cf}^{p}) × Lab^{p}

Figure 6: CFA relation for a program p

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} n^{ℓ}  ⟺ true
(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} x^{ℓ}  ⟺ ρ̂_{cf}(x) ⊆ Ĉ_{cf}(ℓ)
(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} (λ^{π}x.e^{ℓ_{1}})^{ℓ}  ⟺ {π} ⊆ Ĉ_{cf}(ℓ) ∧ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e^{ℓ_{1}}

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} (rec^{π}f(x).e^{ℓ_{1}})^{ℓ} ⟺ {π} ⊆ Ĉ_{cf}(ℓ) ∧ {π} ⊆ ρ̂_{cf}(f) ∧

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e^{ℓ_{1}}

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} (let x = t^{ℓ} in e^{ℓ_{1}})^{ℓ_{2}} ⟺ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} t^{ℓ} ∧ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e^{ℓ_{1}} ∧

Ĉ_{cf}(ℓ) ⊆ ρ̂_{cf}(x) ∧ Ĉ_{cf}(ℓ_{1}) ⊆ Ĉ_{cf}(ℓ_{2})

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} \begin{matrix}(let x = t_{0}^{ℓ_{0}} t_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ⟺ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} t_{0}^{ℓ_{0}} ∧ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} t_{1}^{ℓ_{1}} ∧

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e^{ℓ_{2}} ∧ Ĉ_{cf}(ℓ_{2}) ⊆ Ĉ_{cf}(ℓ_{3}) ∧ ∀(λ^{π}y.e_{1}^{ℓ}) ∈ Ĉ_{cf}(ℓ_{0}).

(Ĉ_{cf}(ℓ_{1}) ⊆ ρ̂_{cf}(y) ∧ Ĉ_{cf}(ℓ) ⊆ ρ̂_{cf}(x))

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} \begin{matrix}(let x = op(t^{ℓ}) \\ in e^{ℓ_{1}})^{ℓ_{2}} \end{matrix} ⟺ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} t^{ℓ} ∧ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e^{ℓ_{1}} ∧

Ĉ_{cf}(ℓ_{1}) ⊆ Ĉ_{cf}(ℓ_{2})

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} \begin{matrix}(let x = \\ if0 t^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ⟺ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} t^{ℓ} ∧ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e_{0}^{ℓ_{0}} ∧

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e_{1}^{ℓ_{1}} ∧ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e^{ℓ_{2}} ∧ Ĉ_{cf}(ℓ_{0}) ⊆ ρ̂_{cf}(x) ∧ Ĉ_{cf}(ℓ_{1}) ⊆ ρ̂_{cf}(x) ∧ Ĉ_{cf}(ℓ_{2}) ⊆ Ĉ_{cf}(ℓ_{3})

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} (let x = \begin{matrix}(let x_{1} = s \\ in e_{1}^{ℓ_{1}})^{ℓ_{2}} \end{matrix} in e^{ℓ_{3}})^{ℓ_{4}} ⟺ (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} (let x_{1} = s in e_{1}^{ℓ_{1}})^{ℓ_{2}} ∧

(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} e^{ℓ_{3}} ∧ Ĉ_{cf}(ℓ_{2}) ⊆ ρ̂_{cf}(x) ∧ Ĉ_{cf}(ℓ_{3}) ⊆ Ĉ_{cf}(ℓ_{4})

Figure 7: Control-flow analysis (CFA)

Given a term e, (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf} e means that (Ĉ_{cf}, ρ̂_{cf}) is a result of the control-flow analysis of e.^{2}

In this work we use the syntax-directed variant of the analysis [32, Chapter 3], and we restrict its analysis relation to a relation ⊨_{cf}^{p} associated to each program p being analyzed. Given a properly labeled program p ∈ Λ_{ml}, the functionality of the associated relation ⊨_{cf}^{p} is defined in Figure 6. The analysis relation is defined in Figure 7 by induction over the syntax of the program.

Any solution (Ĉ_{cf}, ρ̂_{cf}) accepted by the relation ⊨_{cf}^{p} (i.e., such that the statement (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} p holds) is a conservative approximation of the exact flow information [32, Chapter 3]. Furthermore, the analysis relation ⊨_{cf}^{p} has a model-intersection property, i.e., the set of solutions accepted by ⊨_{cf}^{p} is closed under intersection. The model-intersection property ensures the existence of a least solution of the analysis, i.e., a most precise one. (Here, the order relation is given by the pointwise ordering of functions induced by set inclusion.) In practice, a work-list based algorithm computes the least solution.

2In the notation of Nielson, Nielson, and Hankin [32], ⊨_{cf} is simply ⊨.

2.6 Binding-time analysis for Λ_{v} and traditional partial evaluation

We consider a constraint-based binding-time analysis (BTA) for the call-by-value subset Λ_{v} of the computational metalanguage. The analysis is an adaptation of Hatcliff and Danvy’s BTA for the computational metalanguage [16], presented in constraint form [33, 34, 36]. The analysis determines binding times of program points and program variables. The binding-time information is used in offline partial evaluation [6, 22, 33]: the result of the analysis determines the static computations performed at specialization time.

The constraint-based BTA uses flow information to determine the binding times of the operators and operands of applications. Alternatively, we could have considered an analysis computing both flow and binding-time information at the same time, which is known to give equivalent results [34]. We have chosen to separate the control-flow analysis from the binding-time analysis in order to investigate separately the effect of CPS on flow information and on binding times.

The formal definition of the analysis is similar to the definition of the CFA of Section 2.5. The analysis is a relation defined on essentially the same domains (Figure 8); the difference is that the domain of abstract values is now the standard lattice {S ⊑ D} of static and dynamic annotations. The analysis relation is defined inductively over the syntax (Figure 9). At application points, the definition of the BTA refers to the flow information (Ĉ_{cf}, ρ̂_{cf}), which is considered to be the least solution of the control-flow analysis of Section 2.5.

In contrast to the CFA of Section 2.5, the BTA accepts non-closed terms. Following the tradition, we consider the program to be dynamic and its free variables to be dynamic as well. The flow information for the free variables is considered to be empty, which is the result of applying the CFA to the program closed by abstraction over the free variables. Another difference with the CFA of Section 2.5 is that the constraints generated by the BTA are equality constraints.

Finally, additional constraints are generated for λ-abstractions, conditionals and let-expressions. For example, the argument and body of an abstraction are dynamic if the abstraction itself is dynamic. As mentioned in Section 1.2, the following bindingtime constraints ensure contextual coherence. In each let expression, the body is constrained to be dynamic if the header is dynamic. In each conditional expression, both branches are constrained to be dynamic if the test is dynamic. Note that we allow static operations in dynamic contexts so that static computations can take place at partial-evaluation time. A proof of correctness of a specializer using the annotations obtained by this traditional BTA can be found in Hatcliff and Danvy’s work [16].

Val_{bt} = {S, D}  Abstract values
Ĉ_{bt} ∈ Cache_{bt}^{p} = Lab^{p} → Val_{bt} Abstract cache
ρ̂_{bt} ∈ Env_{bt}^{p} = Var^{p} → Val_{bt} Abstract environment

⊨_{bt}^{p} ⊆ (Cache_{bt}^{p} × Env_{bt}^{p}) × Lab^{p} Figure 8: BTA relation for a program p

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} n^{ℓ}  ⟺ true
(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} x^{ℓ}  ⟺ ρ̂_{bt}(x) = Ĉ_{bt}(ℓ)
(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} (λ^{π}x.e^{ℓ_{1}})^{ℓ}  ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e^{ℓ_{1}} ∧

(Ĉ_{bt}(ℓ) = D ⇒ Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(x) = D)

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} (rec^{π}f(x).e^{ℓ_{1}})^{ℓ} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e^{ℓ_{1}} ∧ Ĉ_{bt}(ℓ) = ρ̂_{bt}(f) ∧

(Ĉ_{bt}(ℓ) = D ⇒ Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(x) = D)

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} \begin{matrix}(let x = t^{ℓ} \\ in e^{ℓ_{1}})^{ℓ_{2}} \end{matrix} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} t^{ℓ} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e^{ℓ_{1}} ∧

Ĉ_{bt}(ℓ) = ρ̂_{bt}(x) ∧ Ĉ_{bt}(ℓ_{1}) = Ĉ_{bt}(ℓ_{2}) ∧ ρ̂_{bt}(x) = D ⇒ Ĉ_{bt}(ℓ_{1}) = D

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} \begin{matrix}(let x = t_{0}^{ℓ_{0}} t_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} t_{0}^{ℓ_{0}} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} t_{1}^{ℓ_{1}} ∧

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e^{ℓ_{2}} ∧ Ĉ_{bt}(ℓ_{2}) = Ĉ_{bt}(ℓ_{3}) ∧ (Ĉ_{bt}(ℓ_{0}) = D ⇒ Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(x) = D) ∧ (ρ̂_{bt}(x) = D ⇒ Ĉ_{bt}(ℓ_{2}) = D) ∧

∀(λ^{π}y.e_{1}^{ℓ}) ∈ Ĉ_{cf}(ℓ_{0}).(\begin{matrix}Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(y) ∧ \\ Ĉ_{bt}(ℓ) = ρ̂_{bt}(x)) \end{matrix}

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} \begin{matrix}(let x = op(t^{ℓ}) \\ in e^{ℓ_{1}})^{ℓ_{2}} \end{matrix} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} t^{ℓ} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e^{ℓ_{1}} ∧

Ĉ_{bt}(ℓ) ⊑ ρ̂_{bt}(x) ∧ Ĉ_{bt}(ℓ_{1}) = Ĉ_{bt}(ℓ_{2}) ∧ (ρ̂_{bt}(x) = D ⇒ Ĉ_{bt}(ℓ_{1}) = D)

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} (\begin{matrix}let x = \\ if0 t^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} t^{ℓ} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e_{0}^{ℓ_{0}} ∧

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e_{1}^{ℓ_{1}} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e^{ℓ_{2}} ∧ Ĉ_{bt}(ℓ_{0}) = Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(x) ∧ (Ĉ_{bt}(ℓ) = D ⇒ Ĉ_{bt}(ℓ_{0}) = Ĉ_{bt}(ℓ_{1}) = D) ∧ (ρ̂_{bt}(x) = D ⇒ Ĉ_{bt}(ℓ_{2}) = D) ∧ Ĉ_{bt}(ℓ_{2}) = Ĉ_{bt}(ℓ_{3})

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} (let x = \begin{matrix}(let x_{1} = s \\ in e_{1}^{ℓ_{1}})^{ℓ_{2}} \end{matrix} in e^{ℓ_{3}})^{ℓ_{4}} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} (let x_{1} = s in e_{1}^{ℓ_{1}})^{ℓ_{2}} ∧

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} e^{ℓ_{3}} ∧ Ĉ_{bt}(ℓ_{2}) = ρ̂_{bt}(x) ∧ (ρ̂_{bt}(x) = D ⇒ Ĉ_{bt}(ℓ_{1}) = D) ∧ Ĉ_{bt}(ℓ_{3}) = Ĉ_{bt}(ℓ_{4})

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} p ⟺ (∀x.x free in p ⇒ ρ̂_{bt}(x) = D) ∧

(p = e^{ℓ} ⇒ Ĉ_{bt}(ℓ) = D)

Figure 9: Binding-time analysis for traditional partial evaluation (BTA)

2.7 Binding-time analysis for Λ_{v} and continuation-based par-

tial evaluation

As mentioned in Section 1.2, the traditional binding-time analysis from Section 2.6 is overly conservative because of the context coherence constraint imposed in the let rule.

Val_{bt} = {S, D}  Abstract values
Ĉ_{bt} ∈ Cache_{bt}^{p} = Lab^{p} → Val_{bt} Abstract cache
ρ̂_{bt} ∈ Env_{bt}^{p} = Var^{p} → Val_{bt} Abstract environment

⊨_{bt^{⋆}}^{p} ⊆ (Cache_{bt}^{p} × Env_{bt}^{p}) × Lab^{p}

Figure 10: BTA^{⋆} relation for a program p

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} n^{ℓ}  ⟺ true
(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} x^{ℓ}  ⟺ ρ̂_{bt}(x) = Ĉ_{bt}(ℓ)
(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} (λ^{π}x.e^{ℓ_{1}})^{ℓ}  ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e^{ℓ_{1}} ∧

(Ĉ_{bt}(ℓ) = D ⇒ Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(x) = D)

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} (rec^{π}f(x).e^{ℓ_{1}})^{ℓ} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e^{ℓ_{1}} ∧ Ĉ_{bt}(ℓ) = ρ̂_{bt}(f) ∧

(Ĉ_{bt}(ℓ) = D ⇒ Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(x) = D)

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} \begin{matrix}(let x = t^{ℓ} \\ in e^{ℓ_{1}})^{ℓ_{2}} \end{matrix} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} t^{ℓ} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e^{ℓ_{1}} ∧

Ĉ_{bt}(ℓ) = ρ̂_{bt}(x) ∧ Ĉ_{bt}(ℓ_{1}) = Ĉ_{bt}(ℓ_{2})

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} \begin{matrix}(let x = t_{0}^{ℓ_{0}} t_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} t_{0}^{ℓ_{0}} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} t_{1}^{ℓ_{1}} ∧

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e^{ℓ_{2}} ∧ Ĉ_{bt}(ℓ_{2}) = Ĉ_{bt}(ℓ_{3}) ∧ (Ĉ_{bt}(ℓ_{0}) = D ⇒ Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(x) = D) ∧ ∀(λ^{π}y.e_{1}^{ℓ}) ∈ Ĉ_{cf}(ℓ_{0}).(Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(y) ∧ Ĉ_{bt}(ℓ) = ρ̂_{bt}(x))

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} \begin{matrix}(let x = op(t^{ℓ}) \\ in e^{ℓ_{1}})^{ℓ_{2}} \end{matrix} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} t^{ℓ} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e^{ℓ_{1}} ∧

Ĉ_{bt}(ℓ) ⊑ ρ̂_{bt}(x) ∧ Ĉ_{bt}(ℓ_{1}) = Ĉ_{bt}(ℓ_{2})

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} (\begin{matrix}let x = \\ if0 t^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} t^{ℓ} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e_{0}^{ℓ_{0}} ∧

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e_{1}^{ℓ_{1}} ∧ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e^{ℓ_{2}} ∧ Ĉ_{bt}(ℓ_{0}) = Ĉ_{bt}(ℓ_{1}) = ρ̂_{bt}(x) ∧ Ĉ_{bt}(ℓ_{2}) = Ĉ_{bt}(ℓ_{3})

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} (let x = \begin{matrix}(let x_{1} = s \\ in e_{1}^{ℓ_{1}})^{ℓ_{2}} \end{matrix} in e^{ℓ_{3}})^{ℓ_{4}} ⟺ (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} (let x_{1} = s in e_{1}^{ℓ_{1}})^{ℓ_{2}} ∧

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} e^{ℓ_{3}} ∧ Ĉ_{bt}(ℓ_{2}) = ρ̂_{bt}(x) ∧ Ĉ_{bt}(ℓ_{3}) = Ĉ_{bt}(ℓ_{4})

(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt^{⋆}}^{p} p ⟺ (∀x.x free in p ⇒ ρ̂_{bt}(x) = D) ∧ (p = e^{ℓ} ⇒ Ĉ_{bt}(ℓ) = D)

Figure 11: Binding-time analysis for continuation-based partial evaluation (BTA^{⋆})

(Compared to Figure 9, we disabled the context coherence constraints in the 5th, 6th, 7th, 8th and 9th case.)

The constraint reflects the concern about which reductions can be safely performed by the specializer. Indeed, in the computational metalanguage [16], a named dynamic computation cannot be discarded due to possible computational effects. Similarly, the contextual coherence constraint over the conditional branches is introduced because one cannot decide statically which conditional branch should be selected. We will show in Sections 4 and 7 that these context coherence constraints are the source of binding-time improvements by CPS transformation.

The context coherence constraint on the body of a let-expression can be relaxed if one uses a continuation-based program specializer [3, 16, 25]. The context coherence constraint connecting the conditional branches with the test can be relaxed as well if one allows the same continuation-based specializer to lift the test above the context, either by duplicating the context or by naming the continuation with a let-expression.

We consider a binding-time analysis which takes into account a continuation-based specializer. More formally, we consider the BTA of Figure 9, without the context coherence constraints mentioned above. The functionality of the new relation ⊨_{bt^{⋆}}^{p} is defined in Figure 10, and it is identical to the functionality of the traditional BTA relation ⊨_{bt}^{p} (Figure 8). To define the new BTA relation, we replace the rules for let-expressions and conditional expressions as specified in Figure 11. The result is BTA^{⋆}.

3 Comparing analysis results across program transformations

How do we compare the results of a program analysis before and after a program transformation? The result of an analysis is a function mapping labels and program variables to analysis information. For simplicity, we expect that the transformation preserves some of the labels and variables of the initial program. Under this assumption, we relate the results of the analysis by comparing the analysis information associated with the labels and variables preserved by the transformation.

Let us say that the program p is transformed into the program p′. Let us assume that the points (labels and variables) common to p and p′ are identified as a set L. Let S be an arbitrary solution of the analysis of p and S′ be an arbitrary solution of the analysis of p′. We consider that the solutions S and S′ are equivalent if S′|_{L} = S|_{L}, where S|_{L} is the restriction of the mapping S to the set L of common program points.

To establish a relationship between the two best analysis results we use a constructive technique. Given an arbitrary solution S of a constraint-based analysis of a program p, we show how to construct an equivalent solution S′ of the analysis of the transformed program p′. We then show that the construction is valid, i.e., that S′ is a valid solution of the analysis. Our construction induces a monotone mapping Φ between the two spaces of solutions. From the model-intersection property of the constraint-based analyses we conclude that the best result of the analysis of p′ is at least as good as the results of the analysis of p. This situation is pictured in Figure 12.

In some cases, given a solution of the analysis of p′, we are also able to construct an equivalent solution of the analysis of p, inducing an inverse mapping Ψ. When Φ and Ψ are both monotone and their composition in both ways leads to contractions (similarly to a Galois connection), we are able to show that the best result of the analysis of p is equivalent to the best result of the analysis of p′. In such cases we conclude that the specific program transformation has no impact on the result of the analysis.

[figure: S; •; S′; •; p; p′; solutions; solutions; •; •; analysis; transformation; Φ; analysis; Φ]

Figure 12: Comparing results of constraint-based analyses

4 Control-flow analysis, binding-time analysis and monadic let reductions

In order to avoid generating administrative redexes when introducing continuations, Λ_{ml}-programs need to be normalized with respect to the monadic let-reductions [15]. The Λ_{v} language is closed under the let.β and let.assoc reductions. In this section, we investigate the effect of each of the two reductions over the constraint-based analyses defined in Section 2.

According to the subject-reduction property of the control-flow or binding-time analyses [32, 33], a valid result of an analysis will also be a valid result of the analysis after a let-reduction (though not necessarily the least one). What is not clear, however, is whether the least (i.e., the best) result of the analysis is also the least result of the analysis after such reductions. We rely on the linearity of the transformations to show that flow information is not improved. We also show that let reductions may lead to strict binding-time improvements; we also show that the context coherence constraints are the cause of such improvements: disabling them leads to no improvements after a let reduction.

The let-expressions introduced by the call-by-value embedding of Figure 3 are linear: they do not duplicate or throw away code. Moreover, their linearity is preserved by the let.β and let.assoc reductions. In the following sections, we formalize the notion of linearity (Section 4.1), and use it to characterize the effect of the let.β and let.assoc reductions over CFA, BTA and BTA^{⋆} (Sections 4.1.1 through 4.2.3).

4.1 Linear let-reduction

We formalize the notion of linear let-reduction as a let.β reduction such that the let body contains a unique occurrence of the variable named in the let header. The key observation, which we will prove in Section 4.1.1, is that linear reductions have no effect on the control-flow analysis. Linearity is essential: it is simple to show that non-linear (code-duplicating) reductions may improve the result of the control-flow analysis.

Definition 2 A linear context is an expression with a unique hole [·]. Linear contexts are defined by the following grammar:

E ::= T | (let x = S in e^{ℓ_{1}})^{ℓ} | (let x = s in E)^{ℓ}
S ::= T | T t_{1}^{ℓ_{1}} | t_{0}^{ℓ_{0}} T | op(T) | if0 T e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} | if0 t^{ℓ} E e_{1}^{ℓ_{1}} | if0 t^{ℓ} e_{0}^{ℓ_{0}} E |
(let x = S in e^{ℓ_{1}})^{ℓ} | (let x = s in E)^{ℓ}
T ::= [·] | (λ^{π}x.E)^{ℓ} | (rec^{π}f(x).E)^{ℓ}

We use linear contexts to identify contexts which are filled as the result of a let.β reduction. Note that linear contexts as defined in Definition 2 are more expressive than contexts that may result from the call-by-value embedding: the CPS transformation does not extract terms from inside lambda-expressions and conditional branches. Nevertheless, the results we are presenting hold in this enlarged setting.

We also formalize the notion of a let-context as a context where a let-reduction might take place.

Definition 3 A let context is an expression which contains a unique hole [·] in the place of a let-expression. Let-contexts are defined by the following grammar:

E ::= [·] | T | (let x = S in e^{ℓ_{1}})^{ℓ} | (let x = s in E)^{ℓ}
S ::= [·] | T | T t_{1}^{ℓ_{1}} | t_{0}^{ℓ_{0}} T | op(T) | if0 T e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} | if0 t^{ℓ} E e_{1}^{ℓ_{1}} |
if0 t^{ℓ} e_{0}^{ℓ_{0}} E | (let x = S in e^{ℓ_{1}})^{ℓ} | (let x = s in E)^{ℓ}
T ::= (λ^{π}x.E)^{ℓ} | (rec^{π}f(x).E)^{ℓ}

Given a linear context E and a trivial term t^{ℓ}, we use E[t^{ℓ}] to denote the context E with the hole [·] replaced with t^{ℓ}. It is trivial to see that E[t^{ℓ}] is a well-formed expression. We use the same notation for plugging a labeled let-expression into a let context. Again, the operation is well defined.

We use FV (e) to denote the set of free variables of the expression e. This notation naturally extends to contexts, by considering the hole [·] to contain no free variables. We also use L as the function extracting the label of an expression. By definition, for any labeled expression e^{ℓ}, L(e^{ℓ}) = ℓ.

Definition 4 A linear let is an expression of the form let x = s in e^{ℓ} such that e^{ℓ} contains a unique free occurrence of x.

It is immediate to see that if a let-expression let x = s in e^{ℓ} is linear, then there exists a linear context E and a label ℓ_{1} such that e^{ℓ} = E[x^{ℓ_{1}}].

Definition 5 A linear let.β reduction is a let.β reduction of a linear let.

It is relevant to notice that all the let.β redexes introduced by the call-by-value embedding are linear and that reducing any of these redexes does not change this property.

4.1.1 Linear let.β reduction and CFA

Let us show that a linear let.β reduction does not alter the results of the CFA. Let p be a properly labeled program such that there exist a let context E and a linear context E_{1} such that

p = E[(let x = t^{ℓ} in E_{1}[x^{ℓ_{1}}])^{ℓ_{2}}]

Let p′ be the program p after performing the linear let.β reduction:

p′ = E[E_{1}[t^{ℓ}]]

It is immediate to see that p′ is a properly labeled program.

We show that the least solution of the flow analysis of p is equivalent to the least solution of the analysis of p′. In fact, the least solution for p′ is obtained from the least solution for p by projection on the labels and variables preserved by the transformation.

We define the following functions:

• Φ_{cf}^{let.β} : (Cache_{cf}^{p} × Env_{cf}^{p}) → (Cache_{cf}^{p′} × Env_{cf}^{p′}) such that

Φ_{cf}^{let.β}(Ĉ_{cf}, ρ̂_{cf}) = (Ĉ_{cf}|_{Lab}_{p′} , ρ′_{cf}|_{Var}_{p′})

• Ψ_{cf}^{let.β} : (Cache_{cf}^{p′} × Env_{cf}^{p′}) → (Cache_{cf}^{p} × Env_{cf}^{p}) such that, if Ψ_{cf}^{let.β}(Ĉ′_{cf}, ρ′_{cf}) = (Ĉ_{cf}, ρ̂_{cf}), then

– Ĉ_{cf} = Ĉ′_{cf} ⊔ [ℓ_{1} ↦ Ĉ′_{cf}(ℓ), ℓ_{2} ↦ Ĉ′_{cf}(L(E_{1}[t^{ℓ}]))]

– ρ̂_{cf} = ρ′_{cf} ⊔ [x ↦ Ĉ′_{cf}(ℓ)].

The two functions mediate between solutions for p and p′.

Lemma 4.1 If (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} p then Φ_{cf}^{let.β}(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p′} p′, and if (Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p′} p′ then Ψ_{cf}^{let.β}(Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p} p.

It is immediate to show that Φ_{cf}^{let.β} and Ψ_{cf}^{let.β} form an embedding/projection pair. The following lemma is a direct consequence.

Lemma 4.2 If (Ĉ_{cf}, ρ̂_{cf}) is the least solution of the CFA of p and (Ĉ′_{cf}, ρ′_{cf}) is the least solution of the CFA of p′, then Φ_{cf}^{let.β}(Ĉ_{cf}, ρ̂_{cf}) = (Ĉ′_{cf}, ρ′_{cf}) and Ψ_{cf}^{let.β}(Ĉ′_{cf}, ρ′_{cf}) = (Ĉ_{cf}, ρ̂_{cf}).

Lemma 4.2 says that the result of the CFA is preserved by a linear let.β reduction.

4.1.2 Linear let.β reduction and BTA

We show that a linear let.β reduction may improve the results of the BTA. Let p and p′ be as defined in the previous section. We show that the least binding times of p′ are as good and possibly better than the binding times of p.

We define the function Φ_{bt}^{let.β} : (Cache_{bt}^{p} × Env_{bt}^{p}) → (Cache_{bt}^{p′} × Env_{bt}^{p′}) as

Φ_{bt}^{let.β}(Ĉ_{bt}, ρ̂_{bt}) = (Ĉ_{bt}|_{Lab}_{p′} , ρ′_{bt}|_{Var}_{p′})

Lemma 4.3 If (Ĉ_{bt}, ρ̂_{bt}) ⊨_{cf}^{p} p then Φ_{bt}^{let.β}(Ĉ_{bt}, ρ̂_{bt}) ⊨_{cf}^{p′} p′.

Lemma 4.3 says that the binding times are not worsened by a linear let.β reduction. Yet the analysis can yield strictly better results after a linear let.β reduction. In some cases, the binding times of the reduced program are strictly better than the binding times of the initial program.

For example, the call-by-value embedding of the term (λx.2) z followed by one linear let.β reduction yields the term:

let x_{1} = z in
let x_{2} = (λx.2) x_{1} in x_{2}

Considering z to be dynamic, the let-rule forces the variable x_{2} to be dynamic. Therefore, the constant 2 has to be dynamic as well, and, consequently, it will be residualized at specialization time. In contrast, after one more (linear) let.β reduction we obtain the term

let x_{2} = (λx.2) z in x_{2}

and we can see that, in a global static context, the value 2 is no longer coerced to be dynamic.

The context coherence constraint seems unjustified in the above case since evaluating the variable z has no side effects. But it is the call-by-value embedding which forces the variable z into a computation. The BTA has to impose the constraint in such cases as well [16]. At any rate, this initial loss of precision is avoided by performing the second let.β reduction.

In the next section we show that disabling the context coherence constraints leads to no loss or gain in the precision of the binding times.

4.1.3 Linear let.β reduction and BTA^{⋆}

Let us show that the context coherence constraints from the standard BTA are the source of the benefit obtained by a linear let.β reduction. To do so, we show that a linear let.β reduction does not alter the results of the binding-time analysis for continuation-based partial evaluation, BTA^{⋆}. We use the constructive technique outlined in Section 3. The function Φ_{bt^{⋆}}^{let.β} : (Cache_{bt}^{p} × Env_{bt}^{p}) → (Cache_{bt}^{p′} × Env_{bt}^{p′}) is identical to the one from Section 4.1.2. The function Ψ_{bt^{⋆}}^{let.β} : (Cache_{bt}^{p′} × Env_{bt}^{p′}) → (Cache_{bt}^{p} × Env_{bt}^{p}) is defined similarly to Ψ_{cf}^{let.β} in Section 4.1.1. It is immediate to show that Ψ_{bt^{⋆}}^{let.β} ∘ Φ_{bt^{⋆}}^{let.β} = id and Φ_{bt^{⋆}}^{let.β} ∘ Ψ_{bt^{⋆}}^{let.β} = id. The following lemma is a direct consequence:

Lemma 4.4 If (Ĉ_{bt}, ρ̂_{bt}) is the least solution of the BTA^{⋆} of p and (Ĉ′_{bt}, ρ′_{bt}) is the least solution of the BTA^{⋆} of p′, then Φ_{bt^{⋆}}^{let.β}(Ĉ_{bt}, ρ̂_{bt}) = (Ĉ′_{bt}, ρ′_{bt}) and Ψ_{bt^{⋆}}^{let.β}(Ĉ′_{bt}, ρ′_{bt}) = (Ĉ_{bt}, ρ̂_{bt}).

Lemma 4.4 says that the binding times obtained with BTA^{⋆} are preserved by a linear let.β reduction.

4.2 Let flattening

We show that a let.assoc reduction has no effect on the CFA and on BTA^{⋆}, and that it can improve and will not degrade the results of the standard BTA.

4.2.1 Let flattening and CFA

Let us show that a let.assoc reduction does not alter the results of the CFA. Let p be a properly labeled program as a let context E such that

p = E[(let x_{1} = (let x = s in e_{1}^{ℓ_{1}})^{ℓ} in e_{2}^{ℓ_{2}})^{ℓ_{3}}]

Let p′ be the program p after reassociating the let constructs:

p′ = E[(let x = s in (let x_{1} = e_{1}^{ℓ_{1}} in e_{2}^{ℓ_{2}})^{ℓ_{4}})^{ℓ_{3}}]

It is immediate to see that p′ is a properly labeled program.

Again, we show that the least solution of the flow analysis of p is equivalent to the least solution of the analysis of p′. The least solution for p′ is obtained from the least solution for p by projection on the labels and variables preserved by the transformation.

As in Section 4.1.1, we define the following functions:

• Φ_{cf}^{let.assoc} : (Cache_{cf}^{p} × Env_{cf}^{p}) → (Cache_{cf}^{p′} × Env_{cf}^{p′}) such that

Φ_{cf}^{let.assoc}(Ĉ_{cf}, ρ̂_{cf}) = (Ĉ_{cf}|_{Lab^{p}\{ℓ}} ⊔ [ℓ_{4} ↦ Ĉ_{cf}(ℓ_{2})], ρ̂_{cf}).

• Ψ_{cf}^{let.assoc} : (Cache_{cf}^{p′} × Env_{cf}^{p′}) → (Cache_{cf}^{p} × Env_{cf}^{p′}) such that

Ψ_{cf}^{let.assoc}(Ĉ′_{cf}, ρ′_{cf}) = (Ĉ′_{cf}|_{Lab^{p′} \{ℓ_{4}}} ⊔ [ℓ ↦ Ĉ′_{cf}(ℓ_{1})], ρ′_{cf}).

The two functions mediate between solutions of the analysis of p and p′.

Lemma 4.5 If (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} p then Φ_{cf}^{let.assoc}(Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p′} p′, and if (Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p′} p′ then Ψ_{cf}^{let.assoc}(Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p} p.

Following the constructive technique from Section 3, we can easily prove the following lemma.

Lemma 4.6 If (Ĉ_{cf}, ρ̂_{cf}) is the least solution of the CFA of p and (Ĉ′_{cf}, ρ′_{cf}) is the least solution of the CFA of p′, then Φ_{cf}^{let.assoc}(Ĉ_{cf}, ρ̂_{cf}) = (Ĉ′_{cf}, ρ′_{cf}) and Ψ_{cf}^{let.assoc}(Ĉ′_{cf}, ρ′_{cf}) = (Ĉ_{cf}, ρ̂_{cf}).

Lemma 4.6 says that the result of the CFA is preserved by let flattening.

4.2.2 Let flattening and BTA

Let us show that an isolated let flattening may improve the results of the BTA. Let p and p′ be as defined in Section 4.2.1.

Again, we show that for any binding times of p there exist equivalent binding times of p′. We define the function Φ_{bt}^{let.assoc} : (Cache_{bt}^{p} ×Env_{bt}^{p}) → (Cache_{bt}^{p} ×Env_{bt}^{p}) such that

Φ_{bt}^{let.assoc}(Ĉ_{bt}, ρ̂_{bt}) = (Ĉ_{bt}|_{Lab^{p}\{ℓ}} ⊔ [ℓ_{4} ↦ Ĉ_{bt}(ℓ_{2})], ρ̂_{bt}).

Obviously Φ_{bt}^{let.assoc}(Ĉ_{bt}, ρ̂_{bt}) is the equivalent of (Ĉ_{bt}, ρ̂_{bt}). The following lemma shows that Φ_{bt}^{let.assoc} constructs valid solutions.

Lemma 4.7 If (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} p then Φ_{bt}^{let.assoc}(Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p′} p′.

Since Φ_{bt}^{let.assoc} constructs valid equivalent solutions, by the considerations of Section 3, it follows that the binding times are not worsened by a let-flattening. The analysis, however, can yield strictly better results. In some cases, the binding times after a let-flattening are strictly better than the binding times of the initial program.

For example, the call-by-value embedding of the program succ((λx.2) (pred(z))), after a few let.β and one let.assoc reductions, leads to:

let x_{1} = let x_{2} = pred(z) in let x_{3} = (λx.2) x_{2} in x_{3}
in let x_{4} = succ(x_{1}) in x_{4}

The program above reassociates to:

let x_{2} = pred(z)
in let x_{1} = let x_{3} = (λx.2) x_{2} in x_{3}
in let x_{4} = succ(x_{1}) in x_{4}

In the first program, the let rule forces x_{1} to be dynamic and the succ(x_{1}) computation is dynamic. In the second program x_{1} can be static, and the succ(x_{1}) computation may be performed statically, and only its result (3) will be residualized.

4.2.3 Let flattening and BTA^{⋆}

Let us show that for the let.assoc reduction (similarly to the let.β reduction in Section 4.1.3), all binding-time improvements come from the context coherence constraints. To do so, we show that a let.assoc reduction has no effect on the binding-time analysis for continuation-based partial evaluation BTA^{⋆}.

Taking p and p′ as defined in Section 4.2.1, we define two functions Φ_{bt^{⋆}}^{let.assoc} : (Cache_{bt}^{p} × Env_{bt}^{p}) → (Cache_{bt}^{p′} × Env_{bt}^{p′}) and Ψ_{bt^{⋆}}^{let.assoc} : (Cache_{bt}^{p′} × Env_{bt}^{p′}) → (Cache_{bt}^{p} × Env_{bt}^{p}) which map solutions of BTA^{⋆} for p into solutions of BTA^{⋆} for p′ and vice-versa. The functions are essentially defined as in Section 4.2.1. One can show that Φ_{bt^{⋆}}^{let.assoc} ∘ Ψ_{bt^{⋆}}^{let.assoc} = id and Φ_{bt^{⋆}}^{let.assoc} ∘ Ψ_{bt^{⋆}}^{let.assoc} = id. The following lemma is an immediate consequence:

Lemma 4.8 If (Ĉ_{bt}, ρ̂_{bt}) is the least solution of the BTA^{⋆} of p and (Ĉ′_{bt}, ρ′_{bt}) is the least solution of the BTA^{⋆} of p′, then Φ_{bt^{⋆}}^{let.assoc}(Ĉ_{bt}, ρ̂_{bt}) = (Ĉ′_{bt}, ρ′_{bt}) and Ψ_{bt^{⋆}}^{let.assoc}(Ĉ′_{bt}, ρ′_{bt}) = (Ĉ_{bt}, ρ̂_{bt}).

4.3 Summary and conclusions

We have shown that, once the input program is embedded into the computational metalanguage, let.β and let.assoc-normalization can yield binding-time improvements. At the same time linear let.β and let.assoc preserve the quality of flow information. This property confirms that monadic normal forms are a valuable intermediate representation in a program transformer and in an optimizing compiler.

p ∈ Pgm ::= e^{ℓ}
e ∈ Exp ::= t | let x = s in e^{ℓ}
s ∈ Step ::= t_{0}^{ℓ_{0}} t_{1}^{ℓ_{1}} | op(t^{ℓ}) | if0 t^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}}
t ∈ Triv ::= n | x | λ^{π}x.e^{ℓ} | rec^{π}f(x).e^{ℓ}

Figure 13: Λ_{mnf} : The subset of Λ_{v} normalized with respect to let.β and let.assoc

[[e]]^{Pgm} = λk.[[e]]^{Exp}k  where k is fresh
[[n]]^{Triv} = n
[[x]]^{Triv} = x
[[λx.e]]^{Triv} = λx.λk.[[e]]^{Exp}k  where k is fresh
[[rec f(x).e]]^{Triv} = rec f(x).λk.[[e]]^{Exp}k where k is fresh
[[t]]^{Exp}k = k [[t]]^{Triv}
[[let x = t_{0} t_{1} in e]]^{Exp}k = [[t_{0}]]^{Triv} [[t_{1}]]^{Triv} λx.[[e]]^{Exp}k
[[let x = op(t) in e]]^{Exp}k = õp [[t]]^{Triv} λx.[[e]]^{Exp}k
[[let x = if0 t e_{0} e_{1} in e]]^{Exp}k = let k_{1} = λx.[[e]]^{Exp}k
in if0 [[t]]^{Triv} ([[e_{0}]]^{Exp}k_{1}) ([[e_{1}]]^{Exp}k_{1})

where k_{1} is fresh

Figure 14: Introducing continuations

5 Introducing continuations

The language resulting from normalizing terms in Λ_{v} under the let.β and let.assoc reductions is the language Λ_{mnf} defined in Figure 13. The effect of the normalization is to eliminate naming of trivial values and to flatten all nested computations. Therefore, in Λ_{mnf} a computational step can no longer be a trivial value or a nested computation.

The language Λ_{mnf} is the support for introducing continuations by the transformation shown in Figure 14. Introducing continuations leads to terms in a CPS language.^{3} CPS is a restriction of direct style. In order to use the same program analysis, we therefore embed the CPS language into the Λ_{v} language. For example, applications are transformed into let-expressions that name partially applied CPS λ-abstractions and intermediate computations. Figure 15 displays the corresponding CPS transformation and embedding.^{4} (We have omitted the labels, because they only matter in the following sections. Suffice it to say that we label each CPS trivial term with the same label as its direct-style counterpart.)

We can apply now the constraint-based analyses of Section 2 on both the (let.β + let.assoc)-normalized program and on its CPS counterpart given by the transformation of Figure 15.

3In Figure 14, _{op} is the CPS counterpart of op, to ensure evaluation-order independence [38].

4In Figure 15, we use op instead of _{op} since the direct-style language is call-by-value.

[[e]]^{Pgm} = λk.[[e]]^{Exp}k  where k is fresh
[[n]]^{Triv} = n
[[x]]^{Triv} = x
[[λx.e]]^{Triv} = λx.λk.[[e]]^{Exp}k  where k is fresh
[[rec f(x).e]]^{Triv} = rec f(x).λk.[[e]]^{Exp}k  where k is fresh
[[t]]^{Exp}k = let x = k [[t]]^{Triv} in x  where x is fresh
[[let x = t_{0} t_{1} in e]]^{Exp}k = let x_{0} = [[t_{0}]]^{Triv} [[t_{1}]]^{Triv}
in let x_{1} = x_{0} λx.[[e]]^{Exp}k in x_{1}

where x_{0} and x_{1} are fresh

[[let x = op(t) in e]]^{Exp}k = let x = op([[t]]^{Triv}) in [[e]]^{Exp}k

[[let x = if0 t e_{0} e_{1} in e]]^{Exp}k = let k_{1} = λx.[[e]]^{Exp}k in let x_{1} = if0 [[t]]^{Triv} ([[e_{0}]]^{Exp}k_{1}) ([[e_{1}]]^{Exp}k_{1})

in x_{1}

where k_{1} and x_{1} are fresh

Figure 15: Introducing continuations and embedding into the Λ_{v} language

6 Control-flow analysis and the introduction of continuations

In order to compare the results of the CFA before and after introducing continuations, we follow the constructive technique outlined in Section 3. Therefore, the rest of this section is organized as follows. First, we show how to CPS-transform control-flow information (Section 6.1). Given a direct-style program p and an arbitrary solution of its associated analysis (Ĉ_{cf}, ρ̂_{cf}), we construct a solution (Ĉ′_{cf}, ρ′_{cf}) of the analysis associated to p′, the CPS counterpart of p. We ensure that the construction Φ_{cf}^{CPS} builds a valid solution (Section 6.2). We present a converse transformation, Ψ_{cf}^{CPS} (Section 6.3), which we also prove to be correct (Section 6.4). We then show that the two constructions preserve leastness (Section 6.5).

6.1 CPS transformation of control flow

Given a solution (Ĉ_{cf}, ρ̂_{cf}) of the analysis of a program p (i.e., a cache-environment pair such that (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} p holds), we now construct in linear time a solution (Ĉ′_{cf}, ρ′_{cf}) of the analysis of p′ = [[p]]^{Pgm}, the CPS counterpart of p (i.e., such that (Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p′} p′ holds). By analogy, we refer to the construction of (Ĉ′_{cf}, ρ′_{cf}) out of (Ĉ_{cf}, ρ̂_{cf}) as the CPS transformation of (Ĉ_{cf}, ρ̂_{cf}) into (Ĉ′_{cf}, ρ′_{cf}).

As mentioned in Section 2.1, we have designed the CPS transformation on labeled terms so that it preserves the labels of each trivial term. In addition, each directstyle λ-abstraction is annotated with the same label as its CPS counterpart. As a consequence, the abstract values in direct style are included into the abstract values in CPS, i.e., Lam^{p} ⊆ Lam^{p′} and Val_{cf}^{p} ⊆ Val_{cf}^{p′}. When introducing continuations, all the variables defined in the original direct-style program are preserved. Therefore Var^{p} ⊆ Var^{p′}. In essence, we construct a solution for the CPS program such that the flow information assigned to the variables and to the trivial terms preserved by the transformation is identical to the information found in the direct-style solution.

We also assign flow information to the newly introduced terms and variables, in particular to continuation abstractions and continuation identifiers. To this end, we use two auxiliary functions γ and ξ.

• γ extracts the labels of partially applied CPS λ-abstractions. Formally, given A a set of λ-abstractions from the program p′, γ(A) is defined as the set of λ-abstrac-tions λ^{π^{1}}k.e^{ℓ} such that λ^{π}x.λ^{π^{1}}k.e^{ℓ} ∈ A or such that rec^{π}f(x).λ^{π^{1}}k.e^{ℓ} ∈ A.

• ξ assigns flow information to each continuation identifier k introduced by the CPS transformation of p (at λ-abstractions and recursive function definitions). This information can be obtained from the direct-style flow information, since we can syntactically identify the continuation of the CPS counterpart of any direct-style application. Given p, Ĉ_{cf}, ρ̂_{cf}, and a continuation identifier k introduced by the transformation of a λ-abstraction from p:

[[λ^{π_{1}}x.e]]^{Triv} = λ^{π_{1}}x.λk.[[e]]^{Exp}k

we gather in ξ(k) all the continuations that are passed at the program points where λ^{π_{1}}x.e can be applied. Formally, ξ(k) is defined as the set of all labels π such that in the CPS transformation of p into p′ there exists a transformation step

[[let x = t_{0}^{ℓ_{0}} t_{1} in e]]^{Exp}k_{1} = let x_{0} = [[t_{0}^{ℓ_{0}}]]^{Triv} [[t_{1}]]^{Triv} in let x_{1} = x_{0} λ^{π}x.[[e]]^{Exp}k_{1} in x_{1}

such that π_{1} ∈ Ĉ_{cf}(ℓ_{0}). We make a similar definition for the continuation identifiers introduced at recursive function definitions.

Using γ and ξ, we define (Ĉ′_{cf}, ρ′_{cf}) inductively, following Figure 16. In the right part, for each CPS-transformation step, we assign flow values into Ĉ′_{cf} and ρ′_{cf} using previously defined values.

The construction of flow information defines a function

Φ_{cf}^{CPS} : (Cache_{cf}^{p} × Env_{cf}^{p}) → (Cache_{cf}^{p} × Env_{cf}^{p}).

It is easy to show that Φ_{cf}^{CPS} is monotone.

6.2 Correctness of the transformation

Let us show that the cache-environment pair constructed by Φ_{cf}^{CPS} is indeed a valid solution of the analysis of the CPS counterpart of p.

Theorem 6.1 Given a direct-style program p and its CPS counterpart p′ = [[p]]^{Pgm}, let (Ĉ_{cf}, ρ̂_{cf}) be a solution of the CFA of p (i.e., such that (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} p holds) and let (Ĉ′_{cf}, ρ′_{cf}) = Φ_{cf}^{CPS}(Ĉ_{cf}, ρ̂_{cf}). Then (Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p′} p′ holds.

[[e^{ℓ}]]^{Pgm} = (λ^{π}k.[[e^{ℓ}]]^{Exp}k)^{ℓ_{0}}  Ĉ′_{cf}(ℓ_{0}) = {π} ρ′_{cf}(k) = ∅
[[n^{ℓ}]]^{Triv} = n^{ℓ}  Ĉ′_{cf}(ℓ) = Ĉ_{cf}(ℓ)
[[x^{ℓ}]]^{Triv} = x^{ℓ}  Ĉ′_{cf}(ℓ) = Ĉ_{cf}(ℓ)
[[(λ^{π}x.e^{ℓ_{0}})^{ℓ}]]^{Triv} = (λ^{π}x.(λ^{π_{1}}k.[[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}})^{ℓ}
Ĉ′_{cf}(ℓ) = Ĉ_{cf}(ℓ) Ĉ′_{cf}(ℓ_{2}) = {π_{1}}
ρ′_{cf}(x) = ρ̂_{cf}(x) ρ′_{cf}(k) = ξ(k)
[[(rec^{π}f(x).e^{ℓ_{0}})^{ℓ}]]^{Triv} = (rec^{π}f(x).(λ^{π_{1}}k.[[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}})^{ℓ}
Ĉ′_{cf}(ℓ) = Ĉ_{cf}(ℓ) Ĉ′_{cf}(ℓ_{2}) = {π_{1}}
ρ′_{cf}(x) = ρ̂_{cf}(x) ρ′_{cf}(f) = ρ̂_{cf}(f) ρ′_{cf}(k) = ξ(k)
[[t^{ℓ}]]^{Exp}k = (let x = k^{ℓ_{0}} [[t^{ℓ}]]^{Triv} in x^{ℓ_{1}})^{ℓ_{2}}
Ĉ′_{cf}(ℓ_{0}) = ρ′_{cf}(k)
Ĉ′_{cf}(ℓ_{2}) = Ĉ′_{cf}(ℓ_{1}) = ρ′_{cf}(x) = ∅

\begin{aligned}[ \\ [ & \begin{matrix}(let x = t_{0}^{ℓ_{0}} t_{1}^{ℓ_{1}} \\ in e^{ℓ})^{ℓ_{2}} \end{matrix} & ] \\ & ] \end{aligned}^{Exp} k = (let x_{0} = [[t_{0}^{ℓ_{0}}]]^{Triv} [[t_{1}^{ℓ_{1}}]]^{Triv} in (let x_{1} = x_{0}^{ℓ_{3}} (λ^{π}x.[[e^{ℓ}]]^{Exp}k)^{ℓ_{4}} in x_{1}^{ℓ_{5}})^{ℓ_{6}})^{ℓ_{7}}

Ĉ′_{cf}(ℓ_{3}) = ρ′_{cf}(x_{0}) = γ(Ĉ_{cf}(ℓ_{0}))
Ĉ′_{cf}(ℓ_{4}) = {π} ρ′_{cf}(x) = ρ̂_{cf}(x)
Ĉ′_{cf}(ℓ_{7}) = Ĉ′_{cf}(ℓ_{6}) = Ĉ′_{cf}(ℓ_{5}) = ρ′_{cf}(x_{1}) = ∅

\begin{matrix}[ \\ [ & \begin{matrix}(let x = op(t^{ℓ}) \\ in e^{ℓ_{0}})^{ℓ_{1}} \end{matrix} & ] \\ ] \end{matrix}^{Exp} k = (let x = op([[t^{ℓ}]]^{Triv}) in [[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}}
ρ′_{cf}(x) = ρ̂_{cf}(x) Ĉ′_{cf}(ℓ_{2}) = ∅

[ ; [\begin{matrix}(let x = \\ if0 t^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ] ; ]^{Exp} k =

(let k_{1} = (λ^{π}x.[[e^{ℓ_{2}}]]^{Exp}k)^{ℓ_{4}} in
(let x_{1} = if0 [[t^{ℓ}]]^{Triv} ([[e_{0}^{ℓ_{0}}]]^{Exp}k_{1}) ([[e_{1}^{ℓ_{1}}]]^{Exp}k_{1})
in x_{1}^{ℓ_{5}})^{ℓ_{6}})^{ℓ_{7}}
ρ′_{cf}(k_{1}) = Ĉ′_{cf}(ℓ_{4}) = {π} ρ′_{cf}(x) = ρ̂_{cf}(x)
Ĉ′_{cf}(ℓ_{7}) = Ĉ′_{cf}(ℓ_{6}) = Ĉ′_{cf}(ℓ_{5}) = ρ′_{cf}(x_{1}) = ∅

Figure 16: Transformation of control flow from direct style to CPS

Under the assumptions of the theorem, we start by observing three immediate properties of the flow transformation.

Lemma 6.2 For all variables x in p, ρ′_{cf}(x) = ρ̂_{cf}(x); for all trivial terms t^{ℓ} in p, Ĉ′_{cf}(ℓ) = Ĉ_{cf}(ℓ); and for all expressions e^{ℓ} in p′, Ĉ′_{cf}(ℓ) = ∅.

For an arbitrary expression, we define the notion of return label to capture the return point from which CFA collects flow information, as shown just below in Lemma 6.3.

Definition 6 Given a labeled expression e^{ℓ} ∈ Exp, we define the return label R[[e^{ℓ}]] of e^{ℓ} by structural induction as follows:

\begin{aligned}R[[t^{ℓ}]] & = & ℓ \\ R[[(let x = s in e^{ℓ_{1}})^{ℓ}]] & = & R[[e^{ℓ_{1}}]] \end{aligned}

Lemma 6.3 Let e^{ℓ} be an arbitrary subexpression of p. Then Ĉ_{cf}(R[[e^{ℓ}]]) ⊆ Ĉ_{cf}(ℓ).

A return label identifies the point where a continuation is called in the CPStransformed program. Return labels thus provide a syntactic connection between the points where flow information is collected in direct style and the points where flow information is sent to continuations in CPS.

Lemma 6.4 Let k be a continuation identifier introduced by the CPS transformation of a λ-abstraction from p:

[[λ^{π_{1}}x_{1}.e^{ℓ_{0}}]]^{Triv} = λ^{π_{1}}x_{1}.λk.[[e^{ℓ_{0}}]]^{Exp}k

Then, for each λ^{π}x.e^{ℓ_{1}} ∈ ρ′_{cf}(k), Ĉ_{cf}(R[[e^{ℓ_{0}}]]) ⊆ ρ′_{cf}(x). Let k be a continuation identifier introduced by the CPS transformation of a recursive function definition from p:

[[rec^{π_{1}}f(x_{1}).e^{ℓ_{0}}]]^{Triv} = rec^{π_{1}}f(x_{1}).λk.[[e^{ℓ_{0}}]]^{Exp}k

Then, for each λ^{π}x.e^{ℓ_{1}} ∈ ρ′_{cf}(k), Ĉ_{cf}(R[[e^{ℓ_{0}}]]) ⊆ ρ′_{cf}(x).

Let us consider the first case. By the definition of ξ, the only possibility such that λ^{π}x.e^{ℓ_{1}} ∈ ρ′_{cf}(k) is that the function is the continuation of an application point where λ^{π_{1}}x_{1}.e^{ℓ_{0}} is applied. Focusing on the application point, we show that Ĉ_{cf}(ℓ_{0}) ⊆ ρ̂_{cf}(x) = ρ′_{cf}(x). From Lemma 6.3, Ĉ_{cf}(R[[e^{ℓ_{0}}]]) ⊆ Ĉ_{cf}(ℓ_{0}).

The proof of Theorem 6.1 is sketched in Appendix A.

6.3 Reversing the transformation

In the previous section we have shown that direct-style flow information can be transformed into CPS flow information. We can also show that any result of the analysis of a CPS-transformed program can be matched by a result of the analysis of its directstyle counterpart. Using again the structure given by the CPS transformation, we exhibit a direct-style flow transformation. Given a direct-style program p and its CPS counterpart p′, and given (Ĉ′_{cf}, ρ′_{cf}) a valid solution of the analysis on p′, we recover in linear time a valid solution (Ĉ_{cf}, ρ̂_{cf}) of the analysis of p.

Recovering a direct-style solution is straightforward. For variables and trivial terms in p, we are only “filtering out” the labels of continuations from the results of the analysis of p′. We define the direct-style solution by induction on the CPS transformation, following Figure 17. In the right part, for each CPS-transformation step, we assign flow values into Ĉ_{cf} and ρ̂_{cf}. The left parts of Figures 16 and 17 are identical.

We can show that Figure 17 defines another function

Ψ_{cf}^{CPS} : (Cache_{cf}^{p} × Env_{cf}^{p}) → (Cache_{cf}^{p} × Env_{cf}^{p}).

It is also easy to show that, like Φ_{cf}^{CPS} in Section 6.2, Ψ_{cf}^{CPS} is monotone.

[[e^{ℓ}]]^{Pgm} = (λ^{π}k.[[e^{ℓ}]]^{Exp}k)^{ℓ_{0}}
[[n^{ℓ}]]^{Triv} = n^{ℓ}  Ĉ_{cf}(ℓ) = Ĉ′_{cf}(ℓ) ∩ Lam^{p}
[[x^{ℓ}]]^{Triv} = x^{ℓ}  Ĉ_{cf}(ℓ) = Ĉ′_{cf}(ℓ) ∩ Lam^{p}
[[(λ^{π}x.e^{ℓ_{0}})^{ℓ}]]^{Triv} = (λ^{π}x.(λ^{π_{1}}k.[[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}})^{ℓ}
Ĉ_{cf}(ℓ) = Ĉ′_{cf}(ℓ) ∩ Lam^{p} ρ̂_{cf}(x) = ρ′_{cf}(x) ∩ Lam^{p}
[[(rec^{π}f(x).e^{ℓ_{0}})^{ℓ}]]^{Triv} = (rec^{π}f(x).(λ^{π_{1}}k.[[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}})^{ℓ}
Ĉ_{cf}(ℓ) = Ĉ′_{cf}(ℓ) ∩ Lam^{p} ρ̂_{cf}(x) = ρ′_{cf}(x) ∩ Lam^{p}
ρ̂_{cf}(f) = ρ′_{cf}(f) ∩ Lam^{p}
[[t^{ℓ}]]^{Exp}k = (let x = k^{ℓ_{0}} [[t^{ℓ}]]^{Triv} in x^{ℓ_{1}})^{ℓ_{2}}

\begin{aligned}[ \\ [ & \begin{matrix}(let x = t_{0}^{ℓ_{0}} t_{1}^{ℓ_{1}} \\ in e^{ℓ})^{ℓ_{2}} \end{matrix} & ] \\ & ] \end{aligned}^{Exp} k = (let x_{0} = [[t_{0}^{ℓ_{0}}]]^{Triv} [[t_{1}^{ℓ_{1}}]]^{Triv} in (let x_{1} = x_{0}^{ℓ_{3}} (λ^{π}x.[[e^{ℓ}]]^{Exp}k)^{ℓ_{4}} in x_{1}^{ℓ_{5}})^{ℓ_{6}})^{ℓ_{7}}

Ĉ_{cf}(ℓ_{2}) = Ĉ_{cf}(ℓ) ρ̂_{cf}(x) = ρ′_{cf}(x) ∩ Lam^{p}

\begin{matrix}[ \\ [ & \begin{matrix}(let x = op(t^{ℓ}) \\ in e^{ℓ_{0}})^{ℓ_{1}} \end{matrix} & ] \\ ] \end{matrix}^{Exp} k = (let x = op([[t^{ℓ}]]^{Triv}) in [[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}}
Ĉ_{cf}(ℓ_{1}) = Ĉ_{cf}(ℓ_{0}) ρ̂_{cf}(x) = ρ′_{cf}(x) ∩ Lam^{p}

[ ; [\begin{matrix}(let x = \\ if0 t^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ] ; ]^{Exp} k =

(let k_{1} = (λ^{π}x.[[e^{ℓ_{2}}]]^{Exp}k)^{ℓ_{4}} in
(let x_{1} = if0 [[t^{ℓ}]]^{Triv} ([[e_{0}^{ℓ_{0}}]]^{Exp}k_{1}) ([[e_{1}^{ℓ_{1}}]]^{Exp}k_{1})
in x_{1}^{ℓ_{5}})^{ℓ_{6}})^{ℓ_{7}}
Ĉ_{cf}(ℓ_{3}) = Ĉ_{cf}(ℓ_{2}) ρ̂_{cf}(x) = ρ′_{cf}(x) ∩ Lam^{p}

Figure 17: Transformation of control flow from CPS to direct style

6.4 Correctness of the reverse transformation

Let us show that the reverse transformation indeed yields a valid solution of the analysis of the original program.

Theorem 6.5 Given a direct-style program p and its CPS counterpart p′ = [[p]]^{Pgm}, let (Ĉ′_{cf}, ρ′_{cf}) be a solution of the CFA of p′ (i.e., such that (Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p′} p′ holds) and let (Ĉ_{cf}, ρ̂_{cf}) = Ψ_{cf}^{CPS}(Ĉ′_{cf}, ρ′_{cf}). Then (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} p holds.

As in Section 6.2, we use intermediate results to prove Theorem 6.5. Working under the assumptions of the theorem, we observe two immediate properties of the reverse transformation:

Lemma 6.6 For all x ∈ Var^{p}, ρ̂_{cf}(x) = ρ′_{cf}(x) ∩ Lam^{p}; and for all trivial terms t^{ℓ} in p, Ĉ_{cf}(ℓ) = Ĉ′_{cf}(ℓ) ∩ Lam^{p}.

For an arbitrary expression, the new solution collects all the flow information from the return point of the expression.

Lemma 6.7 Let e^{ℓ} be an expression in p. Then Ĉ_{cf}(ℓ) = Ĉ_{cf}(R[[e^{ℓ}]]).

As a parallel of Lemma 6.4, the following lemma connects the flow at the return points of functions with the flow collected for the variables declared by continuations.

Lemma 6.8 Let k be a continuation identifier introduced by the transformation of a λ-abstraction from p:

[[λ^{π_{1}}x_{1}.e^{ℓ_{0}}]]^{Triv} = λ^{π_{1}}x_{1}.λk.[[e^{ℓ_{0}}]]^{Exp}k

Then, for each λ^{π}x.e^{ℓ_{1}} ∈ ρ′_{cf}(k), Ĉ_{cf}(R[[e^{ℓ_{0}}]]) ⊆ ρ′_{cf}(x). Let k be a continuation identifier introduced by the transformation of a recursive function definition from p:

[[rec^{π_{1}}f(x_{1}).e^{ℓ_{0}}]]^{Triv} = rec^{π_{1}}f(x_{1}).λk.[[e^{ℓ_{0}}]]^{Exp}k

Then, for each λ^{π}x.e^{ℓ_{1}} ∈ ρ′_{cf}(k), Ĉ_{cf}(R[[e^{ℓ_{0}}]]) ⊆ ρ′_{cf}(x).

The proof of Theorem 6.5 is sketched in Appendix A.

6.5 Equivalence of flow

Let p be an arbitrary direct-style program and p′ = [[p]]^{Pgm} its CPS counterpart. By simple unfoldings of definitions, we prove the following lemma.

Lemma 6.9 Given (Ĉ_{cf}, ρ̂_{cf}) a solution of the CFA of p (i.e., such that (Ĉ_{cf}, ρ̂_{cf}) ⊨_{cf}^{p} p holds), Ψ_{cf}^{CPS}(Φ_{cf}^{CPS}(Ĉ_{cf}, ρ̂_{cf})) ⊆ (Ĉ_{cf}, ρ̂_{cf}). Given (Ĉ′_{cf}, ρ′_{cf}) a solution of the CFA of p′, (i.e., such that (Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p′} p′ holds), then it holds that Φ_{cf}^{CPS}(Ψ_{cf}^{CPS}(Ĉ′_{cf}, ρ′_{cf})) ⊆ (Ĉ′_{cf}, ρ′_{cf}).

From these two properties the following main theorem follows directly.

Theorem 6.10 (Equivalence of flow) Given a direct-style program p and its CPS counterpart p′ = [[p]]^{Pgm}, let (Ĉ_{cf}, ρ̂_{cf}) be the least solution of the CFA of p and let (Ĉ′_{cf}, ρ′_{cf}) be the least solution of the CFA of p′. Then Φ_{cf}^{CPS}(Ĉ_{cf}, ρ̂_{cf}) = (Ĉ′_{cf}, ρ′_{cf}) and Ψ_{cf}^{CPS}(Ĉ′_{cf}, ρ′_{cf}) = (Ĉ_{cf}, ρ̂_{cf}).

6.6 Summary and conclusions

Theorem 6.10 shows that the best flow information obtainable by a constraint-based control-flow analysis on a direct-style program is equivalent to the best flow information obtainable by the same analysis on the CPS counterpart of this program and vice versa. Lemma 6.2 and Lemma 6.6 show that the two solutions are equal on the variables and program points common to the two programs. We conclude that, for CFA as defined in Figure 7, no information is lost or gained by the CPS transformation.

7 Binding-time analysis and the introduction of continuations

We describe the effect of the introduction of continuations on the result of the BTA of a program in Λ_{mnf} . First, we define a CPS transformation of binding times (Section 7.1), which we show to be correct and to preserve the quality of the binding times (Section 7.2). Unlike for CFA, however, we show examples where BTA on CPS terms gives more precise results than on the corresponding direct-style terms, thus showing that introducing continuations may lead to more specialization opportunities (Section 7.3). Finally (Section 7.4) we show that if we relax the constraints of the BTA to take into account continuation-based partial evaluation, then, just like CFA, no loss and no gain of information can be observed after the introduction of continuations.

7.1 CPS transformation of binding times

We show that the binding times obtained by analyzing the CPS counterpart of a program are at least as good as the ones obtained by analyzing the original program. We construct in linear time a solution of the BTA over the CPS-transformed program from a solution of the BTA over the original program, such that the quality of the binding times is preserved.

Given the program p and (Ĉ_{bt}, ρ̂_{bt}) a solution of the BTA over p, we define (Ĉ′_{bt}, ρ′_{bt}) as a solution of the BTA over p′, the CPS counterpart of p. The definition is by induction on the introduction of continuations and is given in Figure 18, where the left parts are identical to the left parts of Figures 16 and 17. In the right part, we assign binding times into Ĉ′_{bt} and ρ′_{bt}. As in Section 6, we use Φ_{bt}^{CPS} to denote the function induced by the transformation:

Φ_{bt}^{CPS} : (Cache_{bt}^{p} × Env_{bt}^{p}) → (Cache_{bt}^{p′} × Env_{bt}^{p′}).

7.2 Correctness of the transformation

Let us show that the solution defined in Figure 18 is indeed a valid solution of the BTA. We follow the same technique as in Section 6.2. The correctness of the transformation is established by the following theorem.

Theorem 7.1 Given a direct-style program p and its CPS counterpart p′ = [[p]]^{Pgm}, let (Ĉ_{bt}, ρ̂_{bt}) be an arbitrary solution of the BTA of p (i.e., such that (Ĉ_{bt}, ρ̂_{bt}) ⊨_{bt}^{p} p holds). If (Ĉ′_{bt}, ρ′_{bt}) = Φ_{bt}^{CPS}(Ĉ_{bt}, ρ̂_{bt}) then (Ĉ′_{bt}, ρ′_{bt}) ⊨_{bt}^{p′} p′ holds.

Under the assumption of the theorem, we first observe immediate properties of the CPS transformation of binding times, similar to the ones stated in Lemma 6.2. For instance, the binding time for expressions in CPS is equal to the binding time of the result of the program, which, as mentioned in Section 2.6, is dynamic.

Lemma 7.2 For all variables x in p, ρ′_{bt}(x) = ρ̂_{bt}(x); for all trivial terms t^{ℓ} in p, Ĉ′_{bt}(ℓ) = Ĉ_{bt}(ℓ); and for all expressions e in p′, Ĉ′_{bt}(e) = D.

The binding time of an expression in p is equal to the binding time of its return point.

Lemma 7.3 Let e^{ℓ} be an arbitrary subexpression of p. Then Ĉ_{bt}(R[[e^{ℓ}]]) = Ĉ_{bt}(ℓ).

[[e^{ℓ}]]^{Pgm} = (λ^{π}k.[[e^{ℓ}]]^{Exp}k)^{ℓ_{0}}  Ĉ′_{bt}(ℓ_{0}) = ρ′_{bt}(k) = D
[[n^{ℓ}]]^{Triv} = n^{ℓ}  Ĉ′_{bt}(ℓ) = Ĉ_{bt}(ℓ)
[[x^{ℓ}]]^{Triv} = x^{ℓ}  Ĉ′_{bt}(ℓ) = Ĉ_{bt}(ℓ)
[[(λ^{π}x.e^{ℓ_{0}})^{ℓ}]]^{Triv} = (λ^{π}x.(λ^{π_{1}}k.[[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}})^{ℓ}
Ĉ′_{bt}(ℓ_{2}) = Ĉ_{bt}(ℓ) Ĉ′_{bt}(ℓ) = Ĉ_{bt}(ℓ)
ρ′_{bt}(x) = ρ̂_{bt}(x) ρ′_{bt}(k) = Ĉ_{bt}(ℓ)
[[(rec^{π}f(x).e^{ℓ_{0}})^{ℓ}]]^{Triv} = (λ^{π}x.(rec^{π_{1}}f(k).[[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}})^{ℓ}
Ĉ′_{bt}(ℓ_{2}) = Ĉ_{bt}(ℓ) Ĉ′_{bt}(ℓ) = Ĉ_{bt}(ℓ)
ρ′_{bt}(f) = ρ̂_{bt}(f) ρ′_{bt}(x) = ρ̂_{bt}(x) ρ′_{bt}(k) = Ĉ_{bt}(ℓ)
[[t^{ℓ}]]^{Exp}k = (let x = k^{ℓ_{0}} [[t^{ℓ}]]^{Triv} in x^{ℓ_{1}})^{ℓ_{2}}
Ĉ′_{bt}(ℓ_{0}) = ρ′_{bt}(k)
Ĉ′_{bt}(ℓ_{2}) = Ĉ′_{bt}(ℓ_{1}) = ρ̂_{bt}(x) = D

\begin{aligned}[ \\ [ & \begin{matrix}(let x = t_{0}^{ℓ_{0}} t_{1}^{ℓ_{1}} \\ in e^{ℓ})^{ℓ_{2}} \end{matrix} & ] \\ & ] \end{aligned}^{Exp} k = (let x_{0} = [[t_{0}^{ℓ_{0}}]]^{Triv} [[t_{1}^{ℓ_{1}}]]^{Triv} in (let x_{1} = x_{0}^{ℓ_{3}} (λ^{π}x.[[e^{ℓ}]]^{Exp}k)^{ℓ_{4}} in x_{1}^{ℓ_{5}})^{ℓ_{6}})^{ℓ_{7}}

Ĉ′_{bt}(ℓ_{4}) = Ĉ′_{bt}(ℓ_{3}) = ρ′_{bt}(x_{0}) = Ĉ_{bt}(ℓ_{0})
ρ′_{bt}(x) = ρ̂_{bt}(x) ρ′_{bt}(x_{1}) = D
Ĉ′_{bt}(ℓ_{7}) = Ĉ′_{bt}(ℓ_{6}) = Ĉ′_{bt}(ℓ_{5}) = D

\begin{matrix}[ \\ [ & \begin{matrix}(let x = op(t^{ℓ}) \\ in e^{ℓ_{0}})^{ℓ_{1}} \end{matrix} & ] \\ ] \end{matrix}^{Exp} k = (let x = op([[t^{ℓ}]]^{Triv}) in [[e^{ℓ_{0}}]]^{Exp}k)^{ℓ_{2}}
ρ′_{bt}(x) = ρ̂_{bt}(x) Ĉ′_{bt}(ℓ_{2}) = D

[ ; [\begin{matrix}(let x = \\ if0 t^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} \\ in e^{ℓ_{2}})^{ℓ_{3}} \end{matrix} ] ; ]^{Exp} k =

(let k_{1} = (λ^{π}x.[[e^{ℓ_{2}}]]^{Exp}k)^{ℓ_{4}} in
(let x_{1} = if0 [[t^{ℓ}]]^{Triv} ([[e_{0}^{ℓ_{0}}]]^{Exp}k_{1}) ([[e_{1}^{ℓ_{1}}]]^{Exp}k_{1})
in x_{1}^{ℓ_{5}})^{ℓ_{6}})^{ℓ_{7}}
ρ′_{bt}(k_{1}) = Ĉ′_{bt}(ℓ_{4}) = ρ′_{bt}(x) = ρ̂_{bt}(x)
Ĉ′_{bt}(ℓ_{7}) = Ĉ′_{bt}(ℓ_{6}) = Ĉ′_{bt}(ℓ_{5}) = ρ′_{bt}(x_{1}) = D

Figure 18: Transformation of binding times from direct style to CPS

The flow of the continuation abstractions connects the binding times of the return point of expressions and continuation variables. The binding time of the value abstracted by a continuation is equal to the binding time of any expression that the continuation can be passed to.

Lemma 7.4 Let k be a continuation identifier introduced by the transformation of a λ-abstraction from p:

[[λ^{π_{1}}x_{1}.e^{ℓ_{0}}]]^{Triv} = λ^{π_{1}}x_{1}.λk.[[e^{ℓ_{0}}]]^{Exp}k

Then, for each λ^{π}x.e^{ℓ_{1}} ∈ ρ′_{cf}(k), Ĉ_{bt}(R[[e^{ℓ_{0}}]]) = ρ′_{bt}(x). Let k be a continuation identifier introduced by the transformation of a recursive function definition from p:

[[rec^{π_{1}}f(x_{1}).e^{ℓ_{0}}]]^{Triv} = rec^{π_{1}}f(x_{1}).λk.[[e^{ℓ_{0}}]]^{Exp}k

Then, for each λ^{π}x.e^{ℓ_{1}} ∈ ρ′_{cf}(k), Ĉ_{bt}(R[[e^{ℓ_{0}}]]) = ρ′_{bt}(x).

The proof of Theorem 7.1 is sketched in Appendix A.

Theorem 7.1 and Lemma 7.2 show that we can transform any binding-time solution of a direct-style program into a solution of its CPS counterpart in such a way that the binding times of variables and trivial terms are preserved. This preservation implies that no values are forced to be dynamic just by introducing continuations. It also implies that the static computations (applications, tests or base-type operations) in a direct-style program remain static as well in its CPS counterpart. We thus conclude that the same amount of specialization of the input program can be achieved after introducing continuations.

7.3 Reversing the transformation

We show that it is not always possible to reverse the CPS transformation of binding times. There are cases when the least analysis of a CPS-transformed program produces strictly more static annotations than the least analysis of its direct-style counterpart. Here is a canonical example [16], where succ is the successor function, and the free variable f and z are considered to be dynamic (f might denote a potentially diverging function):

let r = (λ^{π}y.let v = f z in 2) 1 in let r_{1} = succ(r) in r_{1}

In the least solution of the BTA on this term, even if the application of λ^{π}y. … to 1 is classified as static, its result is classified as dynamic because of the dynamic application in the header of its inner let-expression. Thus r is dynamic. Since the second increment operation depends on r, it is dynamic as well. Simply discarding the dynamic computation f z is not meaning-preserving since the computation may diverge.

The CPS counterpart of the canonical example above reads as follows (without embedding it into direct style, for readability):

λk.(λ^{π}y.λk_{1}.f z (λv.k_{1} 2)) 1 (λr.let r_{1} = succ(r) in k r_{1})

The continuation denoted by k_{1} is static, and thus the application k_{1} 2 is performed statically (even if its result is dynamic). Thus, r is static as well, and further computation based on r can be performed at specialization time.

Other binding-time improvements can be obtained when a dynamic test disables further computations based on its result. The canonical example is as follows:

let v = if0 z 0 1 in let v_{1} = succ(v) in v_{1}

It is true that one benefits from such an improvement only by allowing code duplication. But the code duplication takes place at specialization time, not at BTA time. Thus in contrast to Sabry and Felleisen’s analysis [39], the improvement in precision is not due to duplicating the analysis on the two branches.

7.4 Continuation-based partial evaluation

In the two examples above the binding-time improvements come from the context coherence constraints in the specification of the BTA (Figure 9): the body of a let-expression has to be dynamic if the header is dynamic, and both branches of a conditional have to be dynamic if the test is dynamic.

In this section, we show that these contextual coherence constraints are the only ones leading to binding-time improvements. Using the same proof technique as in Section 6, we formally show that introducing continuations has no effect on BTA^{⋆}, i.e., it entails no local increase and also no loss of precision elsewhere in the program: the best binding times in direct style are the best binding times in CPS as well.

More precisely, we can define Φ_{bt^{⋆}}^{CPS}, the CPS transformation of the binding times obtained by BTA^{⋆}. The definition is only a slight modification of the definition of Φ_{bt}^{CPS} in Section 7.1. Given the program p and a solution (Ĉ_{bt}^{⋆}, ρ_{bt}^{⋆}) of BTA^{⋆} (i.e., such that (Ĉ_{bt}^{⋆}, ρ_{bt}^{⋆}) ⊨_{bt^{⋆}}^{p} p holds), we can show that Φ_{bt^{⋆}}^{CPS}(Ĉ_{bt}^{⋆}, ρ_{bt}^{⋆}) ⊨_{bt^{⋆}}^{p′} p′ holds. We can also define the reverse binding-time transformation Ψ_{bt^{⋆}}^{CPS}, which is essentially the same as the reverse flow transformation of Section 6.3 and also operates in linear time: for each term we just extract the binding time of its CPS counterpart. We can show that given a solution (Ĉ′_{bt^{⋆}}, ρ′_{bt^{⋆}}) of BTA^{⋆} for p′ (i.e., such that (Ĉ′_{bt^{⋆}}, ρ′_{bt^{⋆}}) ⊨_{bt^{⋆}}^{p′} p′ holds), Ψ_{bt^{⋆}}^{CPS}(Ĉ′_{bt^{⋆}}, ρ′_{bt^{⋆}}) ⊨_{bt^{⋆}}^{p} p holds too.

We are now in position to connect the binding times in direct style and in CPS as obtained by BTA^{⋆}:

Theorem 7.5 Given a direct-style program p and its CPS counterpart p′ = [[p]]^{Pgm}, let (Ĉ_{bt}^{⋆}, ρ_{bt}^{⋆}) be the least solution of BTA^{⋆} for p and let (Ĉ′_{bt^{⋆}}, ρ′_{bt^{⋆}}) be the least solution of BTA^{⋆} for p′. Then for all variables x in p, ρ_{bt}^{⋆}(x) = ρ′_{bt^{⋆}}(x) and for all trivial terms t^{ℓ} in p, Ĉ_{bt}^{⋆}(ℓ) = Ĉ′_{bt^{⋆}}(ℓ).

We thus conclude that introducing continuations has no effect on the amount of specialization that can be performed when using continuation-based partial evaluation.

7.5 Summary and conclusions

We have shown that, given an input program as a call-by-value encoding of a Λprogram, introducing continuations does not degrade and may improve the results of the BTA for traditional partial-evaluation. We have also shown that introducing continuations does not affect the results of the BTA for continuation-based partial evaluation.

We therefore conclude that, unless one is willing to use continuation-based partial evaluation, a complete CPS transformation of the program is beneficial to the quality of the results of the BTA.

8 Related work

8.1 Program analysis in general

Even though the issue of syntactic accidents is not treated in textbooks and tutorials on program analysis, it appears to be folklore in the program-analysis community. An outstanding recent example is region inference (Section 8.1.1). To some extent, a similar situation occurs in programming practice: who has never modified a program with the sole purpose of improving its performance?

We are only aware of three other studies of the effect of continuations on program analysis: an early work by Nielson [29], Sabry and Felleisen’s PLDI’94 paper [39], and Palsberg and Wand’s recent work [37].

Nielson’s work compares the precision of two data-flow analyses: one based on a direct-style semantics and the other on a continuation semantics. In contrast, we compare the precision of the (same) analysis of a program and of its CPS counterpart. Sabry and Felleisen’s work shows that a CPS transformation leads to incomparable results for a constant propagation analysis (Section 8.1.2). Palsberg and Wand’s work is similar to ours since it involves a CPS transformation of flow information (Section 8.1.3).

8.1.1 Region inference and the CPS transformation

Region inference [44] aims at detecting program points where run-time storage can be deallocated—typically at exit points for blocks and at return points for functions. To overcome syntactic accidents, a programming discipline has therefore been developed to make region inference yield better results.

We note that region improvements and binding-time improvements may come at cross purpose. For example, consider let reassociation:

let x_{2} = \begin{matrix}let x_{1} = e^{ℓ_{1}} \\ in e^{ℓ_{2}} \end{matrix}

in e^{ℓ_{3}} let flattening

[figure] let x_{1} = e^{ℓ_{1}}

in \begin{matrix}let x_{2} = e^{ℓ_{2}} \\ in e^{ℓ_{3}} \end{matrix}

let “deepening”

[figure]

Let flattening allows the region for x_{1} to be released after the region for x_{2}. Let deepening allows the region for x_{1} to be released earlier and requires the region for x_{2} to be allocated earlier. Therefore, let deepening provides a region improvement, especially if e^{ℓ_{3}} contains a recursive call. But on the other hand, and as pointed out by an anonymous reviewer, if e^{ℓ_{1}} contains a recursive call, it is let flattening that provides a region improvement. Similarly, for functions, the CPS transformation yields a binding-time improvement whereas the direct-style transformation yields a region improvement (since in CPS, functions “never return”).

8.1.2 Data-flow analysis and the CPS transformation

In their PLDI’94 paper [39], Sabry and Felleisen have shown that after a CPS transformation, a data-flow analysis may confuse the continuations used at return points, as already noted by Shivers [41, page 33]. An example of confusion of return points is given by the term

let x_{1} = f 1
in \begin{matrix}let x_{2} = f 2 \\ in x_{1} \end{matrix}

and its CPS counterpart

λk.f 1 (λ^{π_{1}}x_{1}.f 2 (λ^{π_{2}}x_{2}.k x_{1}))

analyzed in contexts where f is bound to λx.x and to its CPS counterpart λx.λk_{1}.k_{1} x, respectively. The analysis of the direct-style term starts by examining the first application and detects that x and afterwards x_{1} evaluate to the constant 1. Then, by analyzing the second application, the analysis approximates that the value of x is not constant (it can evaluate to both 1 and 2). The value of x_{2} is also considered unknown. Nevertheless, x_{1} is still considered constant, and the analysis is able to deduce that the whole expression evaluates to the constant 1.

In the CPS program, the analysis of the first application determines that the continuation k_{1} evaluates to π_{1}, and, afterwards, that x_{1} evaluates to 1. After the analysis of the second application, the continuation k_{1} evaluates to both π_{1} and π_{2}. The variable x evaluates to both 1 and 2 and is approximated as unknown. The approximation is passed by the application k_{1} x, into both x_{1} and x_{2}. Therefore, a loss of precision occurs: the result of the whole expression is no longer detected as being a constant.

One can observe, however, that in a constant-propagation analysis the chronological order of the two applications may affect the result. In direct style, the first application of the function f is analyzed in a different context than the second application. Interchanging the two let bindings leads to a different result of the analysis, for an essentially equivalent program. Therefore a limited form of context dependency is built in the constant-propagation analysis considered by Sabry and Felleisen. In contrast, the constraint-based analyses (in the monovariant case) propagate the result of a function at once to all the application sites of this function. These analyses do not exhibit the sequentiality dependency of the constant propagation, and therefore, no precision is lost after a source CPS transformation.

Sabry and Felleisen also present examples where the analysis of a program is improved after the CPS transformation, reflecting that the constant-propagation analysis is not distributive [24, 29]. The improvements are attributed to the fact that the constant-propagation analysis is duplicated over conditional branches (and their corresponding continuations). In contrast, the constraint-based analyses propagate results from one branch of a conditional to another, and therefore, no precision is gained by the CPS transformation.

To summarize, Sabry and Felleisen’s analysis depends on the order in which the source program is traversed and it is duplicated over conditional branches. These two properties led Sabry and Felleisen to conclude that the CPS transformation does not preserve the result of constant propagation. In contrast, our monovariant constraintbased analyses do not depend on the order in which constraints are solved and the analyses are not duplicated over conditional branches. These two properties led us to conclude that the CPS transformation does preserve the results of CFA and of BTA^{⋆}.

8.1.3 CPS transformation of flow information

Recently, Palsberg and Wand have conducted a study of CFA [37], supporting Sabry and Felleisen’s conclusion that the extra precision enabled by the CPS transformation is due to the duplication of the analysis. They developed a CPS transformation of flow information comparable to the one of Figure 16, but independently and prior to us. Palsberg and Wand also mention that least solutions may or may not be preserved by administrative reductions of CPS-transformed programs. In that, they implicitly share our concern about syntactic accidents, even though their primary goal was to transfer Wand’s pioneer results on the CPS transformation of types [26, 45] to the CPS transformation of flow types. Since then, we have shown that least solutions are preserved by administrative reductions of CPS-transformed programs [8, 9].

8.2 Binding-time analysis and the CPS transformation

Binding-time improvements have always been customary for users of binding-time analysis [22, 30]. One of them amounts to considering source programs in CPS [5, 11], which suggests that source programs should be systematically CPS-transformed [4]. (Muylaert-Filho and Burn take the same stand for strictness analysis and the call-by-name CPS transformation [28].)

Essentially, the CPS transformation relocates potentially static contexts inside definitely dynamic contexts (let expressions and conditionals), thereby providing a binding-time improvement. To this end, the CPS transformation itself is continuation-based [12], which paved the way to continuation-based partial evaluation [3, 25].

Hatcliff and Danvy have characterized the full effect of continuation-based partial evaluation as online let flattening in Moggi’s computational metalanguage [16]. This characterization justifies why offline let flattening is also, partially, a binding-time improvement [19]. In any case, offline let flattening is known to be part of the CPS transformation [15].

What had not been shown before, however, and what we have addressed here, is whether such “improvements” worsen binding times elsewhere in a source program.

9 Conclusion and issues

Observing that program analyses are vulnerable to syntactic accidents, we have considered a radical syntactic change: a transformation into CPS. We have studied the interaction between a non-duplicating CPS transformation and two program analyses: control-flow analysis (CFA) and binding-time analysis. Through a systematic construction of the CPS counterpart of flow information, we have found that constraintbased CFA is insensitive to continuation-passing, and that the CPS transformation does improve binding times for traditional partial evaluation. Using the same technique, we have also found that the binding-time analysis for continuation-based partial evaluation is insensitive to the CPS transformation.

These results suggest two further avenues of study:

• In BTA, the beneficial effect of the CPS transformation can be accounted for by disabling the context coherence constraints for let expressions (and for conditionals as well, if one is willing to duplicate static contexts at specialization time). The price of this change, however, is that the corresponding program specializer has to be made continuation-based [16]. We conjecture that the situation is similar, e.g., for security analysis, which has similar let and case rules. Just like BTA, a security analysis thus ought to yield more precise results over CPStransformed programs. We therefore also conjecture that the beneficial effect of the CPS transformation can be accounted for by disabling the context coherence constraints in the let and case rules, if one is willing to develop a corresponding continuation-based processor of security information.

• More generally, as a step towards more robust program analyses that are less vulnerable to syntactic accidents, we need to understand better the programanalysis perspective over syntactic landscapes. Two key questions arise which may be general to program analysis or specific to individual program analyses: which program transformations affect precision? And among those that do, which ones affect precision monotonically? Answering these questions would enable one to develop more reliable program analyses, i.e., program analyses endowed with invariants under program change (be such change a particular type of reduction or other kind of meaning-preserving transformations). Henglein’s invariance properties of polymorphic typing judgments with respect to let unfolding and folding and η-reduction [18] is a step in this direction. Alternatively, one could develop an intermediate language for reasoning about program analysis and program transformation.

Acknowledgments: We are grateful to Andrzej Filinski and Julia L. Lawall for substantial discussions and comments in the course of this work, and to Amr Sabry for extensive comments on the present version of this article. Thanks are also due to Torben Amtoft, Anindya Banerjee, Bernd Grobauer, Dan Hernest, Niels O. Jensen, Torben Mogensen, Lasse R. Nielsen, Morten Rhiger, Olin Shivers, Zhe Yang, and the anonymous reviewers for their feedback.

A Proofs

Proof: 1 (Proof of Theorem 6.1) The proof proceeds by induction on the transformation of p into p′. We sketch the induction steps.

We show that (Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p′} (let x = k^{ℓ_{0}} [[t^{ℓ}]]^{Triv} in x^{ℓ_{1}})^{ℓ_{2}} holds. For an arbitrary continuation λ^{π}y.e^{ℓ_{3}} in the set Ĉ′_{cf}(ℓ_{0}) = ρ′_{cf}(k), we show that two flow constraints are satisfied.

The first constraint is Ĉ′_{cf}(ℓ) ⊆ ρ′_{cf}(y). By Lemma 6.2, Ĉ′_{cf}(ℓ) = Ĉ_{cf}(ℓ). We make a case analysis on the introduction of k by the CPS transformation.

If k is the top-level continuation, then the constraints are vacuously satisfied. If k is introduced by the transformation of a named conditional, then ℓ is the return point of one of the two branches of the test. Obviously Ĉ_{cf}(ℓ) ⊆ ρ′_{cf}(y). Otherwise, k comes from the transformation of a λ-abstraction λ^{π_{1}}x_{1}.e^{ℓ_{4}} from p, such that ℓ = R[[e^{ℓ_{4}}]]. We apply Lemma 6.4.

The second constraint is Ĉ′_{cf}(ℓ_{3}) ⊆ ρ′_{cf}(x). Following Lemma 6.2, it amounts to ∅ ⊆ ∅.

For the rest of the induction steps, the induction hypotheses and the definition of γ suffice to show that the constraints are satisfied.

Proof: 2 (Proof of Theorem 6.5) The proof is by induction on the transformation of p into p′. We sketch the induction steps.

For the transformation step [[t^{ℓ}]]^{Triv}, the constraints follow from the induction hypothesis. The same applies for the transformation step [[t^{ℓ}]]^{Exp}k.

For the transformation of a named application:

[[let x = t_{0}^{ℓ_{3}} t_{1} in e_{2}]]^{Exp}k = let x_{0} = [[t_{0}^{ℓ_{3}}]]^{Triv} [[t_{1}]]^{Triv} in let x_{1} = x_{0} λ^{π}x.e^{ℓ_{2}} in x_{1}

let λ^{π_{1}}y.e_{1}^{ℓ_{4}} be an arbitrary λ-abstraction from p such that π_{1} ∈ Ĉ_{cf}(ℓ_{3}). Let the CPS transformation of the λ-abstraction be λ^{π_{1}}y.λk_{1}.e_{2}. Then π ∈ ρ′_{cf}(k_{1}). From Lemma 6.7 and Lemma 6.8 we obtain that Ĉ_{cf}(ℓ_{4}) ⊆ ρ̂_{cf}(x).

Proof: 3 (Proof of Theorem 7.1) The proof is an adaptation of the proof of Theorem 6.1 to equality constraints. In addition, we need to prove the satisfaction of the additional constraints introduced by BTA. We sketch the induction steps.

We show that (Ĉ′_{cf}, ρ′_{cf}) ⊨_{cf}^{p′} (let x = k^{ℓ_{0}} [[t^{ℓ}]]^{Triv} in x^{ℓ_{1}})^{ℓ_{2}} holds. For this purpose, given an arbitrary λ^{π}x.e^{ℓ_{3}} ∈ Ĉ′_{cf}(ℓ_{0}) = ρ′_{cf}(k) we must show that two equality constraints are satisfied. Similarly to the proof of Theorem 6.10, we make a case analysis on the introduction of k, using Lemma 7.3 and Lemma 7.4 to prove the satisfaction of the constraints.

We also need to show that Ĉ′_{bt}(ℓ_{0}) = D ⇒ Ĉ′_{bt}(ℓ) = D. Again, we make a case analysis on the introduction of k. The top-level case is trivial. The case where k is introduced by the transformation of a function (λy.e_{1}^{ℓ_{5}})^{ℓ_{4}} implies that Ĉ_{bt}(ℓ_{4}) = D. Thus Ĉ_{bt}(ℓ_{5}) = D and then Ĉ′_{bt}(ℓ) = D, since ℓ = R[[e_{1}^{ℓ_{5}}]]. The same reasoning follows for the case where k comes from the transformation of a named conditional.

The remaining cases follow directly from the induction hypotheses and the definition of Ĉ′_{bt}, ρ′_{bt}, Ĉ_{cf} and γ.

References

[1] Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In Alex Aiken, editor, Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Programming Languages, pages 147– 160, San Antonio, Texas, January 1999. ACM Press.

[2] Nick Benton and Philip Wadler. Linear logic, monads and the lambda calculus. In Edmund M. Clarke, editor, Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 420–431, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

[3] Anders Bondorf. Improving binding times without explicit cps-conversion. In William Clinger, editor, Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1, pages 1–10, San Francisco, California, June 1992. ACM Press.

[4] Charles Consel and Olivier Danvy. For a better support of static data flow. In John Hughes, editor, Proceedings of the Fifth ACM Conference on Functional Programming and Computer Architecture, number 523 in Lecture Notes in Computer Science, pages 496–519, Cambridge, Massachusetts, August 1991. Springer-Verlag.

[5] Charles Consel and Olivier Danvy. Static and dynamic semantics processing. In Robert (Corky) Cartwright, editor, Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 14–24, Orlando, Florida, January 1991. ACM Press.

[6] Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 493–501, Charleston, South Carolina, January 1993. ACM Press.

[7] Patrick Cousot and Radhia Cousot. Formal language, grammar and setconstraint-based program analysis by abstract interpretation. In Simon Peyton Jones, editor, Proceedings of the Seventh ACM Conference on Functional Programming and Computer Architecture, pages 170–181, La Jolla, California, June 1995. ACM Press.

[8] Daniel Damian. On Static and Dynamic Control-Flow Information in Program Analysis and Transformation. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-5.

[9] Daniel Damian and Olivier Danvy. CPS transformation of flow information, part II: Administrative reductions. Technical Report BRICS RS-01-40, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, October 2001.

[10] Daniel Damian and Olivier Danvy. A simple CPS transformation of controlflow information. Technical Report BRICS RS-01-55, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2001.

[11] Olivier Danvy. Semantics-directed compilation of non-linear patterns. Information Processing Letters, 37(6):315–322, March 1991.

[12] Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151–160, Nice, France, June 1990. ACM Press.

[13] Olivier Danvy and Lasse R. Nielsen. A first-order one-pass CPS transformation. In Mogens Nielsen, editor, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002, Lecture Notes in Computer Science, Grenoble, France, April 2002. Springer-Verlag. Extended version available as the technical report BRICS RS-01-49.

[14] Kirsten L. Solberg Gasser, Flemming Nielson, and Hanne Riis Nielson. Systematic realisation of control flow analyses for CML. In Mads Tofte, editor, Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming, pages 38–51, Amsterdam, The Netherlands, June 1997. ACM Press.

[15] 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. ACM Press.

[16] John Hatcliff and Olivier Danvy. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, pages 507–541, 1997. Extended version available as the technical report BRICS RS-96-34.

[17] Nevin Heintze. Set-based program analysis of ML programs. In Talcott [43], pages 306–317.

[18] Fritz Henglein. Syntactic properties of polymorphic subtyping. Technical Report Semantics Report D-293, DIKU, Computer Science Department, University of Copenhagen, May 1996.

[19] Carsten K. Holst and Carsten K. Gomard. Partial evaluation is fuller laziness. In Paul Hudak and Neil D. Jones, editors, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, SIGPLAN Notices, Vol. 26, No 9, pages 223–233, New Haven, Connecticut, June 1991. ACM Press.

[20] Suresh Jagannathan and Stephen Weeks. A unified treatment of flow analysis in higher-order languages. In Peter Lee, editor, Proceedings of the Twenty-Second Annual ACM Symposium on Principles of Programming Languages, pages 393– 407, San Francisco, California, January 1995. ACM Press.

[21] Neil D. Jones. What not to do when writing an interpreter for specialisation. In Olivier Danvy, Robert Glück, and Peter Thiemann, editors, Partial Evaluation, number 1110 in Lecture Notes in Computer Science, pages 216–237, Dagstuhl, Germany, February 1996. Springer-Verlag.

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

[23] Ulrik Jørring and William L. Scherlis. Compilers and staging transformations. In Mark Scott Johnson and Ravi Sethi, editors, Proceedings of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 86– 96, St. Petersburg, Florida, January 1986. ACM Press.

[24] John B. Kam and Jeffrey D. Ullman. Monotone data flow analysis frameworks. Acta Informatica, 7:305–317, 1977.

[25] Julia L. Lawall and Olivier Danvy. Continuation-based partial evaluation. In Talcott [43].

[26] Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambdacalculi (summary). In Rohit Parikh, editor, Logics of Programs – Proceedings, number 193 in Lecture Notes in Computer Science, pages 219–224, Brooklyn, June 1985. Springer-Verlag.

[27] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[28] Juarez A. Muylaert-Filho and Geoffrey L. Burn. Continuation passing transformation and abstract interpretation. In G. L. Burn, S. J. Gay, and M. D. Ryan, editors, Theory and Formal Methods 1993: Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods, Workshops in Computing Series, pages 247–259, Isle of Thorns, Sussex, 1993. Springer-Verlag.

[29] Flemming Nielson. A denotational framework for data flow analysis. Acta Informatica, 18:265–287, 1982.

[30] Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

[31] Flemming Nielson and Hanne Riis Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis. In Neil D. Jones, editor, Proceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Programming Languages, pages 332–345, Paris, France, January 1997. ACM Press.

[32] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer Verlag, 1999.

[33] Jens Palsberg. Correctness of binding-time analysis. Journal of Functional Programming, 3(3):347–363, 1993.

[34] Jens Palsberg. Comparing flow-based binding-time analyses. In Peter Mosses, Mogens Nielsen, and Michael Schwartzbach, editors, Proceedings of TAPSOFT ’95, number 915 in Lecture Notes in Computer Science, pages 561–574, Aarhus, Denmark, May 1995. Springer-Verlag.

[35] Jens Palsberg and Patrick O’Keefe. A type system equivalent to flow analysis. ACM Transactions on Programming Languages and Systems, 17(4):576–599, 1995.

[36] Jens Palsberg and Michael I. Schwartzbach. Binding-time analysis: Abstract interpretation versus type inference. In Henri Bal, editor, Proceedings of the Fifth IEEE International Conference on Computer Languages, pages 289–298, Toulouse, France, May 1994. IEEE Computer Society Press.

[37] Jens Palsberg and Mitchell Wand. CPS transformation of flow information.

Unpublished manuscript, available at http://www.cs.purdue.edu/~palsberg/
publications.html, June 2001.

[38] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[39] Amr Sabry and Matthias Felleisen. Is continuation-passing useful for data flow analysis? In Vivek Sarkar, editor, Proceedings of the ACM SIGPLAN’94 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 29, No 6, pages 1–12, Orlando, Florida, June 1994. ACM Press.

[40] Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916–941, 1997.

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

[42] Guy L. Steele Jr. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978.

[43] Carolyn L. Talcott, editor. Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. VII, No. 3, Orlando, Florida, June 1994. ACM Press.

[44] Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Højfeld Olesen, Peter Sestoft, and Peter Bertelsen. Programming with regions in the ML Kit. DIKU Rapport 97/12, University of Copenhagen, Copenhagen, Denmark, 1997.

[45] Mitchell Wand. Embedding type structure in semantics. In Mary S. Van Deusen and Zvi Galil, editors, Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 1–6, New Orleans, Louisiana, January 1985. ACM Press.

Recent BRICS Report Series Publications

RS-01-54 Daniel Damian and Olivier Danvy. Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation. December 2001. 41 pp. To appear in the Journal of Functional Programming. This report supersedes the earlier BRICS report RS-00-15.

RS-01-53 Zoltán Ésik and Masami Ito. Temporal Logic with Cyclic Counting and the Degree of Aperiodicity of Finite Automata. December 2001. 31 pp.

RS-01-52 Jens Groth. Extracting Witnesses from Proofs of Knowledge in the Random Oracle Model. December 2001. 23 pp.

RS-01-51 Ulrich Kohlenbach. On Weak Markov’s Principle. December 2001. 10 pp.

RS-01-50 Jiří Srba. Note on the Tableau Technique for Commutative Transition Systems. December 2001. 19 pp. To appear in the proceedings of FOSSACS ’02.

RS-01-49 Olivier Danvy and Lasse R. Nielsen. A First-Order One-Pass CPS Transformation. December 2001. 21 pp. Extended version of a paper to appear in the proceedings of FOSSACS ’02.

RS-01-48 Mogens Nielsen and Frank D. Valencia. Temporal Concurrent Constraint Programming: Applications and Behavior. December 2001. 36 pp.

RS-01-47 Jesper Buus Nielsen. Non-Committing Encryption is Too Easy in the Random Oracle Model. December 2001. 20 pp.

RS-01-46 Lars Kristiansen. The Implicit Computational Complexity of Imperative Programming Languages. November 2001. 46 pp.

RS-01-45 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average Case Error Estimates. November 2001. 43 pp.

RS-01-44 M. Oliver Möller, Harald Rueß, and Maria Sorea. Predicate Abstraction for Dense Real-Time Systems. November 2001. 27 pp.

RS-01-43 Ivan B. Damgård and Jesper Buus Nielsen. From Known-Plaintext Security to Chosen-Plaintext Security. November 2001. 18 pp.