scholarly journals RS-2 Tagging, Encoding, and Jones Optimality

2003 ◽  
Vol 10 (2) ◽  
Author(s):  
Olivier Danvy ◽  
Pablo E. Martínez López
Keyword(s):  
Partial Evaluation ◽  
Higher Order ◽  
The Self ◽  
Abstract Syntax ◽  
Original Source ◽  
Simple Representation ◽  
Residual Program ◽  
Source Program

A partial evaluator is said to be Jones-optimal if the result of specializing a self-interpreter with respect to a source program is textually identical to the source program, modulo renaming. Jones optimality has already been obtained if the self-interpreter is untyped. If the self-interpreter is typed, however, residual programs are cluttered with type tags. To obtain the original source program, these tags must be removed.<br /> <br />A number of sophisticated solutions have already been proposed. We observe, however, that with a simple representation shift, ordinary partial evaluation is already Jones-optimal, modulo an encoding. The representation shift amounts to reading the type tags as constructors for higher-order abstract syntax. We substantiate our observation by considering a typed self-interpreter whose input syntax is higher-order. Specializing this interpreter with respect to a source program yields a residual program that is textually identical to the source program, modulo renaming.

A partial evaluator for the untyped lambda-calculus

1991 ◽  
Vol 1 (1) ◽  
pp. 21-69 ◽  
Author(s):  
Carsten K. Gomard ◽  
Neil D. Jones
Keyword(s):  
Input Data ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Higher Order ◽  
Residual Program ◽  
Source Program ◽  
Point Operator ◽  
Free Subset ◽  
Residual Code ◽  
Lambda Expression

AbstractThis article describes theoretical and practical aspects of an implemented self-applicable partial evaluator for the untyped lambda-calculus with constants and a fixed point operator. To the best of our knowledge, it is the first partial evaluator that is simultaneously higher-order, non-trivial, and self-applicable.Partial evaluation produces aresidual programfrom a source program and some of its input data. When given the remaining input data the residual program yields the same result that the source program would when given all its input data. Our partial evaluator produces a residual lambda-expression given a source lambda-expression and the values of some of its free variables. By self-application, the partial evaluator can be used to compile and to generate stand-alone compilers from a denotational or interpretive specification of a programming language.An essential component in our self-applicable partial evaluator is the use of explicitbinding time information.We use this to annotate the source program, marking asresidualthe parts for which residual code is to be generated and marking aseliminablethe parts that can be evaluated using only the data that is known during partial evaluation. We give a simple criterion,well-annotatedness,that can be used to check that the partial evaluator can handle the annotated higher-order programs without committing errors.Our partial evaluator is simple, is implemented in a side-effect free subset of Scheme, and has been used to compile and to generate compilers and a compiler generator. In this article we examine two machine-generated compilers and find that their structures are surprisingly natural.

scholarly journals Higher-Order Rewriting and Partial Evaluation

1997 ◽  
Vol 4 (46) ◽  
Author(s):  
Olivier Danvy ◽  
Kristoffer H. Rose
Keyword(s):  
Partial Evaluation ◽  
Expressive Power ◽  
Higher Order ◽  
Program Transformations ◽  
Residual Program ◽  
Reduction System ◽  
Case Basis ◽  
Exotic Property

We demonstrate the usefulness of higher-order rewriting techniques for specializing programs, i.e., for partial evaluation. More precisely, we demonstrate how casting program specializers as combinatory reduction systems (CRSs) makes it possible to formalize the corresponding program transformations as meta-reductions, i.e., reductions in the internal "substitution calculus." For partial-evaluation problems, this means that instead of having to prove on a case-by-case basis that one's "two-level functions" operate properly, one can concisely formalize them as a combinatory reduction system and obtain as a corollary that static reduction does not go wrong and yields a well-formed residual program.<br />We have found that the CRS substitution calculus provides an adequate expressive power to formalize partial evaluation: it provides sufficient termination strength while avoiding the need for additional restrictions such as types that would complicate the description unnecessarily (for our purpose). We also review the benefits and penalties entailed by more expressive higher-order formalisms. In addition, partial evaluation provides a number of examples of higher-order rewriting where being higher order is a central (rather than an occasional or merely exotic) property. We illustrate this by demonstrating how standard but non-trivial partial-evaluation examples are<br />handled with higher-order rewriting.

