Closure analysis in constraint form.
Flow analyses of untyped higher-order functional programs have in the past decade been presented by Ayers, Bondorf, Consel, Jones, Heintze, Sestoft, Shivers, Steckler, Wand, and others. The analyses are usually defined as abstract interpretations and are used for rather different tasks such as type recovery, globalization, and binding-time analysis. The analyses all contain a global closure analysis that computes information about higher-order control-flow. Sestoft proved in 1989 and 1991 that closure analysis is correct with respect to call-by-name and call-by-value semantics, but it remained open if correctness holds for arbitrary beta-reduction.This article answers the question; both closure analysis and others are correct with respect to arbitrary beta-reduction. We also prove a subject-reduction result: closure information is still valid after beta-reduction. The core of our proof technique is to define closure analysis using a constraint system. The constraint system is equivalent to the closure analysis of Bondorf, which in turn is based on Sestoft's.
INTRODUCTION
1.1 Background
The optimization of higher-order functional languages requires powerful program
analyses. The traditional framework for such analyses is abstract interpretation, and
for typed languages, suitable abstract domains can often be defined by induction
on the structure of types. For example, function spaces can be abstracted into
function spaces. For untyped languages such as the -calculus, or dynamically
typed languages such as Scheme, abstract domains cannot be defined by abstracting
function spaces into function spaces. Other domains can be used, but it may then
be difficult to relate the abstract interpretation to the denotational semantics. In
this article we consider a style of program analysis where the result is an abstraction
of the operational semantics.
In the past decade, program analyses of untyped languages has been presented
Author's address: Computer Science Department, Aarhus University, Ny Munkegade, DK-8000
Aarhus C, Denmark; email: palsberg@daimi.aau.dk.
Permission to copy without fee all or part of this material is granted provided that the copies are
not made or distributed for direct commercial advantage, the ACM copyright notice and the title
of the publication and its date appear, and notice is given that copying is by permission of the
Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or
specific permission.
ACM Transactions on Programming Languages and Systems, 17(1):47-62, January 1995. Also in
Proc. CAAP'94, pages 276-290. c
Jens Palsberg
by Ayers [1992], Bondorf [1991], Consel [1990], Jones [1981], Heintze [1992], Sestoft
[1989; 1991], Shivers [1991a; 1991b], Wand and Steckler [1994], and others.
Although the analyses are used for rather different tasks such as type recovery,
globalization, and binding-time analysis, they are all based on essentially the same
Key idea. In the absence of types, define the abstract domains in terms
of program points.
For example, consider the following -term:
Giannini and Rocca [1988] proved that this strongly normalizing term has no higher-order
polymorphic type. Still, a program analysis might answer basic questions such
as:
(1) For every application point, which abstractions can be applied?
(2) For every abstraction, to which arguments can it be applied?
Each answer to such questions should be a subset of the program points in this particular
-term. Thus, let us label all abstractions and applications. Also variables
will be labeled: if a variable is bound, then it is labeled with the label of the - that
binds it, and if it is free, then with an arbitrary label. By introducing an explicit
application symbol, we get the following abstract syntax for the above -term.
An analysis might be able to find out that no matter how reduction proceeds:
-"I can only be applied to I ," that is, an abstraction with label 3 can only be
applied to abstractions with label 3;
-"At the application point dd (in \Delta) both I and K can be applied," that is, at an
application point labeled 12 there can only be applied abstractions with labels 3
and 4; and
-"the abstraction -c:b will never be applied," that is, at no application point can
an abstraction with label 5 be applied.
The quoted sentences give the intuitive understanding of the precise statements
that follow. In this particular example, the labels are rather unnecessary because
no name clashes happen during any reduction and because I , K, and -c:b are in
normal form. In the presence of name clashes or reduction under a -, however, it
is crucial to use sets of program points as the abstract values.
The above questions have turned out to be of paramount importance in many
analyses of untyped functional programs. Following Sestoft and Bondorf, we will
call any analysis that can answer them conservatively a closure analysis. On top of
a closure analysis, one can build for example type recovery analyses, globalization
analyses, and binding-time analyses. The closure analysis answers questions about
higher-order control flow, and the extension answers the questions one is really
interested in, for example, about type recovery. The role of closure analysis is thus
as follows:
Closure Analysis in Constraint Form \Delta 3
"Higher-order closure analysis."
Closure analysis is useful for higher-order languages in general, for example, object-oriented
languages (see Palsberg and Schwartzbach [1991; 1994b]). It is also useful
for typed functional languages because type information is usually not specific
enough to tell which functions among the type-correct ones are called at each application
point.
Closure analysis and its extensions can be defined as abstract interpretations.
They differ radically from traditional abstract interpretations, however, in that
the abstract domain is defined in terms of the program to be analyzed. This
means that such analyses are global: before the abstract domain can be defined,
the complete program is required. Moreover, the program cannot take higher-order
input because that would add program points. Also the minimal function graph
approach to program analysis uses abstract domains defined in terms of the input
program. In contrast, traditional abstract interpretations can analyze pieces of a
program in isolation. We will refer to all analyses based on closure analysis as flow
analyses.
Examples of large-scale implementations of such analyses can be found in the
Similix system of Bondorf [Bondorf 1993; Bondorf and Danvy 1991], the Schism
system of Consel [1990], and the system of Agesen et al. [1993] for analyzing Self
programs [Ungar and Smith 1987]. The last of these implementations demonstrates
that closure analysis can handle dynamic and multiple inheritance.
Closure analysis and its extensions have been formulated using constraints by
others, for example, Heintze [1992; 1994], and Wand and Steckler [1994]. Their
constraint systems are in spirit close to ours, although they are technically somewhat
different. A key difference between Heintze's definition [Heintze 1994] and
ours is that he attempts to avoid analyzing code that will not be executed under
call-by-value. This goal is shared by an analysis of Palsberg and Schwartzbach
[1992a]. The idea of defining program analyses using constraints over set variables
is called set-based analysis by Heintze.
proved that closure analysis is correct with respect to call-
by-name and call-by-value semantics, but it remained open if correctness holds for
arbitrary beta-reduction.
1.2 Our Results
We prove that closure analysis is correct with respect to arbitrary beta-reduction.
We also prove a subject-reduction result: closure information is still valid after
beta-reduction. The correctness result implies that closure analysis is correct with
respect to any reduction strategy.
-We present a novel specification of closure analysis that allows arbitrary beta-
reduction to take place and which subsumes all previous specifications.
-We present a closure analysis that uses a constraint system. The constraint system
characterizes the result of the analysis without specifying how it is computed.
An example of such a constraint system is given in Section 1.3.
-We prove that the constraint-based analysis is equivalent to the closure analysis
of Bondorf [1991], which in turn is based on Sestoft's [Sestoft 1989]. We also
Jens Palsberg
prove that these analyses are equivalent to a novel simplification of Bondorf's
definition.
The proofs of correctness and subject-reduction then proceed by considering only
the constraint-based definition of closure analysis.
In contrast to the closure analyses by abstract interpretation, the one using a
constraint system does not depend on labels being distinct. This makes it possible
to analyze a -term, beta-reduce it, and then analyze the result without relabeling
first. The abstract interpretations might be modified to have this property also, but
it would be somewhat messy. This indicates that a direct proof of correctness of
such a modified abstract interpretation would be more complicated than the proof
presented in this article.
Our technique for proving correctness generalizes without problems to analyses
based on closure analysis. The following two results are not proved in this article:
-The safety analysis of Palsberg and Schwartzbach [1992a; 1992b] is correct with
respect to arbitrary beta-reduction. This follows from the subject-reduction prop-
erty: terms stay safe after beta-reduction.
-The binding-time analysis of Palsberg and Schwartzbach [1994a] that was proved
correct by Palsberg [1993], can be proved correct more elegantly with our new
technique.
The constraint-based definition of closure analysis is straightforward to extend to
practical languages. For a medium-sized example see Palsberg and Schwartzbach
[1994b] where the analysis is defined for an object-oriented language.
1.3 Example
The constraint system that expresses closure analysis of a -term is a set of Horn
clauses. If the -term contains n abstractions and m applications, then the constraint
system contains n constraints. Thus, the size of a constraint
system is in the worst-case quadratic in the size of the -term. Space constraints
disallow us to show a full-blown example involving name clashes and reduction under
a -, so consider instead the -term (-x:xx)(-y:y) which has the abstract syntax
The constraint system that expresses closure analysis
of this -term looks as follows.
From
From
From @ 3 and - 1
ae
From @ 3
ae
From @ 4
ae
From @ 4
ae
Symbols of the forms [[- l ]], [[- l ]], and [[@ i are metavariables. They relate to variables
with label l, abstractions with label l, and applications with label i, respec-
tively. Notice that we do not assume, for example, that there is just one abstraction
Closure Analysis in Constraint Form \Delta 5
with label l. The reason is that we want to do closure analysis of all terms, also
those arising after beta-reduction which may copy terms and hence labels.
To the left of the constraints, we have indicated from where they arise. The first
two constraints express that an abstraction may evaluate to an abstraction with
the same label. The rest of the constraints come in pairs. For each application
point @ i and each abstraction with label l there are two constraints of the form:
flg ' "metavar. for operator of @
flg ' "metavar. for operator of @
Such constraints can be read as:
-The first constraint. If the operator of @ i evaluates to an abstraction with label l,
then the bound variable of that abstraction may be substituted with everything
to which the operand of @ i can evaluate.
-The second constraint. If the operator of @ i evaluates to an abstraction with
label l, then everything to which the body of the abstraction evaluates is also a
possible result of evaluating the whole application @ i .
In a solution of the constraint system, metavariables are assigned closure in-
formation. The minimal solution of the above constraint system is a mapping L
where:
For example, the whole -term will, if normalizing, evaluate to an abstraction
with label 2 (L[[@ 4 at the application point @ 3 there can only be applied
abstractions with label 2 (L[[- 1 the application point @ 3
is the only point
where abstractions with label 2 can be applied (L[[- 1 and such abstractions
can only be applied to -terms that either do not normalize or evaluate to an
abstraction with label 2 (L[[- 2
One of our theorems says that the computed closure information is correct. One
might also try to do closure analysis of the above -term using Bondorf's abstract
interpretation; another of our theorems says that we will get the same result.
Now contract the only redex in the above -term. The result is a -term with
abstract
One third of our theorems says that the
mapping L above gives correct closure information also for this -term.
In the following section we define three closure analyses: Bondorf's, a simpler
abstract interpretation, and one in constraint form. In Section 3 we prove that they
are equivalent, and in Section 4 we prove that they are correct.
2. CLOSURE ANALYSIS
Recall the -calculus [Barendregt 1981].
Definition 2.1. The language   of -terms has an abstract syntax which is defined
by the grammar:
(application)
Jens Palsberg
The labels on variables, abstraction symbols, and application symbols have no
semantic impact; they mark program points. The label on a bound variable is the
same as that on the - that binds it. Labels are drawn from the infinite set Label.
The symbols l; l labels. The labels and the application symbols are
not part of the concrete syntax of  . We identify terms that are ff-congruent. The
ff-conversion changes only bound variables, not labels. We assume the Variable
Convention of Barendregt [1981]: when a -term occurs in this article, all bound
variables are chosen to be different from the free variables. This can be achieved by
renaming bound variables. An occurrence of (- l x:E) @ called a redex. The
semantics is as usual given by the rewriting-rule scheme:
(- l x:E) @
Here, E[E 0 =x l ] denotes the term E with substituted for the free occurrences
of x l . Notice that by the Variable Convention, no renaming of bound variables is
necessary when doing substitution. In particular, when we write (- l y:E)[E 0 =x l 0
we have that y l 6j x l 0
and that y l is not among the free variables of E 0 . Thus,
(- l y:E)[E 0 =x l 0
]). We write ES !   E T to denote that E T has
been obtained from ES by 0 or more beta-reductions. A term without redexes is
in normal form.
The abstract domain for closure analysis of a -term E is called CMap(E) and is
defined as follows.
Definition 2.2. A metavariable is of one of the forms [[- l ]], [[- l ]], and [[@ i ]]. The
set of all metavariables is denoted Metavar. A -term is assigned a metavariable by
the function var, which maps x l to [[- l ]], - l x:E to [[- l ]], and
to
For a -term E, Lab(E) is the set of labels on abstractions (but not applications)
occurring in E. Notice that Lab(E) is finite. The set CSet(E) is the powerset
of Lab(E); CSet(E) with the inclusion ordering is a complete lattice. The set
CMap(E) consists of the total functions from Metavar to CSet(E). The set CEnv(E)
contains each function in CMap(E) when restricted to metavariables of the form
l ]]. Both CMap(E) and CEnv(E) with pointwise ordering, written v, are complete
lattices where the least upper bound is written t. The function hV 7! Si maps the
metavariable V to the set S and maps all other metavariables to the empty set.
Finally, we define upd
2.1 The Specification of Closure Analysis
We can then state precisely what a closure analysis is. An intuitive argument
follows the formal definition.
Definition 2.1.1. For a -term E and for every L 2 CMap(E), we define a binary
relation on -terms, as follows. only if the following
four conditions hold:
l x:E), then EX contains - l 0
z:E 0 such that flg ' L(var(E 0 )).
contains (- l x:E) @
, then EX contains 0such that flg '
)).
Closure Analysis in Constraint Form \Delta 7
such that flg '
)).
A closure analysis of E produces L 2 CMap(E) such that if
Intuitively, if EX !   E Y , then we can get conservative information about the
abstractions in E Y by doing closure analysis of EX . For example, the first condition
in Definition 2.1.1 can be illustrated as follows.
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
In this case, E Y is an abstraction with label l. Thus, EX can evaluate to an
abstraction with label l. The first condition says that in this case the mapping L
must satisfy flg ' L(var(EX )). In other words, the analysis must be aware that
such an abstraction is a possible result of evaluating EX .
The three other conditions in Definition 2.1.1 cover the cases where abstractions
are proper subterms of E Y . The second condition covers the case where an abstraction
in E Y is the body of yet another abstraction. The third and fourth conditions
cover the cases where an abstraction is the operator and the operand of an appli-
cation, respectively. Here, we will illustrate just the first of these three conditions;
the others are similar.
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta \ThetaB
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta \ThetaB
z - l 0
y
In this case, E Y contains an abstraction with label l (- l x:E). This abstraction is
in turn the body of an abstraction with label l 0 (- l 0
l x:E). The second condition
Jens Palsberg
in Definition 2.1.1 says that in this case there must be an abstraction in EX with
label l 0 (- l 0
, the bound variable may be different) such that the mapping L
satisfies flg ' L(var(E 0 )). In other words, the analysis must be aware that some
abstraction - l 0
z:E 0 in EX can evolve into an abstraction with a body being an
abstraction with label l.
Notice the possibility that more than one abstraction in EX has label l 0 . Thus, if
we want closure information for "the body of the abstraction with label l 0 " we must
compute the union of information for the bodies of all abstractions in EX with label
l 0 . A similar comment applies to the third and fourth condition in Definition 2.1.1.
Such use of closure information is not of concern in this article, however.
2.2 Bondorf's Definition
We now recall the closure analysis of Bondorf [1991], with a few minor changes in
the notation compared to his presentation. The analysis assumes that all labels are
distinct. Bondorf's definition was originally given for a subset of Scheme; we have
restricted it to the -calculus. Note that Bondorf's definition is based on Sestoft's
[Sestoft 1989].
We have simplified Bondorf's definition as follows. Bondorf's original definition
assigns distinct metavariables to different occurrences of a variable; in contrast
we assign the same metavariable to each occurrence of a variable. The simplified
definition is equivalent to Bondorf's original definition; see below.
We will use the notation that if - l x:E is a subterm of the term to be analyzed,
then the partial function body maps the label l to E.
Definition 2.2.1. We define
in (upd [[- l
let c be - 0 (var(E 1
let - 00 be upd
let ae 00 be ae 0 t (t l2c (upd [[- l
in (- 00
We can now do closure analysis of E by computing fst(B(E)).
If we modify the above definition such that different occurrences of a variable
are assigned distinct metavariables, then we obtain Bondorf's original definition.
That definition will assign the same set to all metavariables for the occurrences of
a given variable, and moreover, the computed closure information will be the same
as that computed by the stated analysis (we leave the details to the reader).
2.3 A Simpler Abstract Interpretation
Bondorf's definition can be simplified considerably. To see why, consider the
second component of CMap(E) \Theta CEnv(E). This component is updated only in
Closure Analysis in Constraint Form \Delta 9
)-ae and read only in b(x l )-ae. The key observation is that both these
operations can be done on the first component instead. Thus, we can omit the use
of CEnv(E). By rewriting Bondorf's definition according to this observation, we
arrive at the following definition. As with Bondorf's definition, we assume that all
labels are distinct.
Definition 2.3.1. We define
m(x l )-
F
We can now do closure analysis of E by computing fix(m(E)).
A key question is: is the simpler abstract interpretation equivalent to Bondorf's?
We might attempt to prove this using fixed-point induction, but we find it much
easier to do using a particular constraint system as a "stepping stone."
2.4 A Constraint System
For a -term E, the constraint system is a finite set of Horn clauses over inclusions of
the form P ' P 0 , where P and P 0 are either metavariables or elements of CSet(E).
A solution of such a system is an element of CMap(E) that satisfies all Horn clauses.
The constraint system is defined in terms of the -term to be analyzed. We need
not assume that all labels are distinct.
The set R(E 1 @ consists of the two elements
For a -term E, the constraint system C(E) is the union of the following sets of
constraints.
-For every - l x:E 0 in E, the singleton constraint set consisting of flg ' [[- l ]].
-For every
in E and for every - l x:E 0 in E, the set R(E 1 @
Each C(E) has a least solution, namely, the intersection of all solutions.
We can now do closure analysis of E by computing a solution of C(E). The
canonical choice of solution is of course the least one.
The closure analysis of Bondorf and J-rgensen [1993] can be understood as
adding two constraints to each R(E 1 @
such that in effect the inclusions
are changed to equalities. Thus, their
closure analysis computes more approximate information than ours. In return,
their analysis can be computed in almost-linear time, using an other formulation
of the problem [Bondorf and J-rgensen 1993], whereas the fastest known algorithm
for computing the least solution of C(E) uses transitive closure (see Palsberg and
Schwartzbach [1992a; 1994b]).
3. EQUIVALENCE
We now prove that the three closure analyses defined in Section 2 are equivalent
(when applied to -terms where all labels are distinct). We will use the standard
Jens Palsberg
terminology that - is a prefixed point of m(E) if m(E)- v -.
Lemma 3.1. If - is a prefixed point of m(E), then so is it of m(E 0 ) for every
Proof. By induction on the structure of E.
Lemma 3.2. C(E) has least solution fix(m(E)).
Proof. We prove a stronger property: the solutions of C(E) are exactly the
prefixed points of m(E). There are two inclusions to be considered.
First, we prove that every solution of C(E) is a prefixed point of m(E). We
proceed by induction on the structure of E. In the base case, consider x l . Clearly,
every - is a prefixed point of m(x l ). In the induction step, consider first - l x:E.
Suppose - is a solution of C(- l x:E). Then - is also a solution of C(E), so by the
induction hypothesis, - is a prefixed point of m(E). Hence, we get m(- l
(m(E)-)t h[[- l by using the definition of m, that -
is a prefixed point of m(E), and that since C(- l x:E) has solution -, flg ' - l ]]).
Consider then Suppose - is a solution of
solution of C(E 1
so by the induction hypothesis, - is a prefixed point
of m(E 1
Hence, we get m(E 1 @
)-, by using the definition
of m, that - is a prefixed point of m(E 1
), and that C(E 1 @
solution -.
Second, we prove that every prefixed point of m(E) is a solution of C(E). We
proceed by induction on the structure of E. In the base case, consider x l . Clearly,
every - is a solution of C(x l ). In the induction step, consider first - l x:E 0 . Suppose
- is a prefixed point of m(- l x:E 0 ). Then, by Lemma 3.1, - is also a pre-fixed
point of m(E 0 ). By the induction hypothesis, - is a solution of C(E 0 ).
Thus, we need to prove that - satisfies flg ' [[- l
in
For the first of these, use that - is a prefixed point of
from which the result follows. For the second one, consider
in E 0 . By
Lemma 3.1, - is also a prefixed point of m(E 1 @
). Using the assumption
that we get - w
F
-(var(body(l)))i), from which the result follows.
Consider then
. Suppose - is a prefixed point of m(E 1 @
Lemma 3.1, - is also a prefixed point of both m(E 1
). By the induction
hypothesis, - is a solution of both C(E 1
). Thus, we need to prove that
for every - l x:E 0 in
being a
prefixed point of m(E 1 @
F
-(var(body(l)))i), from which the result follows.
Lemma 3.3. C(E) has least solution fst(B(E)).
Proof. Similar to the proof of Lemma 3.2.
Theorem 3.4. The three closure analyses defined in Section 2 are equivalent.
Proof. Combine Lemmas 3.2 and 3.3.
Closure Analysis in Constraint Form \Delta 11
4. CORRECTNESS
We now prove that the three closure analyses defined in Section 2 are correct. The
key is to define an entailment relation A ; A 0 (Definition 4.1) meaning that all
constraints in the constraint system A 0 can be logically derived from those in A. A
central result (Theorem 4.10) is that if EX
theorem is proved without at all considering solutions of the involved constraint
systems.
Definition 4.1. If A is a constraint system, and H is a Horn clause, then the
judgment A ' H ("A entails H") holds if it is derivable using the following five
rules:
(Reflexivity)
(Modus Ponens)
If A; A 0 are constraint systems, then A ; A 0 if and only if 8H 2 A
Lemma 4.2. ; is reflexive, transitive, and solution-preserving. If A ' A 0 , then
Proof. The last property is immediate using Discharge. Reflexivity of ; is
a consequence of the last property. For transitivity of ;, suppose A ; A 0 and
. The statement "if A 0 ' H then A ' H " can be proved by induction on
the structure of the proof of A 0 ' H . To prove A ; A 00 , suppose then that H 2 A 00 .
From A 0 ; A 00 we get A 0 ' H , and from the above statement we finally get A ' H .
To prove that ; is solution-preserving, suppose A ; A 0 and that A has solution
L. We need to prove that for every H 2 A 0 , H has solution L. This can be proved
by induction on the structure of the proof of A ' H .
The following lemmas are structured such that Modus Ponens is only used in the
proof of Lemma 4.3, and Weakening is only used in the proof of Lemma 4.6.
To aid intuition we can informally read A ' var(E) ' var(E 0 ) as "under the
assumption A, the -term E has smaller flow information than the -term E 0 ."
The next lemma states that two specific constraints can be derived from the
constraint system for a redex. Informally, the first constraint says that the argument
has smaller flow information than the bound variable, and the second constraint
says that the body of the abstraction has smaller flow information than the whole
redex.
Jens Palsberg
Lemma 4.3. If A ; C((- l x:E) @
Proof. We have A ' flg ' [[- l x:E). The result
then follows from var(- l Modus Ponens.
The next lemma is a substitution lemma. Informally, it states that a -term
gets smaller flow information if a subterm gets substituted by one with smaller flow
information.
Lemma 4.4. If A ' var(U) ' [[- l ]], then A ' var(E[U=x l ]) ' var(E).
Proof. By induction on the structure of E, using Reflexivity repeatedly.
Informally, the next lemma states that beta-reduction creates -terms with smaller
flow information.
Lemma 4.5. If A ; C(EX ) and
Proof. We proceed by induction on the structure of EX . In the base case,
consider x l . The conclusion is immediate since x l is in normal form.
In the induction step, consider first - l x:E. Suppose . Notice that
Using Reflexivity we get A ' [[- l
Consider finally
. There are three cases. Suppose
Using Reflexivity we get A ' [[@ i
Suppose then that
Using Reflexivity we get A ' [[@ i
Suppose then that
we get A ' From the former of these and
Lemma 4.4 we get A ' var(E[E 2 =x l ]) ' var(E). Using Transitivity we can finally
conclude that A ' var(E[E 2 =x l ]) ' [[@ i ]].
Informally, the next lemma states that entailment is robust under beta-reduction
and substitution.
Lemma 4.6. Suppose A ; R(E 1 @
Proof. For
Reflexivity,
Lemma 4.5, or Lemma 4.4. The result then follows using Weakening.
The following definition is needed for stating and proving Lemma 4.9.
Definition 4.7. The set W (E; is the union of the following sets of constraints.
-For every
in E and for every - l x:E 3
in
-For every
in E 0 and for every - l x:E 3
in E, the set R(E 1 @
Lemma 4.8. W
then W
Proof. Immediate.
Closure Analysis in Constraint Form \Delta 13
The next lemma is a substitution lemma. Like Lemma 4.6, it states that entailment
is robust under substitution.
Lemma 4.9. If A ;W (E; U) and A ' var(U) ' [[- l ]], then A ; C(E[U=x l ]).
Proof. Let ae denote the substitution [U=x l ]. We proceed by induction on the
structure of E. In the base case, consider
. If x l j y l 0
, then
the result follows from A ;W (E; U) and Lemma 4.2. If x l 6j y l 0
, then
again the result follows from A ;W (E; U) and Lemma 4.2.
In the induction step, consider first
, then
also in this case the result follows from A ;W (E; U) and Lemma 4.2. If x l 6j y l 0
ae). By the induction hypothesis, A ; C(E 0 ae). Thus, we need to
show
and for every
in
The first follows from A ; C(- l 0
For the second, consider any E 1 @
in
is a subterm of
is a subterm of U .
In each case the result follows from A ;W (E; U) and Lemma 4.6.
Consider finally
. Notice that
the induction hypothesis, A ; C(E 1 ae) [ C(E 2 ae). Thus, we need to show that
for every - l 0
)ae. Notice that either - l 0
y:E 0 is a subterm of
, or
y:E 0 is a subterm of
, or - l 0
y:E 0 is a subterm
of U . In each case the result follows from A ;W (E; U) and Lemma 4.6.
We can now prove that if we beta-reduce EX to E Y , then the constraint system
for EX entails the constraint system for E Y .
Theorem 4.10. If EX
Proof. We proceed by induction on the structure of EX . In the base case of
x l , the conclusion is immediate since x l is in normal form.
In the induction step, consider first - l x:E. Suppose . By the induction
hypothesis, Thus, we need
to show C(- l x:E) ' flg ' [[- l
in - l x:E 0 , C(- l x:E) ;
first follows using Discharge. For the second, there are
four cases. Notice that by Discharge we have C(- l x:E)
every x:E. In the first case, suppose
is also a subterm
of - l x:E. The result then follows from Lemma 4.6. In the second case, consider
a subterm E 0@
of - l x:E such that E
. Again, the result follows from
Lemma 4.6. In the third case, consider a l x:E such that
. Yet again, the result follows from Lemma 4.6. In the fourth case, consider
a subterm E 0
]. The
substitution arises because of the contraction of a redex. From Lemma 4.3 we get
]]. The result then follows from Lemma 4.6.
Consider finally . For every - l x:E in
x:E). There are three cases.
Suppose that E 1
By the induction hypothesis, C(E 1
0). Thus we need to show that for every - l x:E 0 in E 0
There are three cases. In the first case,
suppose - l x:E 0 is a subterm of
. The result then follows from Lemma 4.6.
14 \Delta Jens Palsberg
In the second case, consider a subterm - l x:E of
such that
the result follows from Lemma 4.6. In the third case, consider a subterm - l x:E of
such that - l x:E
]). The substitution arises because of
the contraction of a redex. From Lemma 4.3 we see C(E 1 @
]].
The result then follows from Lemma 4.6.
Suppose then that E 2
The proof in this case is similar to the case of
we omit the details.
Suppose then that E 1
we see C(E 1 @
we see that W (E;
). The result then follows from Lemma 4.9.
Theorem 4.11. The three closure analyses defined in Section 2 are correct.
Proof. From Theorem 3.4 we see that the three analyses are equivalent when
applied to -terms where all labels are distinct. Thus, it is sufficient to prove that
the one defined using a constraint system is correct. The proof has two steps.
In Step 1, use Lemmas 4.3, 4.4, and 4.5 to prove that if A ; C(EX ) and EX !
both of the following properties hold:
contains - l y:E, then EX contains - l z:E 0 such that A ' var(E) ' var(E 0 ).
0such that A '
In Step 2, suppose C(EX ) has solution L, and suppose EX !   E Y . We will prove
by induction on the length of EX !   E Y .
In the base case, immediate. In the induction step, suppose
. By Theorem 4.10, C(EX
has solution L. By the induction hypothesis, To prove
there are four cases to be considered.
First suppose From
Lemma 4.5 we get C(EX Finally, the result follows by using
that C(EX ) has solution L.
Then suppose
l x:E). From that EZ contains
z:E 0 such that flg ' L(var(E 0 )). From Step 1 of this proof, we get that EX
contains - l 0
w:E 00 such that C(EX ) ' Finally, the result follows
by using that C(EX ) has solution L.
In the last two cases, suppose E Y contains either (- l x:E) @
or
respectively. Both cases are similar to the second one, so we omit the details.
Finally, we prove our subject-reduction result.
Theorem 4.12. If C(E) has solution L and solution L.
Proof. Immediate from Theorem 4.10 and Lemma 4.2.

ACKNOWLEDGMENTS

The author thanks Torben Amtoft, Nils Klarlund, and the anonymous referees for
helpful comments on a draft of the article.
Closure Analysis in Constraint Form \Delta 15



--R

Type inference of Self: Analysis of objects with dynamic and multiple inheritance.

Efficient closure analysis with reachability.
The Lambda Calculus: Its Syntax and Semantics.
Similix 5.0 Manual.
Automatic autoprojection of higher order recursive equations.

Automatic autoprojection of recursive equations with global variables and abstract data types.
Efficient analyses for realistic off-line partial evaluation

Binding time analysis for higher order untyped functional languages.
Characterization of typings in polymorphic type dis- cipline

based program analysis.
Flow analysis of lambda expressions.

Correctness of binding-time analysis


Safety analysis versus type inference.
Safety analysis versus type inference for partial types.

Analysis and efficient implementation of functional programs.
Replacing function parameters by global variables.


SELF: The power of simplicity.
Selective and lightweight closure conversion.
revised October
--TR
Self: The power of simplicity
Binding time analysis for high order untyped functional languages
Object-oriented type inference
Automatic autoprojection of recursive equations with global variable and abstract data types
Automatic autoprojection of higher order recursive equations
Safety analysis versus type inference for partial types
based program analysis
Object-oriented type systems
Selective and lightweight closure conversion
Set-based analysis of ML programs
Safety analysis versus type inference
Type Inference of SELF
Flow Analysis of Lambda Expressions (Preliminary Version)

--CTR
Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.4, p.576-599, July 1995
Jens Palsberg, Equality-based flow analysis versus recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.6, p.1251-1264, Nov. 1998
Paolo Di Blasio , Kathleen Fisher , Carolyn Talcott, A Control-Flow Analysis for a Calculus of Concurrent Objects, IEEE Transactions on Software Engineering, v.26 n.7, p.617-634, July 2000
Suresh Jagannathan , Peter Thiemann , Stephen Weeks , Andrew Wright, Single and loving it: must-alias analysis for higher-order languages, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.329-341, January 19-21, 1998, San Diego, California, United States
Flemming Nielson , Hanne Riis Nielson, Infinitary control flow analysis: a collecting semantics for closure analysis, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.332-345, January 15-17, 1997, Paris, France
Kirsten L. Solberg Gasser , Flemming Nielson , Hanne Riis Nielson, Systematic realisation of control flow analyses for CML, ACM SIGPLAN Notices, v.32 n.8, p.38-51, Aug. 1997
Flanagan , Matthias Felleisen, Componential set-based analysis, ACM SIGPLAN Notices, v.32 n.5, p.235-248, May 1997
Anindya Banerjee, A modular, polyvariant and type-based closure analysis, ACM SIGPLAN Notices, v.32 n.8, p.1-10, Aug. 1997
Flanagan , Matthias Felleisen, Componential set-based analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.2, p.370-416, March 1999
Philippe Meunier , Robert Bruce Findler , Paul Steckler , Mitchell Wand, Selectors Make Set-Based Analysis Too Hard, Higher-Order and Symbolic Computation, v.18 n.3-4, p.245-269, December  2005
Neal Glew , Jens Palsberg, Type-safe method inlining, Science of Computer Programming, v.52 n.1-3, p.281-306, August 2004
David Herman , Philippe Meunier, Improving the static analysis of embedded languages via partial evaluation, ACM SIGPLAN Notices, v.39 n.9, September 2004
Christian Fecht , Helmut Seidl, Propagating differences: an efficient new fixpoint algorithm for distributive constraint systems, Nordic Journal of Computing, v.5 n.4, p.304-329, Winter 1998
Philippe Meunier , Robert Bruce Findler , Matthias Felleisen, Modular set-based analysis from contracts, ACM SIGPLAN Notices, v.41 n.1, p.218-231, January 2006
Thomas Jensen, Types in program analysis, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
Murali Krishna Ramanathan , Ananth Grama , Suresh Jagannathan, Static specification inference using predicate mining, ACM SIGPLAN Notices, v.42 n.6, June 2007
V. Krishna Nandivada , Suresh Jagannathan, Dynamic state restoration using versioning exceptions, Higher-Order and Symbolic Computation, v.19 n.1, p.101-124, March     2006
Jens Palsberg , Christina Pavlopoulou, From polyvariant flow information to intersection and union types, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.197-208, January 19-21, 1998, San Diego, California, United States
Andrew Tolmach , Dino P. Oliva, From ML to Ada: Strongly-typed language interoperability via source translation, Journal of Functional Programming, v.8 n.4, p.367-412, July 1998
H. Seidl , M. H. Srensen, Constraints to stop higher-order deforestation, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.400-413, January 15-17, 1997, Paris, France
Andrew K. Wright , Suresh Jagannathan, Polymorphic splitting: an effective polyvariant flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.166-207, Jan. 1998
Anindya Banerjee , Thomas Jensen, Modular control-flow analysis with rank 2 intersection types, Mathematical Structures in Computer Science, v.13 n.1, p.87-124, February
Jens Palsberg, Type-based analysis and applications, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.20-27, June 2001, Snowbird, Utah, United States
David A. Schmidt, Trace-Based Abstract Interpretation of Operational Semantics, Lisp and Symbolic Computation, v.10 n.3, p.237-271, May 1998
constraints;correctness proof;flow analysis