Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism

Program specialization is a program transformation methodology which improves program efficiency by exploiting the information about the input data which are available at compile time. We show that current techniques for program specialization based on partial evaluation do not perform well on nondeterministic logic programs. We then consider a set of transformation rules which extend the ones used for partial evaluation, and we propose a strategy for guiding the application of these extended rules so to derive very efficient specialized programs. The efficiency improvements which sometimes are exponential, are due to the reduction of nondeterminism and to the fact that the computations which are performed by the initial programs in different branches of the computation trees, are performed by the specialized programs within single branches. In order to reduce nondeterminism we also make use of mode information for guiding the unfolding process. To exemplify our technique, we show that we can automatically derive very efficient matching programs and parsers for regular languages. The derivations we have performed could not have been done by previously known partial evaluation techniques.A preliminary version of this paper appears as: Reducing Nondeterminism while Specializing Logic Programs. Proceedings of the 24th Annual ACM Symposium on Principles of Programming Languages, Paris, France, January 15–17, 1997, ACM Press, 1997, pp. 414–427.     

A Short Cut to Optimal Sequences

We propose a method of developing efficient programs for finding the optimal sequence, such as the maximum valued one among those that are acceptable. We introduce a method of deriving efficient algorithms from naive enumerate-and-choose-style ones. Our method is based on shortcut fusion, which is a program transformation for eliminating intermediate data structures passed between functions, and a set of auxiliary transformations. As an implementation of our method, we introduce a library for finding optimal sequences. The library consists of proposed transformations, together with functions useful to describe desirable sequences, so that naive enumerate-and-choose-style programs will be automatically improved.     

Formal foundation of consistent EMF model transformations by algebraic graph transformation

Model transformation is one of the key activities in model-driven software development. An increasingly popular technology to define modeling languages is provided by the Eclipse Modeling Framework (EMF). Several EMF model transformation approaches have been developed, focusing on different transformation aspects. To validate model transformations with respect to functional behavior and correctness, a formal foundation is needed. In this paper, we define consistent EMF model transformations as a restricted class of typed graph transformations using node type inheritance. Containment constraints of EMF model transformations are translated to a special kind of graph transformation rules such that their application leads to consistent transformation results only. Thus, consistent EMF model transformations behave like algebraic graph transformations and the rich theory of algebraic graph transformation can be applied to these EMF model transformations to show functional behavior and correctness. Furthermore, we propose parallel graph transformation as a suitable framework for modeling EMF model transformations with multi-object structures. Rules extended by multi-object structures can specify a flexible number of recurring structures. The actual number of recurring structures is dependent on the application context of such a rule. We illustrate our approach by selected refactorings of simplified statechart models. Finally, we discuss the implementation of our concepts in a tool environment for EMF model transformations.     

Partial evaluation with inference rules

Suppose we are given a program P in some language L, and a set of inference rules based on unification that define the dynamic semantics of this language L. We propose a tactic for (partially) evaluating a given predicate in a set of inference rules, therefore proposing a new executable semantics to our rules. This tactic applied to P and to the dynamic semantics of L yields classically a new set of specialized inference rules that are a compiled version of P. Our partial evaluation tactic proposes and uses some original improvements, which are applicable to the general field of partial evaluation of unification-based languages.     

Widening techniques for regular tree model checking

We consider the framework of regular tree model checking where sets of configurations of a system are represented by regular tree languages and its dynamics is modeled by a term rewriting system (or a regular tree transducer). We focus on the computation of the reachability set R*(L) where R is a regular tree transducer and L is a regular tree language. The construction of this set is not possible in general. Therefore, we present a general acceleration technique, called regular tree widening which allows to speed up the convergence of iterative fixpoint computations in regular tree model checking. This technique can be applied uniformly to various kinds of transformations. We show the application of our framework to different analysis contexts: verification of parameterized tree networks and data-flow analysis of multithreaded programs. Parametrized networks are modeled by relabeling tree transducers, and multithreaded programs are modeled by term rewriting rules encoding transformations on control structures. We prove that our widening technique can emulate many existing algorithms for special classes of transformations and we show that it can deal with transformations beyond the scope of these algorithms.     

