Unita' dell'Aquila e di Pisa: Risultati sulla trasformazione e la sintesi.
Back to top of page: Results on Transformation and Synthesis.Attivita' dei due anni.
Nel lavoro [64] stato proposto un sistema per la trasformazione di programmi ccp. Alle classiche operazioni di fold/unfold, opportunamente adattate al contesto ccp, sono state aggiunte operazioni specifiche per questo paradigma. E' stata dimostrata la correttezza (totale) del sistema ottenuto e ne e' stata mostrata un'applicazione alla prova di assenza di deadlock.
Nel position paper [65] sono stati analizzati i motivi che rendono attrattiva la valutazione parziale di programmi concorrenti con vincoli (ccp). In particolare, sono state individuate le possibili ottimizzazioni che una tale valutazione parziale permetterebbe di ottenere in termini di eliminazione di canali di comunicazione e di riduzione del non determinismo.
RIFERIMENTI
[64] Etalle S., M. Gabbrielli, and M.C. Meo: Transformation of CCP programs, Proc. of CONCUR'98, LNCS 1466. Springer-Verlag, 1998.
Abstract. We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations which guarantee that the input/output ccp semantics is preserved also when distinguishing deadlocked computations from successful ones. The systems allows to optimize CCP programs while preserving their intended meaning. Furthermore, since it preserves the deadlock behaviour of programs, it can be used for proving deadlock freeness of a class of queries in a given program.
--
[65] Etalle S., M. Gabbrielli: Partial Evaluation of Concurrent Constraint Languages, ACM Computing Surveys, 1998.Abstract. Partial Evaluation (PE) is by now a well-established methodology for the optimization of programs; its viability is confirmed by a large bibliography and a number of implemented systems.
Even though, while there exists a a wide literature on PE of sequential languages, ranging from theoretical studies to implemented tools, there are only few and relatively recent attempts to apply PE to concurrent languages. This situation can be ascribed to the non-determinism and the synchronization mechanisms present in concurrent languages, which substantially complicate their semantics. Nevertheless, PE can be more useful for concurrent languages than it already is for sequential ones. Indeed, in addition to the usual benefits, PE can also yield to the elimination of communication channels and of synchronization points, and to the transformation of non-deterministic computations into deterministic ones. We think that PE can be exploited with maximal benefit in the setting of concurrent constraint (CC) languages and in this position paper we will substantiate our claim.==================================================
Back to top of page: Results on Transformation and Synthesis.Primo anno di attivita'.
In [20] 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.
The paper [21] 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 new1 by new2. 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.Unita' di Roma Tor Vergata: Secondo anno di attivita'.
Per quanto riguarda la trasformazione dei programmi si sono sviluppate due metodologie per la dimostrazione della correttezza totale delle regole di fold, unfold e goal replacement. Tali metodologie sono parametriche rispetto alla semantica che viene preservata durante la trasformazione stessa [620] e pertanto,
possono essere usate per provare la correttezza di regole di trasformazione sia nell'ambito di programmi logici che in quello di programmi funzionali o concorrenti o a vincoli. Occorre solamente che la semantica del linguaggio in esame possa essere espressa con regole di inferenza. Una prima metodologia e' quella dell'Unico Punto Fisso, basata su una proprieta' di ben-fondatezza del calcolo della semantica del programma derivato. Una seconda metodologia e' quella del Miglioramento per cui nel programma di partenza il calcolo della semantica della porzione vecchia del programma da sostituire non e' piu' corto (in una opportuna misura) del calcolo della semantica della porzione nuova di programma che sostituisce la vecchia. Questa seconda metodologia puo' essere applicata anche nel caso in cui le regole per il calcolo della semantica hanno un numero infinito di premesse.Sempre nell'ambito della trasformazione dei programmi si sono sviluppate regole del tipo fold/unfold per il caso di programmi logici 'di ordine elevato', nel senso che consentano di avere goals come argomenti di simboli di predicato [619]. La necessita' di avere regole di trasformazione di programmi logici di ordine elevato deriva dal fatto che spesso occorre evitare di cambiare la posizione relativa delle formule atomiche in un goal composito, giacche' tale cambiamento puo' modificare la semantica operazionale che usi la regola di selezione left-to-right che e' la regola usata dal compilatore Prolog. Accade anche che gli argomenti di tipo goal spesso
denotano una continuazione. Pertanto le regole che vengono proposte in [619] permettono di eseguire in ambiente logico trasformazioni analoghe a quelle che vengono fatte in ambiente funzionale e che fanno uso appunto di argomenti di ordine elevato denotanti continuazioni.Per quanto riguarda la specializzazione dei programmi in [621] si e' studiato il problema della specializzazione di programmi logici con vincoli. Si sono proposte regole e strategie di trasformazione che permettono di derivare programmi con vincoli particolarmente efficienti giacche' permettono di sfruttare proprieta' invarianti che valgono durante la computazione dei programmi. In particolare si e' introdotta la regola di Contextual Constraint Replacement e una opportuna variante della regola di folding. Si sono anche introdotte la Context Propagation Strategy e la Invariant Promotion Strategy.
Nell'area della sintesi dei programmi logici abbiamo completato il lavoro dello scorso anno pubblicando i risultati su rivista [21].
Strumentazione Realizzata:
Sviluppo del Prototipo preliminare di un trasformatore di programmi logici con la realizzazione di un'interfaccia grafica per l'applicazione di regole e strategie.
Ottenibile da: http://www.iasi.cnr.it/~proietti/system.html
RIFERIMENTI
[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.
--
[21] Pettorossi, A. and Proietti, M. Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs Journal of Logic Programming (to appear)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(\overline{X},\overline{Y})$ and $G(\overline{X},\overline{Z})$, where $\overline{X}$, $\overline{Y}$, and $\overline{Z}$ are pairwise disjoint vectors of variables, the {\rm unfold/fold proof method} can be used to show that the equivalence formula $\forall \overline{X}\, (\exists \overline{Y}\, F(\overline{X},\overline{Y}) \leftrightarrow \exists \overline{Z}\, G(\overline{X},\overline{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(\overline{X},\overline{Y})$, by equivalent new goals, such as $G(\overline{X},\overline{Z})$. These goal replacements preserve the least Herbrand model semantics if we find {\it 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(\overline{X},\overline{Y})$ and $G(\overline{X},\overline{Z})$, respectively. We also present a method for {\it program synthesis from implicit definitions}. It can be used to derive a definite logic program for the predicate {\it newp} implicitly defined by an equivalence formula of the form $\forall\, \overline{X} (\exists \overline{Y}\, F(\overline{X},\overline{Y}) \leftrightarrow \exists \overline{Z}\, (H(\overline{X},\overline{Z}), {\it newp}(\overline{X},\overline{Z})))$, such that the predicates occurring in the goals $F(\overline{X},\overline{Y})$ and $H(\overline{X},\overline{Z})$ are defined in a given program $P$, and ${\it newp}$ is a predicate symbol not occurring in $P$. The set of clauses defining {\it newp}, say {\it Eureka}, allows us to prove that the above equivalence formula holds in the least Herbrand model of $P \cup {\it 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.
--
[620] Maurizio Proietti and Alberto Pettorossi , Transforming Inductive Definitions , 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.--
[621] Fioravanti Fabio, Alberto Pettorossi, Maurizio Proietti , Rules and Strategies for Contextual Specialization of Constraint Logic Programs, 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.--
[619] Alberto Pettorossi and Maurizio Proietti , Transformation Rules for Logic Programs with Goals as Arguments, Pre-Proceedings 9th LOPSTR '99 Report University of Venice (Italy) CS-99-16, pages 171-178Abstract.
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.
==================================================
Back to top of page: Results on Transformation and Synthesis.Attivita' dei due anni.
The following results have been achieved in Udine (in collaboration with researchers from the University of Valencia) in the area of the Transformation of Functional Logic Programs.
a) Specialization of Functional Logic Programs:
Languages that integrate functional and logic programming with a complete operational semantics are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction principle of functional languages and the resolution principle of logic languages. In [54], we present a partial evaluation scheme (NPE) for functional logic languages based on an automatic unfolding algorithm which builds narrowing trees. The method is formalized within the theoretical framework established by Lloyd and Shepherdson for the partial deduction of logic programs, which we have generalized for dealing with functional computations. A generic specialization algorithm is proposed which does not depend on the eager or lazy nature of the narrower being used. To the best of our knowledge, this is the first generic algorithm for the specialization of functional logic programs. We study the semantic properties of the transformation and the conditions under which the technique terminates, is sound and complete, and is also generally applicable to a wide class of programs. We also discuss the relation to work on partial evaluation in functional programming, term rewriting systems, and logic programming. Finally, we present some experimental results with an implementation of the algorithm (INDY system) which show in practice that the narrowing-driven partial evaluator effectively combines the propagation of partial data structures (by means of logical variables and unification) with better opportunities for optimization (thanks to the functional dimension).
The NPE method is as powerful as partial deduction of logic programs and positive supercompilation of functional programs. However, although it is possible to treat complex terms containing primitive functions(e.g. conjunctions or equations) in the NPE framework, its basic control mechanisms do not allow for effective polygenetic specialization of these complex expressions. Thus, in [57] we introduce a sophisticated unfolding rule endowed with a dynamic narrowing strategy which permits flexible scheduling of the elements (in conjunctions) which are reduced during specialization. We also present a novel abstraction operator which carefully considers primitive functions and is the key to achieving accurate polygenetic specialization. The abstraction operator extends some recent partitioning techniques defined in the framework of conjunctive partial deduction. We provide experimental results obtained from an implementation which extends the INDY system which demonstrate that the control refinements produce better specializations.
b) Folding and Unfolding of Functional Logic programs
In [55], we study the semantic properties of a general transformation technique called unfolding in the context of functional logic languages. Unfolding a program is defined as the application of narrowing steps to the calls in the program rules in some appropriate form. We show that, unlike the case of pure logic or pure functional programs, where unfolding is correct w.r.t. practically all available semantics, unrestricted unfolding using narrowing does not preserve program meaning, even when we consider the weakest notion of semantics the program can be given. We single out the conditions which guarantee that an equivalent program w.r.t. the semantics of computed answers is produced. Then, we study the combination of this technique with a folding transformation rule in the case of innermost conditional narrowing, and prove that the resulting transformation still preserves the computed answer semantics of the initial program, under the usual conditions for the completeness of innermost conditional narrowing. We also discuss a relationship between unfold/fold transformations and partial evaluation of functional logic programs.
RIFERIMENTI
[54] Alpuente Maria, Moreno Falaschi, German Vidal. Partial Evaluation of Functional Logic Programs, ACM Transactions on Programming Languages and Systems, 20(4):768-844 (1998)
Abstract. Languages that integrate functional and logic programming with a complete operational semantics are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction principle of functional languages and the resolution principle of logic languages. In this article, we present a partial evaluation scheme for functional logic languages based on an automatic unfolding algorithm which builds narrowing trees. The method is formalized within the theoretical framework established by Lloyd and Shepherdson for the partial deduction of logic programs, which we have generalized for dealing with functional computations. A generic specialization algorithm is proposed which does not depend on the eager or lazy nature of the narrower being used. To the best of our knowledge, this is the first generic algorithm for the specialization of functional logic programs. We study the semantic properties of the transformation and the conditions under which the technique terminates, is sound and complete, and is generally applicable to a wide class of programs. We also discuss the relation to work on partial evaluation in functional programming, term-rewriting systems, and logic programming. Finally, we present some experimental results with an implementation of the algorithm which show in practice that the narrowing-driven partial evaluator effectively combines the propagation of partial data structures (by means of logical variables and unification) with better opportunities for optimization (thanks to the functional dimension).
--
[55] Alpuente M., M. Falaschi, G. Moreno, G. Vidal: Safe Folding/Unfolding with Conditional Narrowing, Proc. of ALP'97, LNCS 1298, pages 1-15, (1997)Abstract. Functional logic languages with a complete operational semantics are based on narrowing, a generalization of term rewriting where unification replaces matching. In this paper, we study the semantic properties of a general transformation technique called unfolding in the context of functional logic languages. Unfolding a program is defined as the application of narrowing steps to the calls in the program rules in some appropriate form. We show that, unlike the case of pure logic or pure functional programs, where unfolding is correct w.r.t. practically all available semantics, unrestricted unfolding using narrowing does not preserve program meaning, even when we consider the weakest notion of semantics the program can be given. We single out the conditions which guarantee that an equivalent program w.r.t. the semantics of computed answers is produced. Then, we study the combination of this technique with a folding transformation rule in the case of innermost conditional narrowing, and prove that the resulting transformation still preserves the computed answer semantics of the initial program, under the usual conditions for the completeness of innermost conditional narrowing. We also discuss a relationship between unfold/fold transformations and partial evaluation of functional logic programs.
--
[57] Albert E., M. Alpuente, M. Falaschi, P. Julian, G. Vidal: Improving Control in Functional Logic Program Specialization. Proc. of the Int.l Static Analysis Symp. (SAS'98), LNCS 1503, pp.262-277, 1998.Abstract. We have recently defined a framework for Narrowing-driven Partial Evaluation (NPE) of functional logic programs. This method is as powerful as partial deduction of logic programs and positive supercompilation of functional programs. Although it is possible to treat complex terms containing primitive functions (e.g. conjunctions or equations) in the NPE framework, its basic control mechanisms do not allow for effective polygenetic specialization of these complex expressions. We introduce a sophisticated unfolding rule endowed with a dynamic narrowing strategy which permits flexible scheduling of the elements (in conjunctions) which are reduced during specialization. We also present a novel abstraction operator which carefully considers primitive functions and is the key to achieving accurate polygenetic specialization. The abstraction operator extends some recent partitioning techniques defined in the framework of conjunctive partial deduction. We provide experimental results obtained from an implementation using the Indy system which demonstrate that the control refinements produce better specializations.
==================================================
Back totop of page: Results on Transformation and Synthesis.
Primo anno di attivita'.
In [30] si e' studiata la regola di rimpiazzamento e le condizioni sotto cui essa preserva la terminazione universale. In [32] e' stata definita la classe di programmi ed interrogazioni noFD ed e' stato dimostrato che una query noFD in un programma noFD non puo' generare fallimenti finiti. Tale condizione e' importante per poter fare trasformazioni di programmi che conservano la correttezza. In realta', i vantaggi derivanti dalla conoscenza di tale proprieta' non sono limitati all'area della trasformazione di programmi. Infatti la conoscenza che un programma ha solo derivazioni di successo e' utile anche nel campo della verifica dei programmi e nell'analisi di nondeterminismo, parallelizzabilita' e dinamicita' della regola di selezione.
In [33] si e' invece definita la classe dei programmi ``successful''. Tale classe e' piu' estesa di quella dei programmi noFD in quanto include programmi che utilizzano test, e quindi possono fallire. Si e' dimostrato pero' che una query noFD con predicati ``successful'', qualora sia universalmente terminante, ha almeno un successo. Questa proprieta' e' piu' debole ma e' comunque interessante sia per la correttezza che per le trasformazioni di programmi. La proprieta' di essere ``successful'' e' complessa da verificare. Si sono quindi fornite delle tecniche per semplificarne la verifica e una metodologia per l'analisi fallimenti/successi.
Altra proprieta' dalla quale dipende l'applicabilita' di molte trasformazioni e' la terminazione. In [31] si e' studiata la classe dei programmi well-moded, programmi induttivamente ``ben formati'' rispetto alla funzionalita' input-output. Si e' fornita una caratterizzazione algebrica dei programmi well-moded che terminano che ha il pregio di essere composizionale e semplice da verificare.
Le tecniche di trasformazione di programmi possono essere utilizzate per specializzare un programma, ovvero per trasformare un programma generale in un programma che opera su di un dominio ristretto in modo piu' efficiente. In [34, 35] viene proposto un metodo di specializzazione che, data una specifica call/post (un invariante ed una post-condizione), trasforma un programma logico in un programma che soddisfa la specifica data. Il metodo si basa sulla nozione di derivazione specializzata intesa a descrivere il comportamento di un programma quando vengono assunte delle proprieta' sulle chiamate di procedura.
Unita' di Venezia: Secondo anno di attivita'.
In [BCE99b] si e' introdotta una nuova operazione di trasformazione per i programmi logici definiti che permette di scambiare due atomi nel corpo di una clausola senza alterare le proprieta' di terminazione. La condizione di applicabilita' dell'operazione e' semplice da verificare ed automatizzabile. Si e' quindi mostrato come tale operazione possa essere utilizzata per estendere il sistema di trasformazione introdotto in [A. Bossi, N. Cocco and S. Etalle. Transforming Left Terminating Programs: the reordering problem. In M. Proietti ed., Logic Program Synthesis and Transformation, Lecture Notes in Computer Science 1048, pp. 33-45, Springer-Verlag, 1996]. Il nuovo metodo di trasformazione prevede una suddivisione del programma originale in tre livelli, un nucleo di base e due estensioni successive. Il metodo risulta particolarmente valido quando i programmi da trasformare sono arricchiti con informazioni sulle modalita' di chiamata dei predicati (moding).
Durante il secondo anno si e' inoltre curata la versione finale del lavoro [33].RIFERIMENTI
[30] Bossi A., N. Cocco: Replacement Can Preserve Termination, In J. Gallagher ed., Logic Program Synthesis and Transformation, Springer-Verlag, 1997.
Abstract. We consider the replacement transformation operation, a very general and powerful transformation, and study under which conditions it preserves universal termination besides computer answer substitutions. With this safe replacement we can significantly extend the safe unfold/fold transformation sequence presented in (*). By exploiting type information, more useful conditions can be defined and we may deal with some special cases of replacement very common in practice, namely switching two atoms in the body of a clause and the associativity of a predicate. This is a first step in the direction of exploiting a Pre/Post specification on the intended use of the program to be transformed. Such specification can restrict the istances of queries and clauses to be considered and then relax the applicability conditions on the transformation operations.
(*) Bossi-Cocco: Preserving Universal Termination Through Unfold/Fold. Proc. ALP'94, LNCS 850, Springer-Verlag , 1994.--
[31] Etalle S., A. Bossi, N. Cocco: Termination of Well-Moded Programs, Journal of Logic Programming. To appear.Abstract. We study the termination properties of well-moded programs, and we show that, under suitable conditions, for these programs there exists an algebraic characterization - in the style of Apt and Pedreschi - of the property of being terminating. This characterization enjoys the properties of being compositional and, to some extent, of being easy to check.
--
[32] Bossi A., N. Cocco: Programs Without Failures, In N. Fuchs ed., Proceedings of LOPSTR'97, Lecture Notes in Computer Science 1463, Springer-Verlag, Berlin, 1998Abstract. We try to formalize the intuitive reasoning which we normally use to get convinced that a query has successful LD-derivations in a program. To this purpose we define the class of programs and queries without failures which have the property of not having finitely failing derivations. Such property is simple to verify, it is preserved through leftmost unfolding and it can be useful both in verifying properties of logic programs and in program transformation. The class of programs without failures is very restricted but in program transformations it is sufficient that only some predicates in the program are in the class.
--
[33] Bossi A., N. Cocco: Successes in Logic Programs. In: Logic-Based Program Synthesis and Transformation - LOPSTR'98 selected papers (P. Flener, ed.), Lecture Notes in Computer Science n.1559, Springer-Verlag, 1999, pp. 219-239.Abstract. We study how to verify that a pure Prolog program has solutions for a given query. The detailed analysis of the failure/success behavior of a program is necessary when dealing with transformation and verification of pure Prolog programs. In a previous work [32] we defined the class of noFD programs and queries which cannot have finitely failing derivations. Now, by introducing the concept of a set of exhaustive tests, we define the larger class of successful predicates. We prove that such predicates have at least a successful derivation for any noFD terminating query. Moreover, we propose some techniques based on program transformation for simplifying the verification of the successful condition.
--
[35] Bossi A., S. Rossi: Call-Correct Specialisation of Logic Programs, Proceedings of ICTCS'98,
ed. Degano et al., Prato, 1998.Abstract. We introduce the concept of specialisable call correct program. It is based on the notion of specialised derivation which is intended to describe program behaviour whenever some constraints on procedure calls are assumed. Secialisable call correct programs can be transformedinto call-correct ones. A sufficient condition to verify specialisable call correctness is stated.
--
[34] Bossi A., S. Rossi: Specialising Logic Programs wrt Pre/Post Specifications. Extended abstract of LOPSTR'98, Dept. of Computer Science, University of Manchester, UK, UMCS-98-6-1, 1998Abstract. In this paper we introduce the concept of specialised derivations. They are intended to describe program behaviour whenever some constraints on procedure calls (preconditions) are assumed. Operational and fixpoint semantics, in the s-semantics style, are derived. They characterize successful derivations where only atoms satisfying the given precondition are selected. A novel notion of specialised partial correcteness (s.p.c.) of a program with respect to pre/post specifications is introduced and a proof method is defined. The latter consists in one application of the specialised immediate consequence operator to the ``relevant'' part of the postcondition. Programs, which are proved to be s.p.c. wrt a given pre/post specification, can be transformed into partially correct programs.
--
[630] A. Bossi, N. Cocco, S. Etalle: Transformation of Left Terminating Programs,Proc. of the Int.l Workshop on Logic-based Program Synthesis and Transformation (LOPSTR'99), Rapporto di Ricerca CS-99-16. Dipartimento di Informatica, Universita' Ca' Foscari di Venezia, pp. 199-206, 1999.Abstract. We propose an unfold-fold transformation system which preserves left termination for definite programs besides declarative semantics. The system extends our previous proposal in [A. Bossi, N. Cocco, and S. Etalle. Transforming Left Terminating Programs: the reordering problem. In M. Proietti ed., Logic Program Synthesis and Transformation, Lecture Notes in Computer Science 1048, pp. 33-45, Springer-Verlag, 1996], by introducing a new switching operation. The new operation allows us to switch the atoms in the clause bodies when a specific applicability condition is satisfied. The applicability condition is very simple to verify, yet very common in practice. We also discuss how to verify such condition by exploiting moding information.
==================================================