scholarly journals A Simple Take on Typed Abstract Syntax in Haskell-like Languages

2000 ◽  
Vol 7 (34) ◽  
Author(s):  
Olivier Danvy ◽  
Morten Rhiger
Keyword(s):  
Normal Forms ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Higher Order ◽  
Abstract Syntax ◽  
Typed Lambda Calculus

<p>We present a simple way to program typed abstract syntax in a <br />language following a Hindley-Milner typing discipline, such as Haskell and ML, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: normalization functions (1) preserve types and (2) yield long beta-eta normal forms.</p><p>Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.</p>

scholarly journals Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages

2009 ◽  
Vol 19 (5) ◽  
pp. 509-543 ◽  
Author(s):  
JACQUES CARETTE ◽  
OLEG KISELYOV ◽  
CHUNG-CHIEH SHAN
Keyword(s):  
Partial Evaluation ◽  
Higher Order ◽  
Dependent Types ◽  
Abstract Syntax ◽  
Object Language ◽  
Data Types ◽  
Initial Algebra ◽  
The Family ◽  
De Bruijn ◽  
Algebraic Data Types

AbstractWe have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.

Combined influence of axial electron temperature and exponential plasma density ramp on the self-focusing of a chirped laser in plasma

2020 ◽  
Vol 75 (7) ◽  
pp. 671-675
Author(s):  
Niti Kant ◽  
Vishal Thakur
Keyword(s):  
Electron Temperature ◽  
Pulse Laser ◽  
Plasma Density ◽  
Beam Width ◽  
Spot Size ◽  
Higher Order ◽  
The Self ◽  
Chirped Pulse ◽  
Self Focusing ◽  
Paraxial Ray

AbstractAn analysis of the self-focusing of highly intense chirped pulse laser under exponential plasma density ramp with higher order value of axial electron temperature has been done. Beam width parameter is derived by using paraxial ray approximation and then solved numerically. It is seen that self-focusing of chirped pulse laser is intensely affected by the higher order values of axial electron temperature. Further, influence of exponential plasma density ramp is studied and it is concluded that self-focusing of laser enhances and occurs earlier. On the other hand defocusing of beam reduces to the great extent. It is noticed that the laser spot size reduces significantly under joint influence of the density ramp and the axial electron temperature. Present analysis may be useful for the analysis of quantum dots, the laser induced fusion and etc.

scholarly journals Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs

10.29007/jqtz ◽  
2018 ◽  
Author(s):  
Nada Habli ◽  
Amy P. Felty
Keyword(s):  
Programming Languages ◽  
Automatic Generation ◽  
Higher Order ◽  
Specification Language ◽  
Proof Assistants ◽  
Abstract Syntax ◽  
Formal Systems ◽  
Ongoing Work ◽  
General Specification ◽  
Automated Proof

We describe ongoing work on building an environment to support reasoning in proof assistants that represent formal systems using higher-order abstract syntax (HOAS). We use a simple and general specification language whose syntax supports HOAS. Using this language, we can encode the syntax and inference rules of a variety of formal systems, such as programming languages and logics. We describe our tool, implemented in OCaml, which parses this syntax, and translates it to a Coq library that includes definitions and hints for aiding automated proof in the Hybrid system. Hybrid itself is implemented in Coq, and designed specifically to reason about such formal systems. Given an input specification, the library that is automatically generated by our tool imports the general Hybrid library and adds definitions and hints for aiding automated proof in Hybrid about the specific programming language or logic defined in the specification. This work is part of a larger project to compare reasoning in systems supporting HOAS. Our current work focuses on Hybrid, Abella, Twelf, and Beluga, and the specification language is designed to be general enough to allow the automatic generation of libraries for all of these systems from a single specification.

Sign in / Sign up

Export Citation Format

Share Document