Logic Program Synthesis and Transformation

The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. In this paper we study a refinement calculus for deriving logic programs. Dealing with logic programs rather than imperative programs has the dual advantages that, due to the expressive power of logic programs, the final program is closer to the original specification, and each refinement step can achieve more. Together these reduce the overall number of derivation steps.

We present a logic programming language extended with specification constructs (including general predicates, assertions, and types and invariants) to form a wide-spectrum language. General predicates allow non-executable properties to be included in specifications. Assertions, types and invariants make assumptions about the intended inputs of a procedure explicit, and can be used during refinement to optimize the constructed logic program. We provide a semantics for the extended logic programming language and derive a set of refinement laws. Finally we apply these to an example derivation.

The paper presents an analyzer for verifying the correctness of a Prolog program relative to a specification which provides a list of input/output annotations for the arguments and parameters that can be used to establish program termination. The work stems from Deville's methodology to derive Prolog programs that correctly implement their declarative meaning. In this context, we propose an algorithm that combines, adapts, and sometimes improves various existing static analyses in order to verify total correctness of Prolog programs with respect to formal specifications. Using the information computed during the verification process, an automatic complexity analysis can be also performed.

Standard partial deduction suffers from several drawbacks when compared to top-down abstract interpretation schemes. Conjunctive partial deduction, an extension of standard partial deduction, remedies one of those, namely the lack of side-ways information passing. But two other problems remain: the lack of success-propagation as well as the lack of inference of global success-information. We illustrate these drawbacks and show how they can be remedied by combining conjunctive partial deduction with an abstract interpretation technique known as more specific program construction. We present a simple, as well as a more refined integration of these methods. Finally we illustrate the practical relevance of this approach for some advanced applications, where it surpasses the precision of current abstract interpretation techniques.

Recently, partial deduction of logic programs has been extended to conceptually embed folding. To this end, partial deductions are no longer computed of single atoms, but rather of entire conjunctions; Hence the term “conjunctive partial deduction”.

Conjunctive partial deduction aims at achieving unfold/fold-like program transformations such as tupling and deforestation within fully automated partial deduction. However, its merits greatly surpass that limited context: Also other major efficiency gains can be obtained through considerably improved side-ways information propagation.

In this paper, we present a first investigation of conjunctive partial deduction in practice. We describe the concrete options used in the implementation(s), look at abstraction in a practical Prolog context, include and discuss an extensive set of benchmark results. ¿ From these, we can conclude that conjunctive partial deduction can indeed pay off in practice, beating its conventional precursor on a number of small to medium size programs. However, controlling it in a perfect way proves far from obvious, and a range of challenging open problems remain as topics for further research.

This paper describes an interactive tool for transforming pure Prolog programs. The choice of (pure) Prolog semantics induces a number of conditions that have to be satisfied before a particular transformation step can be applied. The transformation tool has been developed using a programming environment based on algebraic specification. The paper describes the tool and reports on the design decisions, the implemented transformation steps, and the user interface.

We show that sometimes partial deduction produces poor program specializations because of its limited ability in (i) dealing with conjunctions of recursively defined predicates, (ii) combining partial evaluations of alternative computations, and (iii) taking into account unification failures. We propose to extend the standard partial deduction technique by using versions of the definition rule and the folding rule which allow us to specialize predicates defined by disjunctions of conjunctions of goals. We also consider a case split rule to take into account unification failures. Moreover, in order to perform program specialization via partial deduction in an automatic way, we propose a transformation strategy which takes as parameters suitable substrategies for directing the application of every transformation rule.

Finally, we show through two examples that our partial deduction technique is superior to standard partial deduction. The first example refers to the automatic derivation of the Knuth-Morris-Pratt string matching algorithm, and the second example refers to the construction of a parser for a given regular expression. In both examples, the specialized programs are derived starting from naive, non-deterministic initial programs, whereas standard partial deduction can derive similar specialized programs only when complex, deterministic initial programs are provided.

Program specialization optimizes programs for known values of the input. It is often the case that the set of possible input values is unknown, or this set is infinite. However, a form of specialization can still be performed in such cases by means of abstract interpretation, specialization then being with respect to abstract values (substitutions), rather than concrete ones. This paper reports on the application of abstract multiple specialization to automatic program parallelization in the &-Prolog compiler. Abstract executability, the main concept underlying abstract specialization, is formalized, the design of the specialization system presented, and a non-trivial example of specialization in automatic parallelization is given.

