Tadashi Kawamura and Tadashi Kanamori. Preservation of stronger equivalence in unfold/fold logic program transformation. Theoretical Computer Science, 75:139--156, 1990.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

.... of ensuring termination of the partial evaluation process is addressed in [Hol91] Upper bounds for the speedup possible by applying unfold fold transformations have been given in [Han91] Hon91] Several ways to guarantee total correctness have been proposed in the literature, e.g. TS84] [KK90], Sek91] Kot85] GS91] PP91a] They all work by putting forward some restrictions on the types of foldings allowed. For a more detailed description (and comparison with our approach) see Sect. 5. The purpose of this paper is to present a model for unfold fold transformations which enables ....

....for all B, cf. Theorem 13. More specific versions of this theorem are stated in [PP91a] and [Han91] Theorem 22. Suppose all rules at level 1 satisfy A. Then A holds, and thus [ B] 2 = B] 1 for all strategy independent B, cf. Theorem 14. As the correctness condition for folding, TS84] and [KK90] essentially use (a special case of) A. For proofs of Theorem 20, 21 and 22 (which all elaborate on the intuition presented in section 1) see [Amt92] Example 5. Continuing from Example 4, we by Theorem 21 can conclude that L holds which is as expected since S 2 loops on p(t) by the LR ....

[Article contains additional citation context not shown here]

Tadashi Kawamura and Tadashi Kanamori. Preservation of stronger equivalence in unfold/fold logic program transformation. Theoretical Computer Science, 75:139--156, 1990.

....for the above mentioned transformations w.r.t. the least Herbrand model, ii) the generalization of [13] that the same authors presented in [14] where a lexicographic ordering between atoms is adopted for proving the correctness of a more powerful folding transformation, and (iii) the papers [3, 6, 12] which extend the proofs of correctness of the folding and unfolding transformations w.r.t. universal termination, computed answer substitutions, and nite failure semantics. For lack of space, we have not presented these special cases in detail. However, in all these cases one may: i) describe ....

T. Kawamura and T. Kanamori. Preservation of stronger equivalence in unfold /fold logic program transformation. Theoretical Computer Science, 75:139{ 156, 1990.

....several extensions of the original Tamaki and Sato s rules have been studied. It has also been 15 proved that, under suitable hypotheses, the unfold fold rules preserve several semantics of de nite logic programs, such as computed answers, nite failure, pure Prolog, and left termination (see [14, 39, 77, 92, 100, 105, 123]) The transformational approach has also been considered in the case of various extensions of de nite logic programs, such as logic programs with negation (see Section 5) constraint logic programs [8, 64, 106] and concurrent constraint programs [65, 148] General methods for proving the ....

T. Kawamura and T. Kanamori. Preservation of stronger equivalence in unfold/fold logic program transformation. Theoretical Computer Science, 75:139156, 1990.

....van Emden and Kowalski s semantics which is correct wrt successful derivations only. The need for a formal semantics correct wrt ca gave rise to several new definitions and was recognized especially in the case of semantics based abstract interpretation [32, 3, 11] and program transformation [25, 6], where also less abstract observables (such as partial computed answers) have sometimes to be modeled [11] In addition to the problem of modeling observational equivalences, there exists an important property which does not hold in the least Herbrand model semantics, i.e. compositionality wrt ....

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold/Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413--422. Institute for New Generation Computer Technology, Tokyo, 1988. 35

....preserves both soundness and completeness. Variants of the above transformation rules can be shown to be correct w.r.t. richer logic languages and other program semantics (see, for instance, Aravindan Dung 93, Bossi Cocco 93, Bossi Cocco Etalle 92, GardnerShepherdson 91, Kanamori Horiuchi 87, Kawamura Kanamori 88, Maher 93, Proietti Pettorossi 91a, Sato 92, Seki 91, Seki 93] and [Pettorossi Proietti 94] for an overview) 3.2 Transformation Strategies for Logic Programs Here we list some of the strategies we use for transforming logic programs. i) Predicate Tupling Strategy. This strategy, also called ....

Kawamura, T., Kanamori, T.: Preservation of Stronger Equivalence in Unfold/Fold Logic Program Transformation. Proc. Int. Conf. on Fifth Generation Computer Systems, Tokyo (Japan) (1988) 413--422

....the intermediate data structure. The composition can be made automatically [30] whereas tupling has only been automated to some extent [9, 10] Although a lot of literature has been devoted to proving the correctness of fold unfold systems w.r.t. the various semantics proposed for logic programs [7, 13, 20, 21, 23, 28], in functional programming the problem of correctness has received surprisingly little attention [26, 27] Of the very few studies of correctness of fold unfold transformations in functional programming, the most general and recent work is [26] which defines a simple (syntactic) condition for ....