Unfolding-based Improvements on Fuzzy Logic Programs

Unfolding is a semantics-preserving program transformation technique that consists in the expansion of subexpressions of a program using their own definitions. In this paper we define two unfolding-based transformation rules that extend the classical definition of the unfolding rule (for pure logic programs) to a fuzzy logic setting. We use a fuzzy variant of Prolog where each program clause can be interpreted under a different (fuzzy) logic. We adapt the concept of a computation rule, a mapping that selects the subexpression of a goal involved in a computation step, and we prove the independence of the computation rule. We also define a basic transformation system and we demonstrate its strong correctness, that is, original and transformed programs compute the same fuzzy computed answers. Finally, we prove that our transformation rules always produce an improvement in the efficiency of the residual program, by reducing the length of successful Fuzzy SLD-derivations.     

Compiler Optimization Correctness by Temporal Logic

Rewrite rules with side conditions can elegantly express many classical compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transformation-enabling side conditions are specified in a temporal logic suitable for describing program data flow.The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations: dead code elimination, constant folding, and code motion. A transformation is correct if whenever it can be applied to a program, the original and transformed programs are semantically equivalent, i.e., they compute the same input-output function. The proofs of semantic equivalence inductively show that a transformation-specific bisimulation relation holds between the original and transformed program computations.     

Program Development as a Formal Activity

A methodology of program development by transformations is outlined. In particular, ways of representing the transformation rules are discussed, and the relationship between notions of their correctness and the semantic definition of programming languages is studied. How transformation techniques are complemented by the use of abstract data types and assertions is described. In the resulting calculus of transformations, the single rules not only represent design or optimization techniques, but they also incorporate verification principles. To illustrate this approach, the Warshall algorithm is developed by successive applications of transformations.     

Program Development Schemata as Derived Rules

We show how the formalization and application of schemata for program development can be reduced to the formalization and application of derived rules of inference. We formalize and derive schemata as rules in theories that axiomatize program data and programs themselves. We reduce schema-based program development to ordinary theorem proving, where higher-order unification is used to apply rules. Conceptually, our formalization is simple and unifies divergent views of schemata, program synthesis, and program transformation. Practically, our formalization yields a simple methodology for carrying out development using existing logical frameworks; we illustrate this in the domain of logic program synthesis and transformation using the Isabelle logical framework.     

Unfolding rules for GHC programs

This paper presents a set of rules for the transformation of GHC (Guarded Horn Clauses) programs based on unfolding. The proposed set of rules, called UR-set, is shown to preserve freedom from deadlock and to preserve the set of solutions to be derived. UR-set is expected to give a basis for various program transformations, especially partial evaluation of GHC programs.     

Linear programs in a simple reversible language

Very simple reversible programming languages can be useful for the study of reversible transformations. For this purpose we define simple reversible language (SRL), a very simple reversible language, and analyse its properties. The language SRL is similar to the “loop” languages that have been used by several authors to characterise the set of primitive recursive functions. There are, however, important differences: SRL has domain instead of and only reversible programs can be written in SRL. The reversibility of linear homogeneous SRL programs is related to the fact that the corresponding set of matrices has the algebraic structure of a group. We show that such programs implement exactly the linear transformations corresponding to the group of integer positive modular matrices, while in ESRL, an extended version of SRL, the set of transformations that can be implemented by linear homogeneous programs corresponds exactly to the group of integer modular matrices.     

Scheduling model‐to‐model transformations with continuations

