Journal of Functional Programming (1993), vol. 3(3), pp. 347–363Correctness of Binding-time AnalysisJens [email protected] Science Department, Aarhus UniversityNy Munkegade, DK–8000 Aarhus C, DenmarkAbstractA binding-time analysis is correct if it always produces consistent binding-time informa-tion. Consistency prevents partial evaluators from “going wrong”. A sufficient and decid-able condition for consistency, called well-annotatedness, was first presented by Gomardand Jones.In this paper we prove that a weaker condition implies consistency. Our condition isdecidable, subsumes the one of Gomard and Jones, and was first studied by Schwartzbachand the present author. Our result implies the correctness of the binding-time analysisof Mogensen, and it indicates the correctness of the core of the binding-time analyses ofBondorf and Consel. We also prove that all partial evaluators will on termination haveeliminated all “eliminable”-marked parts of an input which satisfies our condition. Thisgeneralizes a result of Gomard. Our development is for the pure λ-calculus with explicitbinding-time annotations.1 IntroductionA partial evaluator is an implementation of Kleene’s Smntheorem. When given aprogram and some of its expected input, a partial evaluator produces a so-calledresidual program. The residual program will, when given the remaining input, pro-duce the same result as would have the original program when given all of theinput. The challenge for a partial evaluator is to produce residual programs thatare significantly faster than the input programs. Partial evaluators can for examplebe used to generate compilers from interpreters (Bondorf, 1991; Gomard & Jones,1991).Most partial evaluators use a binding-time analysis in a pre-processing phase.A binding-time analysis annotates a program by marking as “eliminable” thoseparts which may be evaluated during partial evaluation and by marking remainingparts as “residual”. Partial evaluation then proceeds by attempting to evaluate theeliminable parts.A binding-time analysis is correct if it always produces consistent binding-timeinformation. Consistency prevents partial evaluators from “going wrong”. A partialevaluator “goes wrong” if it commits a so-called “projection error” (Gomard &Jones, 1991), that is, if it trusts a part of the program to be of a particular form,of which it is not.A sufficient and decidable condition for consistency, called well-annotatedness,was first presented by Gomard and Jones (1991). They proved that a particular2 Jens Palsbergpartial evaluator cannot “go wrong” when given a well-annotated program. Go-mard also presented a binding-time analysis that always produces well-annotatedprograms (Gomard, 1990; Gomard, 1991).In this paper we prove that a weaker condition than that of Gomard and Jonesimplies consistency. Our condition is decidable, subsumes the one of Gomard andJones, and was first studied by Schwartzbach and the present author (Palsberg &Schwartzbach, 1992). Our result implies the correctness of the binding-time analysisof Mogensen (1992), and it indicates the correctness of the core of the binding-timeanalyses of Bondorf (1991) and Consel (1990). By “the core” of an analysis we meanits restriction to the λ-calculus.Finally, we prove that all partial evaluators will on termination have eliminatedall “eliminable”-marked parts of an input which satisfies our condition. This gen-eralizes a result of Gomard who proved that a particular partial evaluator willon termination have eliminated all “eliminable”-marked parts of a well-annotatedprogram.Our consistency criterion is true of the output of radically different binding timeanalyses. The binding-time analysis of Gomard and Jones is based on so-calledpartial type inference. The analysis of Mogensen extends it with the use of recursivetypes. The binding-time analyses of Bondorf and Consel are based on an abstractinterpretation called closure analysis.Our results demonstrate that a partial evaluation strategy can be changed with-out affecting the correctness of the chosen binding-time analysis. We focus on anovel family of so-called top-down partial evaluators and prove that if such one isgiven a consistent input, then it cannot “go wrong”.Our development is for the pure λ-calculus with explicit binding-time annota-tions. This allows us to concentrate on the higher-order aspects of binding-timeanalysis.In the following section we define the pure λ-calculus with explicit binding-timeannotations, the so-called 2-level λ-calculus. In section 3 we introduce the key con-cept of consistent 2-level λ-terms, and we present the family of top-down partialevaluators for the 2-level λ-calculus. In section 4 we recall the consistency conditionstudied by Schwartzbach and the present author. In section 5 we state our results,and in section 6 we prove the required lemmas. Finally, in section 7 we conclude.2 The 2-level λ-calculusAs a basis for discussing the input to binding-time analyses we start by recallingthe pure λ-calculus (Barendregt, 1981).Definition 1The language of λ-terms is defined by the grammar:E ::=x (variable)| λx.E (abstraction)| E1@ E2(application)An occurrence of (λx.E) @ E0is called a redex. The semantics is as usual given byCorrectness of Binding-time Analysis 3the rewriting rule scheme:(λx.E) @ E0→ E[E0/x] (beta-reduction)Here, E[E0/x] denotes the term E with E0substituted for free occurrences of x(after renaming bound variables if necessary). We write ES→∗ETto denote thatEThas been obtained from ESby 0 or more beta-reductions. A term without redexesis said to be in normal form. We use the convention that application associates tothe left.To simplify matters, we will assume that the input to a binding-time analysis isjust one λ-term that encodes both the term to be analyzed and the known input.For example, suppose we want to analyze the term E which takes its input throughthe free variables x and y. Suppose also that the value of x is known to be E0andthat the value of y is unknown. We will then supply the analysis with the term(λx.E) @ E0. Notice that y is free also in this term. Thus, free variables henceforthcorrespond to unknown input.The output of a binding-time analysis can be presented as an annotated versionof the analyzed term. In the annotated term, all residual abstractions and appli-cations are underlined. The language of annotated terms is