PE1996, Abstracts
-
Global Control for Partial Deduction through Characteristic Atoms and Glo
bal Trees
-
Michael Leuschel and Bern Martens
-
Compiler Generation for Interactive Graphics using Intermediate Code
-
Scott Draves
-
An approach for the understanding of scientific application programs based on program specialization
-
Sandrine BLAZY, Philippe FACON
-
Program specialization via program slicing
-
Thomas Reps and Todd Turndige
-
Current Developments in Partial Evaluation for Equational Programs
-
Alain Miniussi, David Sherman
-
Practical Aspects of Specialization
of Algol-like Programs
-
Mikhail A. Bulyonkov and
Dmitrij V. Kochetov
-
Multi-Level Lambda-Calculi: an Algebraic Description
-
Flemming Nielson and Hanne Riis Nielson
-
Efficiently Generating Efficient Generating Extensions in Prolog
-
Jesper J{\o}rgensen and Michael Leuschel
-
Pragmatics of Type-Directed Partial Evaluation
-
Olivier Danvy
-
Synchronization Analyses for Multiple Recursion Parameters
-
WN Chin, SC Khoo, P Thiemann
-
What {\em Not} to Do When Writing an Interpreter for Specialisation
-
Neil D. Jones
-
A Uniform Approach
for Compile-Time and Run-Time Specialization
-
Charles Consel, Luke Hornof, Francois Noel, Jacques Noyé, Nicolae Volanschi
-
Regular Approximation of Computation Paths
in Logic and Functional Languages
-
J.P. Gallagher and L. Lafave
-
Compiler Generation for Interactive Graphics using Intermediate Code
-
Scott Draves
-
Type Specialisation for the Lambda Calculus
-
John Hughes
-
Reasoning about Hierarchies of Online Program Specialization Systems
-
John Hatcliff, Robert Glueck
-
Automatic Techniques for
Logic Program Specialization
-
Alberto Pettorossi and Maurizio Proietti
-
ML pattern match compilation and partial evaluation
-
Peter Sestoft
-
Specialization of Imperative Programs through
Analysis of Relational Expressions
-
Alexander Sakharov
-
A Roadmap to Metacomputation by Supercompilation
-
Robert Gl{\"u}ck and Morten Heine S{\o}rensen
-
A Self-Applicable Supercompiler
-
Andrei P. Nemytykh and Victoria A. Pinchuk and Valentin F. Turchin
-
Evolution of Partial Evaluators: Removing Inherited Limits.
-
Torben Æ. Mogensen
-
Self-Applicable Online Partial Evaluation
-
Michael Sperber
Author:
Michael Leuschel and Bern Martens
Keywords:
partial deduction, online control, global control, characteristic trees, termination
Abstract:
Recently, considerable advances have been made in the (online) control
of logic program specialisation.
A clear conceptual distinction has been established between local and
global control and on both levels concrete strategies as well as
general frameworks have been proposed.
For global control in particular, recent work has developed concrete techniques
based on the preservation of characteristic trees
(limited, however, by a given, arbitrary depth bound)
to obtain a very precise control of polyvariance.
On the other hand, the concept of an m-tree has been introduced
as a refined way to trace ``relationships'' of partially deduced atoms,
thus serving as the basis for a general framework within which global termination
of partial deduction can be ensured in a non ad hoc way.
Blending both, formerly separate, contributions,
in this paper, we present an elegant and sophisticated technique
to globally control partial deduction of normal logic programs.
Leaving unspecified the specific local control one may wish to plug in,
we develop a concrete global control strategy combining the use
of characteristic atoms and trees with global (m-)trees.
We thus obtain partial deduction that always terminates in an elegant,
non ad hoc way, while providing excellent specialisation as well as
fine-grained (but reasonable) polyvariance.
We conjecture that a similar approach may contribute to improve
upon current (online) control
strategies for functional program tranformation methods such as (positive)
supercompilation.
Author:
Scott Draves
Keywords:
graphics, compiler generation, intermediate representation, meta-level systems
Abstract:
This paper describes a compiler generator (cogen) designed
for interactive graphics, and presents preliminary results of its
application to pixel-level code. The cogen accepts and produces a
reflective intermediate code in continuation passing, closure passing
style (CPS-CPS). This allows low overhead runtime code generation
(RTCG) as well as multi-stage compiler generation. {\tt{}cogen} is novel
because it supports unrestricted lifting and {\em{}partially static integers\/}. In addition to standard partial evaluation examples, we
examine graphics kernels such as bcopy, 1D finite filtering, and
packed sub-word-sized pixel access.
Author:
Sandrine BLAZY, Philippe FACON
Keywords:
software maintenance, program understanding, program specialization, interprocedural analysis, formal specification, inference rules, Fortran
Abstract:
This paper reports on an approach for improving the
understanding of old programs which have become very complex due to numerous extensions. We have adapted
partial evaluation techniques for program understanding. These techniques mainly use propagation through
statements and simplifications of statements. We focus here on the automatic interprocedural analysis and
we specify both tasks for call-statements, in terms of inference rules with notations taken from the
specification languages B and VDM. We describe how we have implemented in a tool and used that interprocedural
analysis to improve program understanding. The difficulty of that analysis comes from the lack of well defined
interprocedural mechanisms and the complexity of visibility rules in Fortran.
Author:
Thomas Reps and Todd Turndige
Keywords:
program projection, program slicing, program specialization,
projection function
Abstract:
In this paper, we show how program slicing can be used to perform a certain kind of program-specialization operation.
The specialization operation that slicing performs is different from
the specialization operations performed by algorithms for partial
evaluation, supercompilation, bifurcation, or deforestation.
In particular, we give examples in which the specialized programs that
we create via slicing could not be created as the result of applying partial evaluation, supercompilation, bifurcation, or deforestation to
the original unspecialized program. The parameters to functions and procedures define the range of usage
patterns that the designer of a piece of software has anticipated.
In this sense, partial evaluation, supercompilation, and bifurcation
are somewhat limited:
They support tailoring of existing software only in ways that have
already been ``foreseen'' by the software's author.
In contrast, the specialization operation that slicing supports
permits programs to be specialized in ways that did not have to be
anticipated by the writer of the original program.
Author:
Alain Miniussi, David Sherman
Keywords:
equational programming, call unfolding, intermediate code
Abstract:
Equational programs, which use term-rewriting as their basic
implementation method, can be greatly improved by partial evaluation
of intermediate code programs written in EM~code.
Such transformation removes various kinds of overhead associated with
rewriting, such as intermediate rewriting steps, boxing and unboxing
of arithmetic values, and intermediate constructions resulting from
recursive definitions.
Unfolding strategies for equational programs must be both
\emph{terminating}, and \emph{good enough} with respect to pragmatic
criteria.
In this paper we give a general introduction to the particular
problems associated with partial evaluation of equational programs,
and propose some criteria for deciding whether an unfolding strategy
is good enough from a practical standpoint.
We then present a new algorithm for driving unfolding of EM~code
programs, and show that, in addition to terminating, it
produces a good result.
As we have already implemented the new strategy, this final point is
demonstrated with a number of concrete examples.
Author:
Mikhail A. Bulyonkov and
Dmitrij V. Kochetov
Keywords:
Specialization of imperative programs,
memory requirements, configuration analysis.
Abstract:
A ``linearized'' scheme of polyvariant specialization for
imperative languages is described in the paper. The scheme
is intended for increasing efficiency of specialization.
Main properties of the scheme are linear generation of
residual code and single memory shared by different
variants of specialization process. The scheme was used in
partial evaluator for the Modula-2 language. Some
benchmarks of the evaluator are discussed to demonstrate
efficiency of the processor.
Author:
Flemming Nielson and Hanne Riis Nielson
Keywords:
Abstract:
Two-level lambda-calculi have been heavily utilised for applications
such as partial evaluation, abstract interpretation and code
generation. Each of these applications pose different demands on the
exact details of the two-level structure and the corresponding
inference rules. We therefore formulate a number of existing systems in
a common framework. This is done in such a way as to conceal those
differences between the systems that are not essential for the
multi-level ideas (like whether or not one restricts the domain of the
type environment to the free identifiers of the expression) and thereby
to reveal the deeper similarities and differences. In their most
general guise the multi-level lambda-calculi allow multi-level
structures that are not restricted to (possibly finite) linear orders
and thereby generalise previous treatments in the literature.
Author:
Jesper J{\o}rgensen and Michael Leuschel
Keywords:
partial deduction, off-line specialization, cogen approach
Abstract:
The so called ``cogen approach'', writing a compiler generator instead of a specializer, to program specialization has been used with considerably success in partial evaluation of both functional and imperative languages. This paper demonstrates that this approach is also applicable to partial evaluation of logic programming languages, also called partial deduction. Self-application has not been as much in focus in partial deduction as in partial evaluation of functional and imperative languages, and the attempts to self-apply partial deduction system have, of yet, not been all together that succesful. So especially for partial deduction the cogen approach could prove to have a considerable importance when it come to practical applications. It is demonstrated that using the cogen approach one gets very efficient compiler generators which generate very efficient generating extensions which in turn yield very good and non-trivial specialisation.
Author:
Olivier Danvy
Keywords:
Abstract:
Type-directed partial evaluation stems from the residualization of
arbitrary static values in dynamic contexts, given their type. Its
algorithm coincides with the one for coercing a subtype value into a
supertype value, which itself coincides with the one of normalization in
the $\lambda$-calculus. Type-directed partial evaluation is thus used
to specialize compiled, closed programs, given their type.
Since Similix, let-insertion is a cornerstone of partial evaluators for
call-by-value procedural programs with computational effects. It
prevents the duplication of residual computations, and more generally
maintains the order of dynamic side effects in residual programs.
This article describes the extension of type-directed partial evaluation
to insert residual let expressions. This extension requires the user to
annotate arrow types with effect information. It is achieved by
delimiting and abstracting control, comparably to continuation-based
specialization in direct style. It enables type-directed partial
evaluation of effectful programs (\eg, a definitional lambda-interpreter
for an imperative language) that are in direct style. The residual
programs are in A-normal form.
Author:
WN Chin, SC Khoo, P Thiemann
Keywords:
Keywords: Program Transformation, Tupling, Memoisation, Synchronization Analyses, Multiple Recursion Parameters, Termination Proofs
Abstract:
Tupling is a transformation tactic to obtain new functions, without redundant calls and/or multiple traversals of common inputs. In \cite{Chin:PEPM93}, we presented an automatic method for tupling functions with a single recursion parameter each.
In this paper, we propose a new family of parameter analyses, called {\em synchronization analyses}, to help extend the tupling method to functions with multiple recursion parameters. To achieve better optimisation, we formulate three different forms of tupling optimisations for
the elimination of intra-call traversals, the elimination of inter-call traversals and the elimination of redundant calls. We also guarantee the safety of the extended method by ensuring that its transformation always terminates.
Author:
Neil D. Jones
Keywords:
Abstract:
A partial evaluator, given a program and a known ``static'' part of its input
data, outputs a residual program in which computations depending only
on the static data have been performed.
{\em Ideally} the partial evaluator would be a
``black box'' able to extract nontrivial static computations whenever possible;
which never fails to terminate; and which always produces residual programs of
reasonable size and maximal efficiency, so all possible static computations have
been done. {\em Practically} speaking, partial evaluators fall short of
this goal;
they may loop, sometimes pessimise, and/or explode code size.
A partial evaluator is analogous to a spirited horse: while impressive results
can be obtained when used well, the user must know what he/she is doing.
Our thesis
is that {\em this knowledge can be communicated} to new users of these tools.
This paper preesents a series of examples, concentrating on a
quite broad and on the whole successful application area: using
specialisation to
remove interpretational overhead. It presents a series of examples, both
positive
and negative, to illustrate the effects of program style on the efficiency and
size of the of target programs obtained by specialising an interpreter with
respect to a known source program.
Author:
Charles Consel, Luke Hornof, Francois Noel, Jacques Noyé, Nicolae Volanschi
Keywords:
Abstract:
As partial evaluation gets more mature, it is now possibel to use
this program transformation technique to tackle realistic languages and
real-size application programs. However, this evolution raises a number of
critical issues that need to be addressed before the approach becomes truly
practical.
First of all, most existing partial evaluators have been developed based on
the assumption that they could process any kind of application program. This
attempt to develop universal partial evaluators does not address some
critical needs of real-size application programs. Furthermore, as partial
evaluators treat richer and richer languages , their size and complexity
increase drastically. This increasing complexity revealed the need to
enhance design principles. Finally, exclusively specializing programs at
compile time seriously limits the applicability of partial evaluation since
a large class of invariants in real-size programs are not known until run
time and therefore cannot be taken into account.
In this paper, we propose design principles and techniques to deal with each
of these issues.
By defining an architecture for a partial evaluator and its essential
components, we are able to to tackle a rich language
linke C without compromising the design and the structure of the resulting
implementation.
By designing a partial evaluator targeted towards a specific application
area, namely system software, we have developed a system capable of treating
realisitc programs.
Because our approach to designing a partial evaluator clearly separates
preprocessing and processing aspects, we are able to introduce run-time
specialization in our partial evaluation system as a new way of exploiting
information produced by the preprocessing phase.
Author:
J.P. Gallagher and L. Lafave
Keywords:
Abstract:
The aim of this work is to compute descriptions of successful
computation paths in logic or functional program executions. Computations
paths are represented as terms, built from special constructor symbols, each
constructor and symbol corresponding to a specific clause or equation in a
program. Such terms, called trace-terms, are abstractions of computation
trees, which capture information about the control flow of the program. A
method of appoximating trace-terms is described, based on well-established
methods for computing regular approximations of terms. The special function
symbols are first introduced into programs as extra arguments in predicates
or functions. Then a regular approximation (with respect to a given class of
program executions) is computed, giving a regular description of the terms
appearing in every argument in the program. The approximation of the extra
arguments (the trace-terms) can then be examined to see what computation
paths were followed during the computation. This information can then be
used to control an off-line specialisation system. A key aspect of the
analysis is the use of suitable widening operations during the regular
approximation, in order to preserve information on determinacy and branching
structure of the computation. This method is applicable to both logic and
functional languages, and appears to offer appropriate control information
in both formalisms.
Author:
Scott Draves
Keywords:
cogen, graphics, continuations, binding times
Abstract:
This paper describes a compiler generator (cogen) designed for interactive graphics, and presents preliminary results of its application to pixel-level code. The cogen accepts and produces a reflective intermediate code in continuation-passing, closure-passing style. This allows low overhead run-time code generation as well as multi-stage compiler generation. We extend partial evaluation techniques by allowing unrestricted lifting and {em partially static integers}. In addition to some standard examples, we examine graphics kernels such as bcopy, one-dimensional finite filtering, and packed pixel access.
Author:
John Hughes
Keywords:
type specalisation lambda calculus
Abstract:
Partial evaluation of typed languages has long suffered from the problem
that the types appearing in residual programs are constrained too strongly
by those appearing in the unspecialised original program. In the simplest
case, the only types that can appear in residual programs are those from the
original source. When for example programs are compiled by specialising an
interpreter, then the only types that can appear in the compiled code are
those used in the interpreter. In particular, since the interpreter must
represent values of different types by injecting them into a universal type,
then in the compiled code values are also tagged members of this type, and
tags must be checked whenever a value is used. If the language being
compiled is itself typed, then these tags and checks are unnecessary. When
the interpreter is a self-interpreter, the `optimality' criterion is not
met:
mix sint p ~= p
because the left hand side tags its data and the right hand side does not.
In this paper we present what we believe is the first partial evaluator that
can remove these tags. The object language is the simply typed lambda
calculus with a two-level type system: static tags are removed, while
dynamic tags remain.
A novel feature of our partial evaluator is that we can derive static
information about expressions which others treat as purely dynamic, such as
a dynamic conditional. But just as compilers reject programs whose types do
not match, so our partial evaluator rejects programs whose static
information does not match. For example, the two arms of a dynamic
conditional must carry the same static information.
We are forced to relax the functional nature of the mapping from source
expressions to static information; rather a relation holds between them,
which means that the same source expression may be related to many different
static values. Static information can't be computed by a bottom-up
evaluation, therefore, and indeed our specialiser is expressed not as an
interpreter, but as a system of inference rules specifying how static
information can be inferred. Unsurprisingly, the inference of static
information (which includes type information) is very similar to type
inference.
The static value inferred for an expression is then used to derive a
suitable residual type for the specialised expression. Since the same
expression in the source can be related to many different static values, its
specialisations can have many different residual types.
An interesting aspect is that our specialiser need not use unfolding: we can
`evaluate' static expressions without unfolding function calls by inferring
their static value. To demonstrate this we have implemented a specialised
which doesn't unfold at all. But for this reason our specialiser is not
`optimal': when we compute
mix sint p
we eliminate type tags, but the residual program must be unfolded somewhat
in order to recover p.
The present specialised is just a toy, but we believe the techniques will
scale up to make possible improved specialisation of real typed languages.
Author:
John Hatcliff, Robert Glueck
Keywords:
program encodings, abstract machines, online partial evaluation, self-application, super-compilation
Abstract:
The conventional wisdom is that online techniques are not well-suited
for obtaining useful results from metasystem hierarchies. However,
this conclusion ignores both practical and theoretical progress. Our
goal is to identify and clarify the foundational issues involved in
hierarchies of online specialization systems. To achieve this, we
develop a very simple online specialization system which focuses
tightly on the following problematic points of online specialization:
(1) semantics of specialization, (2) properties of program
encodings and identifying position of entities in a hierarchy, (3)
tracking unknown values across levels in metasystem hierarchies.
Author:
Alberto Pettorossi and Maurizio Proietti
Keywords:
Abstract:
We address the problem of specializing logic programs w.r.t. sets
of partially known input data. We assume that, at compile time, we are given
a property of the input data as a conjunction of atoms defined by sets of
clauses of teh logic program to be specialised. We describe a general method
which, given a program P and a property of the input data, allows us to
derive a specialized program P' such that P and P' are equivalent w.r.t.
each input data satisfying property . The correctness of our technique is
shown by a proof method based on unfolding and folding transformations. Our
specialization method makes use of a technique for program generalization
which is needed for improving the efficiency of the specialized program.
Author:
Peter Sestoft
Keywords:
ML pattern matching, compilation,
Knuth-Morris-Pratt string matching
Abstract:
We demonstrate a method for compiling ML-style pattern matches.
The method is conceptually simple and produces reasonably good compiled
matches. The approach is inspired by the instrumentation and partial
evaluation of naive matchers, as pioneered by Consel and Danvy for string
matching, adn carried over to tree matching by Jorgensen.
Following that paradigm, we first present a naive ML pattern matcher,
instrument it to collect and exploit extra information, and show that
partial evaluation of the instrumented general matcher with respect to a
given match produces an efficient specialized matcher.
We then discard the partial evaluation step and show that a match compiler
can be obtained just by slightly modifying the instrumented general matcher.
The resulting matchers naturally detect inexhaustive matches and redundant
match rules. The match compiler can be used for lazy languages (e.g.
Haskell) as well as strict ones (e.g. Standard ML).
Author:
Alexander Sakharov
Keywords:
imperative languages, program specialization, control flow
graphs, data flow analysis, fixpoint algorithms, interpretation of conditional
branches, polyvariant specialization.
Abstract:
An original analysis method for specialization of imperative programs is
described in this paper. This analysis is an inter-procedural data flow method
operating on control flow graphs and collecting information about program
expressions. It applies to various procedural languages. The set of analyzed
formulas includes equivalences between program expressions and constants,
linear-ordering inequalities between program expressions and constants,
equalities originating from some program assignments, and atomic constituents
of controlling expressions of program branches. Analysis is executed by a
worklist-based fixpoint algorithm which interprets conditional branches and
ignores some impossible paths. This analysis algorithm incorporates a simple
inference procedure that utilizes both positive and negative information.
The analysis algorithm is shown to be conservative; its asymptotic time
complexity is cubic. A polyvariant specialization of imperative programs,
that is based on the information collected by the analysis, is also
defined at the level of nodes and edges of control flow graphs. The
specialization incorporates a further refinement of analysis information
through local propagation. Multiple variants are produced by replicating
subgraphs whose in-links are limited to one node.
Author:
Robert Gl{\"u}ck and Morten Heine S{\o}rensen
Keywords:
Program transformation, supercompilation, driving,generalization, metacomputation, metasystem transition
Abstract:
This paper gives a gentle introduction to Turchin's supercompilation and its applications in metacomputation with an emphasis on recent developments. First, a complete supercompiler, including positive driving and generalization, is defined for a functional language and illustrated with examples. Then a taxonomy of related transformers is given and compared to the supercompiler. Finally, we put supercompilation into the larger perspective of metacomputation and consider three metacomputation tasks: specialization, composition, and inversion.
Author:
Andrei P. Nemytykh and Victoria A. Pinchuk and Valentin F. Turchin
Keywords:
program transformation,
supercompilation,
metacomputation,
self-applicaiton,
metasystem transition, MST-schemes, metacode,
Refal,
pattern-matching graphs
Abstract:
A {\em supercompiler} is a program which can perform a deep
transformation of programs using a principle which is similar to
{\em partial evaluation}, and can be referred to as {\em metacomputation}.
Supercompilers that have been in existence up to now
(see \cite{TNT82}, \cite{Tur86}) were not self-applicable: this is
a more difficult problem than self-application of a partial evaluator,
because of the more intricate logic of supercompilation.
In the present paper we describe the first self-applicable model
of a supercompiler and present some tests.
Three features distinguish it from the previous models and make
self-application possible:
(1)~The input language is a subset of Refal which we
refer to as {\em flat} Refal.
(2)~The process of {\em driving} is performed as
a transformation of {\em pattern-matching graphs}.
(3)~{\em Metasystem jumps} are implemented, which allows the supercompiler
to avoid interpretation whenever direct computation is possible.
Author:
Torben Æ. Mogensen
Keywords:
Partial evaluation, evolution, inherited limits
Abstract:
We show the evolution of partial evaluators over the past ten years from a particular perspective: the attempt to remove limits on the structure of residual programs that are inherited by structural bounds in the original programs. It will often be the case that a language allows an unbounded number or size of a particular features, but each program (being finite) will only have a finite number or size of these features. If the residual programs cannot overcome the bounds given in the original program, that can be seen as a weakness in the partial evaluator, as it potentially limits the effectiveness of residual programs. The inherited limits are best observed through specializing a self-interpreter and examining the object programs produced by specialisation of this. We show how historical developments in partial evaluators gradually remove inherited limits, and suggest how this principle can be used as a guideline for further development.
Author:
Michael Sperber
Keywords:
online partial evaluation, binding-time analysis, self-application
Abstract:
We propose a hybrid approach to partial evaluation to achieve
self-application of realistic online partial evaluators. Whereas
the offline approach to partial evaluation leads to efficient
specializers and self-application, online partial evaluators
perform better specialization at the price of efficiency. Moreover,
no online partial evaluator for a realistic language has been
successfully self-applied. We propose a binding-time analysis for
an online partial evaluator. The analysis distinguishes between
static, dynamic, and unknown binding times.
Thus, it makes some reduce/residualize decisions offline while
leaving others to the specializer. The analysis does not introduce
unnecessary generalizations. After some standard binding-time
improvements, our partial evaluator successfully self-applies.
Peter Thiemann