Model transformations are at the heart of model‐driven engineering because they allow the automation of diverse kinds of model manipulations. Transformation scheduling is a key issue in the design and implementation of many transformation languages. This paper reports our results using continuations as the underlying technique for building a scheduling mechanism implicitly driven by data dependence among transformation rules. To support our experiments, we have built a proof‐of‐concept model transformation language, which is also reported here. First, we motivate the problem by analyzing the scheduling mechanism of current model transformation languages. Then, we introduce the notion of continuation, showing its applicability to model transformations. Afterwards, we present our approach, notably explaining how dependence is specified and giving the scheduling algorithm. We also analyze the lazy resolution of rules and how to deal with collection operations. The approach is validated by an implementation that targets the Java Virtual Machine and by running of the performance benchmarks that show its efficiency and scalability. Besides, we discuss how it can be applied to other existing transformation languages and present several applicability scenarios. Copyright © 2013 John Wiley & Sons, Ltd.     

Basic Results in Automatic Transformations of Shared Memory Parallel Programs into Sequential Programs

We study the problem of developing a set of syntax-driven transformations for automatic translation of shared memory parallel programs into sequential programs. The result is a sequential program that is semantically equivalent to the original program. Consequently, the problem of debugging parallel programs is reduced to the problem of debugging sequential programs. Moreover, the efficiency of parallel programs can be increased by sequentializing code segments that include extra parallelism.The main difficulty in developing such a system is to preserve the fairness property of any actual parallel execution, which states that no process can wait forever unserved. Thus, non termination of the sequential version (namely an infinite loop) is allowed only if there is at least one fair parallel execution that does not halt as well (i.e., a process that executes an infinite loop whose termination is not dependent on any other process).We show that it is sufficient to consider the case of two sequential programs executed in parallel in order to solve the general case. We then describe several types of transformations and check their ability to preserve fairness. The results, with regards to the existence of such a transformation for general parallel programs are not conclusive; however, we do show that restricted cases (which are likely to appear in the reality) can be sequentialized using this set of transformations.     

The List Introduction Strategy for the Derivation of Logic Programs

We present a new program transformation strategy based on the introduction of lists. This strategy is an extension of the tupling strategy which is based on the introduction of tuples of fixed length. The list introduction strategy overcomes some of the limitations of the tupling strategy and, in particular, it makes it possible to transform general recursive programs into linear recursive ones also in cases when this transformation cannot be performed by the tupling strategy. The linear recursive programs we derive by applying the list introduction strategy have in most cases very good time and space performance because they avoid repeated evaluations of goals and unnecessary constructions of data structures. Received December 2000 / Accepted in revised form January 2002     

Domain-Specific Optimisation with User-Defined Rules in CodeBoost

The use of domain-specific optimisations can significantly enhance the performance of high-level programs. However, current programming languages have poor support for specifying such optimisations. In this paper, we introduce user-defined rules in CodeBoost. CodeBoost is a tool for source-to-source transformation of C++ programs. With CodeBoost, domain-specific optimisations can be specified as rewrite rules in C++-like syntax, within the C++ program, together with the classes where they apply. We also illustrate the effectiveness of user-defined rules and domain-specific optimisation on a real-world example application.     

Bytecode Rewriting in Tom

In this paper, we present a term rewriting based library for manipulating Java bytecode. We define a mapping from bytecode programs to algebraic terms, and we use Tom, an extension of Java that adds pattern-matching facilities, to describe transformations. An originality of Tom is that it provides a powerful strategy language to express traversals over trees and to control how transformation rules are applied. To be even more expressive, we use CTL formulae as conditions and we show how their satisfiability can be ensured using the strategy formalism. Through small examples, we show how bytecode analysis and transformations can be defined in an elegant way. In particular, we outline the implementation of a ClassLoader parameterized by a security policy that restricts file access.     

Program transformation through meta-shifting

A program transformation strategy called meta-shifting is developed for control optimization of programs written in languages with control freedom. The strategy involves writing a specialized evaluator for each program (segment) with specific control. It is applied to an equational language to derive a general method to transform one program into another, which simulates (approximately) normal order evaluation of the original program, under interpreters with arbitrary evaluation order.