Sebastian Hunt, David Sands · 1991
Given a description of the parameters in a program that will be known at partial evaluation time, a binding time analysis must determine which parts of the program are dependent solely on these known parts (ancl therefore also known at partial evaluation time). In this paper a binding time analysis for the simply typed lambda calculus is presented. The analysis takes the form of an abstract interpretation and uses a novel formalisation of the problem of binding time analysis, based on the use of partial equivalence relations. A simple proof of correctness is achieved by the use of logical relations.
Cited by 61Open access
1993
Abstract Binding time analysis has proved to be a valuable pre-analysis for partial evaluation. Until now (almost) all binding time analyses have been monovariant, such that binding time analysis could assign only one binding time description to each function definition. This means that if a function f (x) is called once with dynamic data, no reductions on x can be performed in the body of f even when f is called with static data.
Cited by 0
Christian Mossin · 1994
Binding time analysis has proved to be a valuable pre-analysis for partial evaluation. Until now (almost) all binding time analyses have been monovariant, such that binding time analysis could assign only one binding time description to each function definition. This means that if a function f(x) is called once with dynamic data, no reductions on x can be performed in the body of f even when f is called with static data. There is currently great interest in polyvariant binding time analysis. Gengler and Rytz [Gengler & Rytz 1992a, Gengler & Rytz 1992b] use a kind of repeated abstract interpretation which is very slow. Consel [Consel 1992] avoids repeating the analysis by collapsing closure and binding time analysis and letting control flow information depend on binding time values. Both approaches copy (functions resp. binding time descriptions) in the “needed ” number of variants. Recently type inference has attracted much attention as a program analysis framework. This framework has been very successful in binding time analysis and
Cited by 0
Wim Vanhoof, Maurice Bruynooghe · 2001
Cited by 0
The MIT Press eBooks · 1999
In this work, we develop a binding-time analysis for the logic programming language Mercury.We introduce a precise domain of binding-times, based on the type information available in Mercury programs, that allows the analyser to reason with partially static data structures.The analysis is polyvariant, and deals with the module structure and higher-order capabilities of Mercury programs.
Cited by 4
Jens Palsberg · Journal of Functional Programming · 1993
Abstract A binding-time analysis is correct if it always produces consistent binding-time information. Consistency prevents partial evaluators from ‘going wrong’. A sufficient and decidable condition for consistency, called well-annotatedness, was first presented by Gomard and Jones. In this paper we prove that a weaker condition implies consistency. Our condition is decidable, subsumes the one of Gomard and Jones, and was first studied by Schwartzbach and the present author. Our result implies the correctness of the binding-time analysis of Mogensen, and it indicates the correctness of the core of the binding-time analyses of Bondorf and Consel. We also prove that all partial evaluators will on termination have eliminated all ‘eliminable’-marked parts of an input which satisfies our condition. This generalizes a result of Gomard. Our development is for the pure λ-calculus with explicit binding-time annotations.
Cited by 42Open access
Klimov Y.A.http://library.keldysh.ru/author_page.asp?aid=2965 · Соционет (Соционет/ЦЭМИ РАН/ИЭОПП СО РАН)
Abstract: \n Binding Time Analysis (BTA, BT-analysis) is an essential part of the Partial Evaluation (PE) technique of program specialization. The results of BT-analysis are used for decorating a program to be specialized with annotations, which are used later by the residual program generator. The specializer CILPE deals with programs written in SOOL, a simple Stack Object-Oriented Language. The paper present the approach to BT-analysis taken in CILPE. The annotations added to a SOOL program must satisfy certain requirements, which are formulated as a set of inference rules. The BT-analyzer in CILPE complies with these rules.
Cited by 0Open access
Sebastian Hunt, David Sands · 1991
Given a description of the parameters in a program that will be known at partial evaluation time, a binding time analysis must determine which parts of the program are dependent solely on these known parts (and therefore also known at partial evaluation time). In this paper a binding time analysis for the simply typed lambda calculus is presented. The analysis takes the form of an abstract interpretation and uses a novel formalisation of the problem of binding time analysis, based on the use of partial equivalence relations. A simple proof of correctness is achieved by the use of logical relations. 1 Introduction Given a description of the parameters in a program that will be known at partial evaluation time, a binding time analysis must determine which parts of the program are dependent solely on these known parts (and therefore also known at partial evaluation time). A binding time analysis performed prior to the partial evaluation process can have several practical benefits (see [...
Cited by 0
Lars Birkedal Morten, Morten Welinder · 1995
We present an efficient base algorithm for binding-time analysis based on constraint solving and the union-find algorithm. In practice it has been used to handle all of Standard ML except modules and we show the principles of how constraints can be used for binding-time analysis of Standard ML; in particular we show how to binding-time analyse nested pattern matching. To the best of our knowledge no previous binding-time analysis has treated nested pattern matching. This article is partly based on [BW93] in which we document the development of a semantics-based compiler generator, ML-Mix, for Standard ML programs. 1 Introduction There are two common ways of doing binding-time analysis: by fixed-point iteration and by constraint solving. Analyses based on the former method tend to be stronger [PS94], but have so far been rather slow (cubic complexity for higherorder languages) and thus impractical for large programs. Analyses based on the latter method are as fast as we can expect --...
Cited by 0
Kirsten Lackner Solberg, Hanne Riis Nielson, Flemming Nielson · 1992
this paper we shall take a logical approach and aim at constructing an algorithm for generating a set of constraints to be solved. In this way we will be able to make full use of substitutions as in ordinary type inference [8] --- this is contrary to other algorithms (e.g. [9]) where extra recursive calls have to be performed. The starting point for our work is the inference system for binding times of the simply typed -calculus as specified in [9]. This is reviewed in Section 2. However, we shall reformulate it in a style motivated by the inference system for linear types given in [13] using the so-called "use" types. This is described in Section 3. We construct an algorithm for binding time analysis from this inference system. This algorithm is O (n
Cited by 5
Rogardt Heldal, John Hughes · Lecture notes in computer science · 2001
Cited by 4
Ming Wang · 2001
The most important phase of partial evaluation is the binding time analysis(BTA), which works ahead to distinguish those computations which can be computed in partial evaluation time from which should be left to the running time, when the binding time information of the program's initial argument is given. However, we have discovered that existing partial evaluation technology can not effectively specialize existing realistic programs. This is due to that they are lack of accuracy of binding time analysis in dealing with typical features of imperative programs. In this paper, we introduce an approach that fundamentally differs from previous work in several respects, separate the different tasks performed by a binding time analysis into three distinct phases: binding time phase, recursive call analysis phase and sensitivity analysis phase. This separation simplifies the design of the analysis. Additionally, this approach allows us to express new program transformations, such as evaluating and residualizing the same program construct.
Cited by 2
Luke Hornof, Jacques Noyé · 1997
Since a binding-time analysis determines how an off-line partial evaluator will specialize a program, the accuracy of the binding-time information directly determines the degree of specialization. We have designed and implemented a binding-time analysis for an imperative language, and integrated it into our partial evaluator for C, called Tempo [9]. This binding-time analysis includes a number of new features, not available in any existing partial evaluator for an imperative language, which are critical when specializing existing programs such as operating system components [24, 25].• Flow sensitivity. A different binding-time description is computed for each program point, allowing the same variable to be considered static at one program point and dynamic at another.• Context sensitivity. Each function call is analyzed with the context of the call site, generating multiple binding-time annotated instances of the same function definition.• Return sensitivity. A different binding-time description is computed for the side-effects and the return value of a function.
Cited by 34Open access
Charles Consel · 1993
Binding-time analysis is a crucial component of an offline partial evaluator. The accuracy of the binding-time information that it produces determines the degree of specialization of programs.
Cited by 57Open access
Mitchell Wand · Journal of Functional Programming · 1993
Abstract Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for incorporating flow analyses into verified compilers.
Cited by 36Open access
Kenichi Asai · 2016
This paper relates 2-level lambda-calculus and staged lambda-calculus (restricted to 2 stages) to obtain monovariant binding-time analysis for lambda-calculus that produces the output in the form of staging annotations. The relationship between the two lambda-calculi provides us with a precise and easy instruction on how to implement binding-time analysis to be incorporated in the staged lambda-calculus. It forms a basis for introducing binding-time analysis to full-fledged staged languages such as MetaOCaml.
Cited by 4
Neil D. Jones · Theoretical Computer Science · 1991
Cited by 12
2008
First-order projection-based binding-time analysis has proven genuinely useful in partial evaluation [Lau91a, Lau91c]. There have been three notable generalisations of projection-based analysis to higher order. The first lacked a formal basis [Mog89]; the second used structures strictly more general that projections, namely partial equivalence relations (PERs) [HS91]; the third involved a complex construction that gave rise to impractically large abstract domains [Dav93]. This paper presents a technique free of these shortcomings: it is simple, entirely projection-based, satisfies a formal correctness condition, and gives rise to reasonably small abstract domains. Though the technique is cast in terms of projections, there is also an interpretation in terms of PERs. The principal limitation of the technique is the restriction to monomorphic typing. 1
Cited by 0
Jens Palsberg, Michael I. Schwartzbach · 2002
Binding-time analysis is important in partial evaluators. Its task is to determine which parts of a program can be evaluated if some of the expected input is known. Two approaches to do this are abstract interpretation and type inference. We compare two specific such analyses to see which one determines most program ports to be eliminable. The first is a an abstract interpretation approach based on closure analysis and the second is the type inference approach of Gomard and Jones (1991). Both apply to the pure /spl lambda/-calculus. We prove that the abstract interpretation approach is more powerful than that of Gomard and Jones: the former determines the same and possibly more program parts to be eliminable as the latter.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
Cited by 27
Kirsten Lackner Solberg, Hanne Riis Nielson, Flemming Nielson · 1992
) Kirsten Lackner Solberg Dept. of Math. and Computer Science Odense University, Denmark e-mail: kls@imada.ou.dk Hanne Riis Nielson Flemming Nielson Computer Science Department Aarhus University, Denmark e-mail: fhrn, fng@daimi.aau.dk 1 Introduction We consider the problem of introducing a distinction between binding times (e.g. compile-time and run-time) into functional languages. It is well-known that such a distinction is important for the efficient implementation of imperative languages (Aho et al., 1986) and more recent results show that the performance of functional languages may be improved by using binding time information (e.g. Nielson and Nielson (1989) and Jrgensen (1992)). There are several approaches to the specification of binding time analyses. Some approaches are based on variants of abstract interpretation (e.g. Bondorf (1990), Consel (1990), and Hunt and Sands (1991)), others are based on projection analysis (e.g. Launchbury (1991)), and yet others (e.g. Ni...
Cited by 0