....is not only safe but also helpful as it will become apparent in Example 3. ii) In contrast to [2] the substitution of Def. 4 is not a unifier but just a matcher. This is similar to many other folding rules for logic programs, which have been defined in a similar functional style (see, e.g. [7, 20, 24, 28]) iii) Finally, the non erasing condition in Def. 1 can now be fully clarified: it avoids to consider a rule l r, with Var(r) ae Var(l) as a folding rule, since it might introduce extra variables in the rhs of the resulting rule. Many attempts have been also made to define a folding ....

[Article contains additional citation context not shown here]

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold /Fold Logic Program Transformation. TCS, 75:139--156, 1990.

....(which is not necessarily terminated) and by assuming that c n = false in the last con guration of the derivation above. 2 In the following we call split derivations both successful, deadlocked and failed split derivations. The previous de nition is inspired by the de nition of descent clause of [KK88]; however, here we use a di erent notion of weight and rather di erent conditions on them. The following notion of mode will be useful to short the notation. De nition 4.6 Let D 0 ; D n be a transformation sequence, A be an agent and d be a constraint. We de ne the mode m(A; d) of the ....

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold/Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413-422. Institute for New Generation Computer Technology, Tokyo, 1988.

....transformations is to reduce the complexity of a first order Horn theory as measured by the number of possible ground instantiations of clauses. Unfold fold transformations were originally introduced by Tamaki and Sato [28] to enhance the efficiency of logic programs. Kawamura and Kanamori [11] show the equivalence preserving nature of the transformation rules. A precise definition of the transformation rules is given in the Appendix. We will propose theory transformation to solve the instantiation problem , i.e. the problem that simple minded instantiation of variables by con10 ....

Tadashi Kawamura and Tadashi Kanamori. Preservation of stronger equivalence in unfold/fold logic program transformation. Theoretical Computer Science, 75:139--156, 1990.

....the correctness results for the declarative semantics that hold for the system of [TS84] are valid for our system as well and we have the following. Remark 15. Let P 0 ; Pn be a transformation sequence. TS84] The least Herbrand models of the initial and final programs coincide. [KK90] The computed answers substitution semantics of the initial and final programs coincide. 4 Preservation of Left Termination The system presented in the previous section does not preserve left termination yet. This is because the switching operation is unrestricted : It has no special ....

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold /Fold Logic Programming Transformation. Theoretical Computer Science, 75(1&2):139--156, 1990.

....On the other hand, when using divide and conquer, the number of SLD refutations of the positive examples is the same for both the overly general and the resulting hypothesis. This follows from the fact that the number of SLD refutations does not increase when unfolding is applied (proven in [ Kanamori and Kawamura,1988 ] In order to reduce the amount of redundancy when using divide and conquer, only a minor change to the algorithm is needed: instead of placing a positive example in all subsets that correspond to clauses that cover the example, the example can be placed in one such subset. 3 Empirical ....

Kanamori T. and Kawamura T., "Preservation of Stronger Equivalence in Unfold/Fold Logic Program Transformation (II)", ICOT Technical Report TR-403, Japan (1988)

....examples covered by the current clause. In such cases, it seems more appropriate to count the number of SLD refutations of positive and negative examples, rather than just counting the number of covered examples, as the number of SLD refutations does not change when unfolding is applied (shown in [15]) 7 2.3 Guaranteeing Unique Sequences of Input Clauses One of the conditions for Covering and Divide and Conquer to produce valid hypotheses is that no positive and negative examples have the same sequence of input clauses in their SLD refutations. In this section, we present a transformation ....

....On the other hand, when using Divide and Conquer, the number of SLD refutations of the positive examples is the same for both the overly general and the resulting hypothesis. This follows from the fact that the number of SLD refutations does not increase when unfolding is applied (proven in [15]) In order to allow for reduction of the amount of redundancy when using Divide and Conquer, only a minor change to the algorithm is needed: instead of placing a positive example 11 in all subsets that correspond to clauses that cover the example, the example can be placed in one such subset. 4 ....

Kanamori T. and Kawamura T., "Preservation of Stronger Equivalence in Unfold/Fold Logic Program Transformation (II)", ICOT Technical Report TR-403, Japan (1988)

....Sg. Let L = f R i S j ji; j 0; i j 0 g. Then, QL (EDB) f(a; b) a; c) a; d) b; c) b; d) c; d)g: The spelled words are R, RR, RRS, R, RS, S, respectively. 2. 2 Logic program transformation In the transformation system of [23] which we adopt (in the formulation which appears in [14]) a sequence P 0 , P n of definite logic programs is generated, starting from the initial program P 0 , by applying the unfold fold transformation rules [23,19,21,11,12] defined below, and by introducing clauses defining new predicates (called Eureka definitions) 19] The unfold fold ....

