Sistemi formali

per la specifica, l'analisi, la verifica, la sintesi e

la trasformazione di sistemi software.

Università degli studi di Roma Tor Vergata

Dipartimento di Informatica, Sistemi e Produzione

Risultati - Results

The results of our research activity have been described in the following papers. Below we illustrate the main contributions of each paper.

[20]
Pettorossi, A. and Proietti, M. Transformation of Logic Programs Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 5. 1998. D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors. pages 697-787

Abstract. Program transformation is a methodology for deriving correct and efficient programs from specifications. In this chapter, we will look at the so called `rules + strategies' approach, and we will report on the main techniques which have been introduced in the literature for that approach, in the case of logic programs. We will also present some examples of program transformation, and we hope that through those examples the reader may acquire some familiarity with the techniques we will describe.

In this paper the authors give an overview of the techniques for the transformation of logic programs following the `rules + strategies' approach. It is an updated account which refers to recent results in the area.
    The attention is first focused on definite logic programs. The following transformation rules are considered: (i) definition introduction (of possibly recursive predicates), (ii) definition elimination, (iii) unfolding, (iv) folding, (v) goal replacement (within a given clause), (vi) clause replacement (which is used for clause rearrangement, deletion of subsumed clauses, deletion of clauses with finitely failed body, and generalization + equality introduction). Various semantics functions are considered, such as the least Herbrand model semantics, the computed answers substitutions semantics, the finite failure semantics, and the pure Prolog semantics. For each of these semantics and for given sets of transformation rules the authors state correctness theorems for sequences of programs generated by applying these rules. The correctness theorems are of the following form: given a set R of rules, if a sequence of programs is constructed by using R then the semantics of the initial program of the sequence is equal to the semantics of the final program of the sequence. There are also versions of the correctness theorems which allow for the use of the folding rule with respect to predicate definitions which occur in previous programs in the sequence, not in the program at hand.
    The authors also present a method, called the unfold/fold proof method, for proving equivalencies of the form: for all X (there exists Y such that G1(X,Y) iff there exists Z such that G2(X,Z)), where G1 and G2 are goals (that is, conjunctions of atoms). This method is very useful for the application of the goal replacement rule which indeed requires the proofs of such equivalencies. The unfold/fold proof method makes use of transformation techniques, and thus, it allows us to perform both proofs of programs and derivations of programs within the same transformational framework using the same transformation system.
    Then the authors consider the class of normal programs with the computed answer substitution semantics and the Clark's completion semantics. Also for this class of programs and for these semantics, various correctness theorems are stated.
    In the second part of the paper the authors present the strategies for directing the application of the transformation rules so that efficient programs may be derived from initial program versions (or initial specifications). The following basic strategies are considered: (i) the tupling strategy, (ii) the loop absorption strategy, (iii) the generalization strategy. It is shown that some useful techniques for program transformation, which have been published in the literature, such as compiling control, program composition, and changing of data representations, can all be considered as suitable sequences of applications of the basic strategies.
    Then the paper gives a brief overview of other techniques for program transformation, such as the schema based technique, the recursion removal technique, the annotation technique, and the memoing technique. The final part of the paper is devoted to the analysis of the relationship between program transformation, partial evaluation and program specialization. In particular, the Lloyd-Shepherdson's approach to partial evaluation of logic programs is compared to the one based on unfold/fold rules and their close correspondence is illustrated through an example on string matching.

[21]
Pettorossi, A. and Proietti, M. Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs Journal of Logic Programming, Vol. 41, No. 2&3 (Nov. 1999), pp.197-230.

Abstract. We present a method for proving properties of definite logic programs. This method is called unfold/fold proof method because it is based on the unfold/fold transformation rules. Given a program P and two goals (that is, conjunctions of atoms) F(X,Y) and G(X,Z), where X, Y, and Z are pairwise disjoint vectors of variables, the unfold/fold proof method can be used to show that the equivalence formula \forall X. (\exists Y. F(X,Y) <=> \exists Z. G(X,Z)) holds in the least Herbrand model of P. Equivalence formulas of that form can be used to justify goal replacement steps, which allow us to transform logic programs by replacing old goals, such as F(X,Y), by equivalent new goals, such as G(X,Z). These goal replacements preserve the least Herbrand model semantics if we find non-ascending unfold/fold proofs of the corresponding equivalence formulas, that is, unfold/fold proofs which ensure suitable well-founded orderings between the successful SLD-derivations of F(X,Y) and G(X,Z), respectively. We also present a method for program synthesis from implicit definitions. It can be used to derive a definite logic program for the predicate newp implicitly defined by an equivalence formula of the form \forall X. (\exists Y. F(X,Y) <=> \exists Z. (H(X,Z), newp(X,Z))), such that the predicates occurring in the goals F(X,Y) and H(X,Z) are defined in a given program P, and newp is a predicate symbol not occurring in P. The set of clauses defining newp, say Eureka, allows us to prove that the above equivalence formula holds in the least Herbrand model of P \cup Eureka using an unfold/fold proof. Thus, the correctness of our synthesis method derives from the one of the unfold/fold proof method. We finally illustrate our synthesis method through some examples of program specialization, program synthesis, and program transformation, which can all be viewed as program syntheses from implicit definitions.

