Search

We introduce a language-independent framework for reasoning about program inverters by conditional term rewriting systems. These systems can model the three fundamental forms of inversion, i.e., full, partial and semi-inversion, in declarative languages. The correctness of the generic inversion algorithm introduced in this contribution is proven for all well-behaved rule inverters, and we demonstrate that this class of inverters encompasses several of the inversion algorithms published throughout the past years. This new generic approach enables us to establish fundamental properties, e.g., orthogonality, for entire classes of well-behaved full inverters, partial inverters and semi-inverters regardless of their particular local rule inverters. We study known inverters as well as classes of inverters that yield left-to-right deterministic systems; left-to-right determinism is a desirable property, e.g., for functional programs; however, at the same time it is not generally a property of inverted systems. This generic approach enables a more systematic design of program inverters and fills a gap in our knowledge of program inversion.

Inversion is an important and useful program transformation and has been studied in various programming language paradigms. Semi-inversion is more general than just swapping the input and output of a program; instead, parts of the input and output can be freely swapped. In this paper, we present a polyvariant semi-inversion algorithm for conditional constructor term rewriting systems. These systems can model logic and functional languages, which have the advantage that semi-inversion, as well as partial and full inversion, can be studied across different programming paradigms. The semi-inverter makes use of local inversion and a simple but effective heuristic and is proven to be correct. A Prolog implementation is applied to several problems, including inversion of a simple encrypter and of a program inverter for a reversible language.

Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, Giles studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modeling reversible functional programming, notably morphism schemes for reversible recursion, a †-trace, and algebraic ω -compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles regarding the formulation of recursive data types at the inverse category level.

We present an algorithm for inverse computation in a first-order functional language based on the notion of a perfect process tree. The Universal Resolving Algorithm introduced in this paper is sound and complete, and computes each solution for which the given program terminates, in finite time. The algorithm has been implemented for TSG, a typed dialect of S-Graph, and shows some remarkable results for the inverse computation of functional programs such as a pattern matcher and an interpreter for imperative programs.

We survey fundamental concepts for inverse programming and then present the Universal Resolving Algorithm, an algorithm for inverse computation in a first-order, functional programming language. We discuss the key concepts of the algorithm, including a three-step approach based on the notion of a perfect process tree, and demonstrate our implementation with several examples of inverse computation.

Structures using constructors are of ordinary use in functional programming to represent data structures of unbound size. Lack of associativity of constructors, however, hinders program analyses or efficient executions. This paper describes ideas of abstraction toward constructors, and similarly abstraction from constructing functions, which we call functional constructors. We demonstrate our ideas making program analyses easier and enable transformation to efficient execution.

Program specialization can divide a computation into several computation stages. This paper investigates the theoretical limitations and practical problems of standard specialization tools, presents multi-level specialization, and demonstrates that, in combination with the cogen approach, it is far more practical than previously supposed. The program generator which we designed and implemented for a higher-order functional language converts programs into very compact multi-level generating extensions that guarantee fast successive specialization. Experimental results show a remarkable reduction of generation time and generator size compared to previous attempts of multi-level specialization by self-application. Our approach to multi-level specialization seems well-suited for applications where generation time and program size are critical.

We currently have limited understanding of how complex data (e.g. algebraic data types) can be represented and manipulated in reversible machine code, in particular without generating garbage. In this paper we present methods for representing and manipulating binary trees (constructor terms) in the heap of a reversible machine. We also give methods for enforcing the so-called first-match policy for a simplified version of the recent reversible functional language RFUN by Yokoyama et al., and simple methods to support let-calls via stack environments.

We identify concepts of reversibility for a functional language by means of a set of semantic rules with specific properties. These properties include injectivity along with local backward determinism, an important operational property for an efficient reversible language. We define a concise reversible first-order functional language in which access to the backward semantics is provided to the programmer by inverse function calls. Reversibility guarantees that in this language a backward run (inverse interpretation) is as fast as the corresponding forward run itself. By adopting a symmetric first-match policy for case expressions, we can write overlapping patterns in case branches, as is customary in ordinary functional languages, and also in leaf expressions, unlike existing inverse interpreter methods, which enables concise programs. In patterns, the use of a duplication/equality operator also simplifies inverse computation and program inversion. We discuss the advantages of a reversible functional language using example programs, including run-length encoding. Program inversion is seen to be as lightweight as for imperative reversible languages and realized by recursive descent. Finally, we show that the proposed language is r-Turing complete.

Program inversion is a fundamental concept in programtransformation. We describe the principles behind an automatic program inverter, which we developed for a first-order functional language, and show several inverse programs automatically produced by our system. The examples belong to different application areas, including encoding and decoding, printing and parsing, and bidirectional data conversion. The core of the system uses a stack-based language, local inversion, and eliminates nondeterminism by applying methods from parsing theory.

We present a method for automatic program inversion of functional programs based on methods of LR parsing. We formalize the transformation and illustrate it with the inversion of a program for run-length encoding. We solve one of the main problems of automatic program inversion—the elimination of nondeterminism—by viewing an inverse program as a context-free grammar and applying to it methods of LR parsing to turn it into a recursive, deterministic inverse program. This improves the efficiency of the inverse programs and greatly expands the application range of our earlier method for program inversion.

We present a method for automatic program inversion in a first-order functional programming language. We formalize the transformation and illustrate it with several examples including the automatic derivation of a program for run-length decoding from a program for run-length encoding. This derivation is not possible with other automatic program inversion methods. One of our key observations is that the duplication of values and testing of their equality are two sides of the same coin in program inversion. This leads us to the design of a new self-inverse primitive function that considerably simplifies the automatic inversion of programs.