T. Kawamura and T. Kanamori. Preservation of stronger equivalence in unfold/fold logic program transformations. Theoretical Computer Science, 75:139--156, 1990.

....Learning in this domain, our method is able to derive sufficient and correct (although possibly lengthy) classification rules for arbitrary games and positions. In the realm of Partial Evaluation, correctness results for program transformation systems have already been established (cf. [KaKa88], Ll91] TaSa84] These concern procedural (as in the theorem above) as well as declarative (i.e. model based) semantics. However, the expansion of negative subgoals is only considered for limited cases, since its variables generally do not become fully instantiated at partial evaluation time ....

Kawamura, T., and Kanamori, T., Preservation of Stronger Equivalence in Unfold/Fold Logic Program Transformation, ICOT Technical Report, Tokyo, (1988)

....Page: 1 19 The original unfold fold transformation system of Tamaki and Sato [44] is meant for definite programs, and is shown to be correct wrt the least Herbrand model semantics of a definite program. Later, the same system was shown to preserve answer substitutions, by Kawamura and Kanamori [27]. The correctness of the transformation technique, when applied to normal programs, is closely related to how we understand the negation in a program. So far, numerous non monotonic approaches to handle negation have been proposed, and the relationship among them is well studied [e.g. ....

....have been obtained so far, for the unfold fold transformation system described above. Initially, Tamaki and Sato showed that this transformation is correct for definite programs wrt least Herbrand model semantics [44] Later Kawamura and Kanamori obtained a stronger result for definite programs in [27], stating that the set of all computed answer substitutions 2 of definite programs are preserved by this transformation. In [31] Maher showed that the transformation system with MGS folding also preserves the least Herbrand model semantics. For normal programs, correctness of unfold fold ....

[Article contains additional citation context not shown here]

Kawamura,T. and Kanamori,T., Preservation of stronger equivalence in Unfold/Fold logic program transformation, Theoretical Computer Science 75:139-156 (1990).

....P , briefly it is an unfolding of P . The clauses fc 1 ; c n g are called unfoldings of c. 2 Unfolding is a complete transformation for all queries. The result is due to the independence of the selection rule and the fact that unfolding preserves the computed answer substitution semantics [10, 22]. In [11] we proved that it is also non increasing. Hence no restrictive condition is necessary in order to preserve universal termination and c.a.s. when using unfolding alone. The stronger property of being strictly decreasing becomes useful when composing unfolding with folding. Definition 8 ....

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold/Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413--422. Institute for New Generation Computer Technology, Tokyo, 1988.

....we can choose the top predicates in P 0 in various ways. Notice also that dependencies of some intermediate predicates on top predicates may be introduced by folding steps (see the second correctness theorem below) The approach we follow here is more general than the approach described in [ Kawamura and Kanamori, 1990 ] where only two sets of predi Transformation of Logic Programs 31 cates are considered (the so called new predicates and old predicates) Let us also introduce a new goal replacement rule, called basic goal replacement , which is a particular case of independent goal replacement. Rule R5.6 ....

....page 22) Rule R5.8 Deletion of Duplicate Clauses. By the rule of deletion of duplicate clauses we replace all occurrences of a clause C in a program by a single occurrence of C. Several researchers have addressed the problem of proving the correctness of the transformation rules w.r.t. CAS [ Kawamura and Kanamori, 1990; Bossi et al. 1992a; Bossi and Cocco, 1993 ] We now present for the CAS semantics two theorems which correspond to the first and second correctness theorems w.r.t. the LHM semantics. As already mentioned, in these theorems the various instances of the goal replacement rule refer to the ....

T. Kawamura and T. Kanamori. Preservation of stronger equivalence in unfold/fold logic program transformation. Theoretical Computer Science, 75:139--156, 1990.

....into equivalent, more efficient ones. Afterwards, Tamaki and Sato [19] proposed an elegant framework for the transformation of logic programs based on the same rules. Their system was proven to be correct w.r.t. the least Herbrand model semantics [19] and the computed answer substitution semantics [13]. The system was later extended to logic programs with negation and serious research effort has been devoted to proving its correctness w.r.t. the various semantics available for normal programs. All the (unfold fold) transformation systems proposed so far for (constraint) logic programs, with the ....

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold /Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413--422. ICOT, Tokyo, 1988.