We present in this paper a new method for computing the reachability set associated with a Petri net. The method proceeds, first, by coding the reachability problem into a predicate defined by a logic program with arithmetic constraints, then by transforming the encoding program. Each transition of the Petri net is encoded as a clause. The guards appearing in the clauses correspond to the enabling conditions of the corresponding transitions. In order to characterize arithmetically the least model of the transformed program, we define a system of two reduction rules which apply iteratively to the program. When the process of reduction terminates with success, it generates a formula of Presburger arithmetic, which contains the components of the initial marking as parameters. In the particular case of a BPP-net (i.e., a Petri net where every transition has exactly one input place), the process is guaranteed to succeed, thus providing us with an exact and generic characterization of the reachability set. We show finally how unfolding of propositional logic programs can be viewed as transformation of BPP-nets.

Argument size relationships are useful in termination analysis which, in turn, is important in program synthesis and goal-replacement transformations. We show how a precise analysis for inter-argument size relationships, formulated in terms of abstract interpretation, can be implemented straightforwardly in a language with constraint support like CLP(\(\mathcal{R}\)) or SICStus version 3. The analysis is based on polyhedral approximations and uses a simple relaxation technique to calculate least upper bounds and a delay method to improve the precision of widening. To the best of our knowledge, and despite its simplicity, the analysis derives relationships to an accuracy that is either comparable or better than any existing technique.

As typed logic programming becomes more mainstream, system building tools like partial deduction systems will need to be mapped from untyped languages to typed ones. It is important, however, when mapping techniques across that the new techniques should exploit the type system as much as possible. In this paper, we show how norms, which play a crucial role in termination analysis, can be generated from the prescribed types of a logic program. Interestingly, the types highlight restrictions of earlier norms and suggest how these norms can be extended to obtain some very general and powerful notions of norm which can be used to measure any term in an almost arbitrary way. We see our work on norm derivation as a contribution to the termination analysis of typed logic programs which, in particular, forms an essential part of offline partial deduction systems.

The notion of partial deduction known from logic programming is defined in the framework of Structural Synthesis of Programs (SSP). Partial deduction for unconditional computability statements in SSP is defined. Completeness and correctness of partial deduction in the framework of SSP are proven. Several tactics and stopping criteria are suggested.

Schema-based transformational systems maintain a library of logic program schemata which capture large classes of logic programs. One of the shortcomings of schema-based transformation approaches is their reliance on a large (possibly incomplete) set of logic program schemata that is required in order to capture all of the minor syntactic differences between semantically similar logic programs. By defining a set of extensible logic program schemata and an associated set of logic program transformations, it is possible to reduce the size of the schema library while maintaining the robustness of the transformational system. In our transformational system, we have defined a set of extensible logic program schemata in λProlog. Because λProlog is a higher-order logic programming language, it can be used as the representation language for both the logic programs and the extensible logic program schemata. In addition to the instantiation of predicate variables, extensible logic program schemata can be extended by applying standard programming techniques (e.g., accumulating results), introducing additional arguments (e.g., a second list to append to the end of the primary list), combining logic program schemata which share a common primary input, and connecting logic program schemata which are connected via a result of one schema being an input to the other schema. These extensions increase the robustness of logic program schemata and enhance traditional schema-based transformational systems.

Meta-level compositions of object logic programs are naturally implemented by means of meta-programming techniques. Metainterpreters defining program compositions however suffer from a computational overhead that is due partly to the interpretation layer present in all meta-programs, and partly to the specific interpretation layer needed to deal with program compositions. We show that meta-interpreters implementing compositions of object programs can be fruitfully specialised w.r.t. meta-level queries of the form Demo(E,G), where E denotes a program expression and G denotes a (partially instantiated) object level query. More precisely, we describe the design and implementation of a declarative program specialiser that suitably transforms such metainterpreters so as to sensibly reduce — if not to completely remove — the overhead due to the handling of program compositions. In many cases the specialiser succeeds in eliminating also the overhead due to meta-interpretation.

There is no universal agreement on exactly what form a specification should take, what part it should play in synthesis, and what its precise relationship with the specified program should be. In logic programming, the role of specification is all the more unclear since logic programs are often used as executable specifications. In this paper we take the view that specifications should be set in the context of the problem domain, which we call a framework. We conduct a preliminary study of two useful forms of logic specifications: if-and-only-if and partial specifications. First we set up a three-tier formalism for synthesis, the top-tier being a framework. Then within this formalism we define these two forms of specifications, and discuss their roles in synthesis.

We apply logic program development technology to define abstract proof procedures, in the form of logic programs, for computing the admissibility semantics for default reasoning proposed in [2].

The proof procedures are derived from a formal specification. The derivation guarantees the soundness of the proof procedures. The completeness of the proof procedures is shown by employing a technique of symbolic execution of logic programs to compute (an instance of) a relation implied by the specification.