We survey fundamental concepts in inverse programming and present the Universal Resolving Algorithm (URA), an algorithm for inverse computation in a first-order, functional programming language. We discuss the principles behind the algorithm, including a three-step approach based on the notion of a perfect process tree, and demonstrate our implementation with several examples. We explain the idea of a semantics modifier for inverse computation which allows us to perform inverse computation in other programming languages via interpreters.

Deforestation is a well-known program transformation technique which eliminates intermediate data structures that are passed between functions. One of its weaknesses is the inability to deforest programs using accumulating parameters.We show how intermediate lists built by a selected class of functional programs, namely 'accumulating maps', can be deforested using a single composition rule. For this we introduce a new function dmap, a symmetric extension of the familiar function map. While the associated composition rule cannot capture all deforestation problems, it can handle accumulator fusion of functions defined in terms of dmap in a surprisingly simple way. The rule for accumulator fusion presented here can also be viewed as a restricted composition scheme for attribute grammars, which in turn may help us to bridge the gap between the attribute and functional world.

We study the problem to transform functional programs, which intensively use append functions (like inefficient list reversal), into programs, which use accumulating parameters instead (like efficient list reversal). We give an (automatic) transformation algorithm for our problem and identify a class of functional programs, namely restricted 2- modular tree transducers, to which it can be applied. Moreover, since we get macro tree transducers as transformation result and since we also give the inverse transformation algorithm, we have a new characterization for the class of functions induced by macro tree transducers.

Existing partial evaluators usually fix the strategy for binding-time analysis. But a single strategy cannot fulfill all goals without leading to compromises regarding precision, termination, and code explosion in partial evaluators. Our goal is to improve the usability of partial evaluator systems by developing an adaptive approach that can accommodate a variety of different strategies ranging from maximally polyvariant to entirely uniform analysis, and thereby make offline specialization more practical in a realistic setting. The core of the analysis has been implemented in FSpec, an offline partial evaluator for a subset of Fortran 77.

We present an algorithm for inverse computation in a first-order functional language based on the notion of a perfect process tree. The Universal Resolving Algorithm (URA) introduced in this paper is sound and complete, and computes each solution, if it exists, in finite time. The algorithm has been implemented for TSG, a typed dialect of S-Graph, and shows some remarkable results for the inverse computation of functional programs such as pattern matching and the inverse interpretation of While-programs.

This paper gives an introduction to Turchin's supercompiler, a program transformer for functional programs which performs optimizations beyond partial evaluation and deforestation. More precisely, the paper presents positive supercompilation.

In recent work, we proposed a simple functional language S-graph-n to study metaprogramming aspects of self-applicable online program specialization. The primitives of the language provide support for multiple encodings of programs. An important component of online program specialization is the termination strategy. In this paper we show that such a representation has the great advantage of simplifying generalization of multiply encoded data. After developing and formalizing the basic metaprogramming concepts, we extend two basic methods to multiply encoded data: most specific generalization and the homeomorphic embedding relation. Examples and experiments with the initial design of an online specializer illustrate their use in hierarchies of online program specializers.

Program specialization can divide a computation into several computation stages. The program generator which we designed and implemented for a higher-order functional language converts programs into very compact multi-level generating extensions that guarantee fast successive specialization. Experimental results show a remarkable reduction of generation time and generator size compared to previous attempts of multiple self-application.

This paper gives a gentle introduction to Turchin's super-compilation 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.

Partial evaluation can automatically generate program transformers from interpreters. In the context of functional languages, we investigate the design space of higher-order interpreters to achieve certain transformation effects. Our work is based on the interpretive approach and exploits the language preservation property of offline partial evaluators. We have generated higher-order online partial evaluators, optimizing closure converters, and converters to first-order tail form. The latter can serve as the middle end of a compiler. The generated transformers are strictly more powerful than the partial evaluators used for their generation.

Program specialization can divide a computation into several computation stages. We present the key ingredient of our approach to multi-level specialization: an accurate and fast multi-level binding-time analysis. Three efficient program analyses for higher-order, functional languages are presented which are based on constraint systems and run almost-linear in the size of the analyzed programs. The three constraint normalizations have been proven correct (soundness, completeness, termination, existence of best solution). The analyses have all been implemented for a substantial, higher-order subset of Scheme. Experiments with widely-available example programs confirm the excellent run-time behavior of the normalization algorithms.

Our aim is to study how the interpretive approach — inserting an interpreter between a source program and a program specializer — can be used to improve the transformation of programs and to automatically generate program transformers by self-application of a program specializer.

Partial deduction and driving are two methods used for program specialization in logic and functional languages, respectively. We argue that both techniques achieve essentially the same transformational effect by unification-based information propagation. We show their equivalence by analyzing the definition and construction principles underlying partial deduction and driving, and by giving a translation from a functional language to a definite logic language preserving certain properties. We discuss residual program generation, termination issues, and related other techniques developed for program specialization in logic and functional languages.

We propose a new method for improving the specialization of programs by inserting an interpreter between a subject program and a specializer. We formulate three specializer projections which enable us to generate specializers from interpreters. The goal is to provide a new way to control the specialization of programs, and we report the first practical results. This is a step towards the automatic production of specializers. Using an existing, self-applicable partial evaluator we succeeded in generating a stand-alone specializer for a first-order functional language which is stronger than the partial evaluator used for its generation. The generated specializer corresponds to a simple supercompiler. As an example we show that the generated specializer can achieve the same speed-up effect as the Knuth, Morris and Pratt algorithm (D.E. Knuth et al., vol. 6, no. 2, 1977) by specializing a naive matcher with respect to a fixed pattern. The generated specializer is also strong enough to handle bounded static variation, a case which partial evaluators usually can not handle. >