The paper is divided into two parts: the first part concerns a proof method, called the unfold/fold proof method, for proving properties of goals, that is, conjunctions of atoms, within the contest of a given Horn clause program, and the second part concerns the use of this proof method for the synthesis of logic programs from specifications.
In the first part of the paper it is shown that, in particular, the unfold/fold proof method can be used for proving that given a logic program P, and two goals G1 and G2, an equivalence of the form: (*) forall X (there exists Y such that G1(X,Y) iff there exists Z such that G2(X,Z)), holds in the least Herbrand model of P. The proof consists in deriving by transformation from the program P and the clause C1: new1(X) <- G1(X,Y) a set, say S, of clauses which can also be derived by transformation from the program P and the clause C2: new2(X) <- G2(X,Z), after the replacement of new2 by new1. During both the derivation of S from P U {C1} and the derivation of S from P U {C2}, the following transformation rules can be applied: (i) unfolding, (ii) folding, (iii) goal replacement, (iv) generalization + equality introduction, and (v) simplification of equalities. Once an equivalence, such as (*), between the goals G1 and G2 has been proved, it can be used for applying the goal replacement rule in transforming programs starting from the program P. In order for the replacement of the goal G1 by the goal G2 to preserve total correctness (that is, the program before the replacement and the program after the replacement have the same least Herbrand model) it is required that the unfold/fold proof of the equivalence (*) be `non-ascending', that is, for each clause, say M, in S derived from P U {C1} by a sequence s1 of transformation rules, it is the case that M with new1 renamed by new2, can also be derived from P U {C2} using a sequence s2 of transformation rules which has a number of unfolding steps which is not larger than that of s1.
In the second part of the paper the unfold/fold proof method is used for synthesizing the set of clauses, say Eureka, such that given a program P and an implicit specification of a new predicate newp of the form: (**) forall X (there exists Y such that spec(X,Y) iff there exists Z such that (context(X,Z) and newp(X,Z))), we have that (**) holds in the least Herbrand model of P U Eureka. In the specification (**) it is assumed that the predicates occurring in the formulas spec and context they are all defined in P. This synthesis method is applied to the problem of automatically synthesizing programs which manipulate difference-lists from equivalent ones which manipulate lists, and also to the problem of avoiding redundant non-determinism present in left-recursive programs.

3. [620]

Transforming Inductive Definitions

Maurizio Proietti and Alberto Pettorossi

D. De Schreye (ed.) Proceedings of the 16th International Conference on Logic Programming (ICLP'99), Las Cruces, New Mexico, USA,
Nov. 29 - Dec. 4, 1999, MIT Press, pp. 486-499.

      Abstract.
     The main goal of this paper is to provide a common foundation to the theories of correctness of program transformations for a large
     variety of programming languages. We consider the notion of rule set and the notion of inductive set which is defined by a rule set. We
     also consider a class of transformations of rule sets, called rule replacements, which replace an old rule set by a new rule set. These
     replacements can be viewed as generalizations of the most commonly used transformations, such as folding and unfolding. We study
     two methods for proving the correctness of rule replacements, that is, for showing that the old rule set and the new rule set define the
     same inductive set. These methods are: (i) the Unique Fixpoint Method, based on the well-foundedness property of the new rule set,
     and (ii) the Improvement Method, based on the fact that the premises of the old rule set are replaced by premises which have `smaller'
     proofs w.r.t. a suitable well-founded relation. Our Unique Fixpoint and Improvement Methods generalize many methods described in
     the literature which deal with transformation rules for functional and logic programming languages. Our methods have also the
     advantages of: (i) being parametric w.r.t. the well-founded relation which is actually used, and (ii) being applicable to rules with finite
     or infinite sets of premises.

4. [621]

Rules and Strategies for Contextual Specialization of Constraint Logic Programs

Fioravanti Fabio, Alberto Pettorossi, Maurizio Proietti

M. Leuschel (ed.) Proceedings of the ICLP'99 Workshop on Optimization and Implementation of Declarative Programming Languages
(WOID'99), Las Cruces, New Mexico, USA, Dec.2-3, 1999, pp. 1-9.

     Abstract.
     We address the problem of specializing a constraint logic program w.r.t. a constrained atom which specifies the context of use of the
     program. We follow an approach based on transformation rules and strategies. We introduce a novel transformation rule, called
     contextual constraint replacement, to be combined with variants of the traditional unfolding and folding rules. We present a general
     Partial Evaluation Strategy for automating the application of these rules, and two additional strategies: the Context Propagation
     Strategy which is instrumental for the application of our contextual constraint replacement rule, and the Invariant Promotion Strategy
     for taking advantage of invariance properties of the computation. We show through some examples the power of our method and we
     compare it with existing methods for partial deduction ofconstraint logic programs based on extensions of Lloyd and Shepherdson's
     approach.

5. [619]

Transformation Rules for Logic Programs with Goals as Arguments

Alberto Pettorossi and Maurizio Proietti

Pre-Proceedings 9th LOPSTR '99 Report University of Venice (Italy) CS-99-16, pages 171-178

     Abstract.
     We introduce a logic language where predicate symbols may have both terms and goals as arguments. We define its operational
     semantics by extending SLD-resolution with the left-to-right selection rule, and we propose a set of transformation rules for
     manipulating programs written in that language. These transformation rules are shown to be correct in the sense that they preserve the
     chosen operational semantics. This logic language has higher order capabilities which turn out to be very powerful for the derivation of
     efficient logic programs. In particular, in our language we can avoid the problem of goal rearrangement which is often encountered
     during program transformation. Moreover, goals as arguments allow us to perform on logic programs transformation steps similar to
     the ones performed on functional programs when using higher order generalizations and continuation arguments.

For problems and suggestions: adp@iasi.rm.cnr.it

Save this page at: home2/users/adp/public.html/MURST40-Levi-98/40Levi_RisultatiRoma2.html