scholarly journals Binding Time Analysis: Abstract Interpretation vs. Type Inference

1992 ◽  
Vol 21 (393) ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Abstract Interpretation ◽  
Lambda Calculus ◽  
Type Inference ◽  
Time Analysis ◽  
Binding Time ◽  
Better Than ◽  
Binding Time Analysis

Binding time analysis is important in partial evaluators. Its task is to determine which parts of a program can be specialized 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 parts to be eliminable. The first is the abstract interpretation approach of Bondorf, and the second is the type inference approach o£ Gomard. Both apply to the untyped lambda calculus. We prove that Bondorf's analysis is better than Gomard's.

scholarly journals Polyvariant Analysis of the Untyped Lambda Calculus

1992 ◽  
Vol 21 (386) ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Fixed Point ◽  
Program Transformation ◽  
Lambda Calculus ◽  
Safety Analysis ◽  
Type Inference ◽  
Simple Type ◽  
Time Analysis ◽  
Fixed Point Computation ◽  
Binding Time ◽  
Binding Time Analysis

<p>We present a polyvariant closure, safety, and binding time analysis for the untyped lambda calculus. The innovation is to analyze each abstraction afresh at all syntactic application points. This is achieved by a semantics-preserving program transformation followed by a novel monovariant analysis, expressed using type constraints. The constraints are solved in cubic time by a single fixed-point computation.</p><p>Safety analysis is aimed at determining if a term will cause an error during evaluation. We have recently proved that the monovariant safety analysis accepts strictly more terms than simple type inference. This paper demonstrates that the polyvariant transformation makes even more terms acceptable, even some without higher-order polymorphic types. Furthermore, polyvariant binding time analysis can improve the partial evaluators that base a polyvariant specialization on only monovariant binding time analysis.</p>

A Temporal-Logic Approach to Binding-Time Analysis

1995 ◽  
Vol 2 (51) ◽  
Author(s):  
Rowan Davies
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Time Analysis ◽  
Typed Lambda Calculus ◽  
Binding Time ◽  
Logic Approach ◽  
Multi Level ◽  
Binding Time Analysis

<p>The Curry-Howard isomorphism identifies proofs with typed lambda-<br />calculus terms, and correspondingly identifies propositions with<br />types. We show how this isomorphism can be extended to relate<br />constructive temporal logic with binding-time analysis. In particular,<br />we show how to extend the Curry-Howard isomorphism<br />to include the   ("next") operator from linear-time temporal<br />logic. This yields the simply typed lambda-calculus which we prove<br />to be equivalent to a multi-level binding-time analysis like those<br />used in partial evaluation.</p><p><br />Keywords: Curry-Howard isomorphism, partial evaluation, binding-time analysis, temporal logic.</p>

Specifying the correctness of binding-time analysis

1993 ◽  
Vol 3 (3) ◽  
pp. 365-387 ◽  
Author(s):  
Mitchell Wand
Keyword(s):  
Flow Analysis ◽  
Lambda Calculus ◽  
Time Analysis ◽  
Correctness Criterion ◽  
Binding Time ◽  
Binding Time Analysis

AbstractMogensen 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.

scholarly journals Eta-Expansion Does The Trick

1995 ◽  
Vol 2 (41) ◽  
Author(s):  
Olivier Danvy ◽  
Karoline Malmkjær ◽  
Jens Palsberg
Keyword(s):  
Partial Evaluation ◽  
Lambda Calculus ◽  
Product Type ◽  
Proper Treatment ◽  
Time Analysis ◽  
Function Type ◽  
Dynamic Case ◽  
Unified View ◽  
Binding Time ◽  
Binding Time Analysis

Partial-evaluation folklore has it that massaging one's source programs can make them specialize better. In Jones, Gomard, and Sestoft's recent textbook, a whole chapter is dedicated to listing such "binding-time improvements'': non-standard use of continuation-passing style, eta-expansion, and a popular transformation called "The Trick''. We provide a unified view of these binding-time improvements, from a typing perspective.<br /> <br />Just as a proper treatment of product values in partial evaluation requires partially static values, a proper treatment of disjoint sums requires moving static contexts across dynamic case expressions. This requirement precisely accounts for the non-standard use of continuation-passing style encountered in partial evaluation. In this setting, eta-expansion acts as a uniform binding-time coercion between values and contexts, be they of function type, product type, or disjoint-sum type. For the latter case, it achieves "The Trick''.<br /> <br />In this paper, we extend Gomard and Jones's partial evaluator for the lambda-calculus, lambda-Mix, with products and disjoint sums; we point out how eta-expansion for disjoint sums does The Trick; we generalize our earlier work by identifying that eta-expansion can be obtained in the binding-time analysis simply by adding two coercion rules; and we specify and prove the correctness of our extension to lambda-Mix.<br /><br /> See revised version BRICS-RS-96-17.

scholarly journals Enhanced type inference for binding-time analysis

2020 ◽  
Vol 12 (2) ◽  
pp. 232-250
Author(s):  
Mátyás Szokoli ◽  
Attila Kiss
Keyword(s):  
Type Inference ◽  
Time Analysis ◽  
Analysis Algorithm ◽  
Speed Difference ◽  
Binding Time ◽  
Dynamic Typing ◽  
Binding Time Analysis

Abstract In this paper we will be taking a look at type inference and its uses for binding-time analysis, dynamic typing and better error messages. We will propose a new binding-time analysis algorithm ℬ, which is a modification of an already existing algorithm by Gomard [4], and discuss the speed difference.

Sign in / Sign up

Export Citation Format

Share Document