....and optimization [25] Soon later, Tamaki and Sato [37] proposed an elegant framework for the transformation of logic programs based on unfold fold rules. Their system was proven to be correct w.r.t. the least Herbrand model semantics [37] and the computed answer substitution semantics [24]. The system was then extended by Seki [34] to logic programs with negation, in particular he provided new, more restrictive applicability conditions which guarantee that the system preserves also the finite failure set and the perfect model semantics of stratified programs. Since then serious ....

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold/Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413--422. Institute for New Generation Computer Technology, Tokyo, 1988.

....A 7 B , B , C F , B , B is the folded clause of clause X with respect 1 i n 1 m to clause Y. In this case, we say that we fold clause Y into clause X. It has been shown that equivalence is preserved in a logic program that undergoes the unfolding and folding under certain circumstances (Kanamori Kawamura, 1988). Kanamori and Kawamura have shown that clause X may be folded into clause Y as long as: 1. clause Y was produced from the original program via unfolding clause X 2. the predicate in the head of clause X does not appear (with the same arity) anywhere else in the original program 19 Note that ....

Kanamori, T. & Kawamura, T. (1988). Preservation of Stronger Equivalence in Unfold/Fold Logic Program Transformation. ICOT Technical Report TR-403, Mitsubishi Electric Corporation, Amagasaki, Japan.

....starting from P 0 . Example 4 (Continued from example 3) The sequence of programs P 0 ; P 1 ; P 2 ; P 3 in examples 1, 2 and 3 is a transformation sequence starting from P 0 . 4 Correctness proof The correctness of the transformation rules is proved in this section along the same line as in [TS84, TS86, KK90]. For this, we first introduce the notions of partial and total correctness. Definition15 (Partially Correct Transformation) Let P 0 be the initial program in a transformation sequence, and P i a program obtained from P 0 by applying the transformation rules. The transformation is said to be ....

T. Kawamura and T. Kanamori. Preservation of stronger equivalence in unfold/fold logic program transformations. Theoretical Computer Science, 75:139--156, 1990.

....semantics. This is the reason why the need for a different formal semantics was recognized by many authors, giving rise to several new definitions [30, 49, 113, 42] The need for better semantics was also recognized in the case of semantics based abstract interpretation [94] and transformation [76]. 1.4 Compositionality In addition to the problem related to modeling the computed answers observational equivalences, there exists another problem with the least Herbrand model semantics. Namely a very important property, i.e. compositionality, does not hold. Compositionality has to do with a ....

....a [ compositional program equivalence 7 . Most of the transformation techniques are proved to be safe w.r.t. the declarative semantics only, thus failing to capture the safeness w.r.t. the more complex observable behavior. In some cases the observational equivalences related to computed answers [76, 89] and to finite failures [102] are considered. Usually proving that the transformation preserves the observational equivalence is rather complex (see, for example, the proofs of the partial evaluation theorems in [89] The same goal could more easily be achieved by proving that the transformation ....

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold/Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413--422. Institute for New Generation Computer Technology, Tokyo, 1988.

....and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires fees and or specific permissions. c flACM 0164 0925 94 0700 1081 03.50 As the large literature shows [TS84, KK88, Sek90, Sek91, Sek93, AD93], a lot of research has been devoted to proving the correctness of the system wrt the various semantics proposed for logic programs. However the question of the consequences of the transformation on the (universal) termination of the program has not yet been tackled. Recall that a program is ....

....This is due to the fact that it does not always preserve the declarative semantics and thus its use must be restricted by some applicability conditions. Depending on the approach, such conditions can be either a constraint on how to sequentialize the operations while transforming the program [TS84, KK88], or can be expressed in terms of semantic properties of the program, independently from its transformation history [BC93, Mah87] In the method proposed by Tamaki and Sato [TS84] the transformation sequence and the folding operation are defined in terms of each other. Definition 3.4 ....

[Article contains additional citation context not shown here]

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold/Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413--422. Institute for New Generation Computer Technology, Tokyo, 1988.

.... [10] this is not the case of the classical van Emden and Kowalski s semantics [27] The need for a different semantics (correct wrt computed answers) gave rise to several new definitions and was particularly recognized in the case of abstract interpretation [25, 2, 6] and program transformation [20, 3], where also less abstract observables (e.g. partial computed answers) have sometimes to be modeled [6] In addition to the problem of modeling observational equivalences, there exists an important property which does not hold in the least Herbrand model semantics, i.e. OR compositionality. A ....

T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold /Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413--422. ICOT, Tokyo, 1988.

No context found.

T. Kanamori and T. Kawamura. Preservation of stronger equivalence in unfold/fold logic program transformation (ii). Technical Report TR-403, ICOT, June 1988.

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.