D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231--277, 1999.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

.... programs, a narrowing driven partial evaluator is also able to improve programs even when no input data are provided (e.g. by removing unnecessary data structures) These remarks also apply to several partial evaluation methods for logic programs, e.g. conjunctive) partial deduction [26] [13], as well as to some (online) methods for functional programs like supercompilation [35] generalized partial computation [15] and positive supercompilation [32] the closest to our framework. An implementation of the partial evaluator has been successfully incorporated into the latest ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231--277, 1999.

....interpretation (e.g. by approximating the operational semantics presented in Sect. 3. 2) A different line of research involves the de nition of a forward slicing technique for logic programs by exploiting the similarities between narrowing driven specialization and conjunctive partial deduction [9]. In this context, precision could be improved by considering re ned frameworks for partial deduction like, e.g. abstract partial deduction [20] This topic is subject of ongoing work. Acknowledgements We gratefully acknowledge the anonymous referees as well as the participants of LOPSTR 2002 ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231-277, 1999.

....deduction is applied, is deterministic. We show that by applying partial deduction to a nondeterministic version of the matching program, one cannot derive a specialized program which is deterministic, and thus, one cannot get a program which corresponds to a DFA. Conjunctive partial deduction [8] is a program specialization technique which extends partial deduction by allowing the specialization of logic programs w.r.t. conjunctions of atoms, instead of a single atom. Conjunctive partial deduction can be realized by the de nition, unfolding, and folding rules where each new predicate ....

....zero( 0; 0; 1] Ys ) C G for (that is, non zero( 0; 1] Ys ) 3 Partial Deduction via Unfold Fold Transformations In this section we recall the rule based approach to partial deduction. We also point out some limitations of partial deduction [35, 40] and conjunctive partial deduction [8]. These limitations motivate the introduction of the new, enhanced rules and strategies for program specialization presented in Sections 4, 5, and 6. 3.1 Transformation Rules and Strategies for Partial Deduction In the rule based approach, partial deduction can be viewed as the construction of a ....

[Article contains additional citation context not shown here]

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(2-3):231-277, 1999.

....subsidiary strategy, and (ii) the set of de nitions which are introduced for performing folding steps. In particular, for ensuring termination it may be necessary to consider suitable generalizations of the bodies of the clauses to be folded (see, for instance, the techniques presented in [5, 8, 12, 18, 20, 26]) However, the generalization technique required when applying the Determinization Strategy is more sophisticated than the ones proposed for the case of partial evaluation of (constraint) logic programs [8, 12, 20] This is due to the fact that the new de nitions which are introduced during the ....

....slightly modify the transformation rules and the transformation strategy if di erent semantics are to be preserved. The Determinization Strategy is an extension to constraint logic programs of the strategy presented in [23] Our strategy is also an enhancement of conjunctive partial deduction [5], in that we allow new predicates to be de ned in terms of disjunctions of conjunctions of constrained atoms. We have used our strategy for specializing constrained matching algorithms and we have derived programs which are highly ecient because, as in the case of the Knuth Morris Pratt matcher, ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. J. Logic Programming, 41(2-3):231-277, 1999.

....a concept also seen in Smith, Wand, Danvy and Asai s re ective tower languages Brown, Blonde and Black. 2.5 Challenging Problems 2.5.1 On the state of the art in partial evaluation. Partial evaluation has been most successful on simple pure languages such as Scheme [6, 7, 14, 45] and Prolog [60], and there has been some success on C: the C mix [28] and Tempo systems [16] Further, Schultz has succeeded in doing Java specialization by translating to C, using the Tempo system, and the translating back [61] There have been a number of practically useful applications of partial evaluation, ....

Danny De Schreye, Robert Gluck, Jesper Jrgensen, Michael Leuschel, Bern Martens, and Morten H. B. Srensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(2&3):231{ 277, 1999.

....the niteness of (i) the unfolding subsidiary strategy and (ii) the set of de nitions which are introduced for performing folding steps. In particular, for ensuring termination it may be necessary to consider suitable generalizations of the bodies of the clauses to be folded (see, for instance, [5], 7] 10] 15] 16] 22] As a consequence of Theorem 1, if the Determinization Strategy terminates, then the specialized program Psp is equivalent to the initial program P in the following sense: for every constraint d, lm(P; D) j= 9(d c p(t1 ; t h ) i lm(Psp ; D) j= 9(d ....

.... to reason by cases as often done in various specialization techniques (see, for instance, 9] 13] 22] Clause splitting, together with the other familiar unfolding and folding rules, is applied according to the Determinization Strategy which is an enhancement of conjunctive partial deduction [5]. Indeed, we allow new predicates to be de ned in terms of disjunctions of conjunctions of constrained atoms. The Determinization Strategy is an extension to constraint logic programs of the strategy presented in [19] We have used our strategy for specializing constrained matching algorithms and ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. J. Logic Programming, 41(2-3):231-277, 1999.

.... Proietti [11] manipulate dags in a fashion that is very similar to our notion of a proper split. It seems that we are able to synchronise common calls, because we use a local global unfolding strategy similar to what is used in partial deduction (see e.g. Gallagher [4] or De Schreye, et.al. [3]) Further work needs to be done in three directions. Firstly, we need to prove the eciency and correctness properties conjectured in this paper. Secondly, we want to investigate the exact relationship between tupling and graph based supercompilation. Thirdly, to establish empirical results, an ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(2-3):231-277, 1999.

.... sage, paddy, mixtus, ecce) as well as semi automated ones (logimix, leupel, logen) have been developed and successfully applied to at least medium size applications [25, 15] 1 Another recent line of research has focussed on overcoming some of the inherent limitations of partial evaluation, 24] [26, 14] [23, 22] integrating ideas from constraint logic programming, unfold fold program transformation, and abstract interpretation respectively while keeping the above described advantages in terms of complexity and automatic controllability. Personal Details: The proposer has received his PhD ....

....trees, which are in but the most simplest of cases infinite. To be able to extract a finite and efficient specialised program, these infinite computation trees have to be abstracted in a finite but also as precise as possible way. Several fully automatic techniques have been developed for this [17, 27, 21, 14], taking precision considerations into account, while still ensuring termination 3 in a non ad hoc manner. At first sight, these techniques seem to be an ideal starting point for our problem; a belief which we propose to further investigate in this research project. The fact that we require ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. The Journal of Logic Programming, 41(2 & 3):231--277, 1999. To appear.

....of the transformation rules presented in Section 3.4 so to derive ecient, specialized programs with reduced nondeterminism. In particular, we get derived programs which are semideterministic. As we will indicate in Section 7, our strategy is an enhancement of the specialization technique [5], called conjunctive partial deduction, which allows the introduction of new predicates de ned in terms of conjunctions of atoms. Our Determinization Strategy is based upon three subsidiary strategies: i) the Unfold Simplify subsidiary strategy, which uses the safe unfolding, equation ....

.... de ned in terms of disjunctions of conjunctions of atoms (recall that a set of clauses with the same head is equivalent to a single clause whose premise is the disjunction of the bodies of the clauses in the given set) Thus, our technique improves over the one of conjunctive partial deduction [5], which is a specialization technique where new predicates are de ned in terms of conjunctions of atoms. The use of the case split rule is a form of reasoning by cases, which is a very well known technique in mechanical theorem proving (see, for instance, the Edinburgh LCF theorem prover [14] ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(2-3):231-277, 1999.

....performing program derivation in di erent computation domains. The work on unfold fold program transformation is tightly related to other transformation techniques. In particular, partial evaluation (also called partial deduction) and other program specialization techniques la Lloyd Shepherdson [16,27,44,47] can be rephrased in terms of a subset of the unfold fold rules [56,67] Compiling control [7] is another transformation technique which is related to the rules and strategies approach. Compiling control is based on the idea expressed by Kowalski s motto: Algorithm = Logic Control, and it works ....

D. De Schreye, R. Glck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(23):231277, 1999.

....specializations for the same function definition and can also combine distinct original function definitions into a comprehensive specialized function. This means that narrowing driven PE has the same potential for specialization as positive supercompilation [25] and conjunctive partial deduction [10]. Despite its power, the narrowing driven approach to PE suffers from several limitations: i) Firstly, in the context of lazy functional logic languages, expressions in head normal form (i.e. rooted by a constructor symbol) cannot be evaluated at PE time. This restriction is imposed because the ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231--277, 1999.

....the values of the input variables can be precomputed in f 0 . In fact, narrowing driven PE is able to achieve some form of composition and tupling automatically [6] These remarks also apply to several PE methods for logic programs (e.g. partial deduction [26] and conjunctive partial deduction [14]) as well as to some (on line) PE methods for functional programs (like supercompilation [31] generalized partial computation [15] and positive supercompilation [30] the closest to our framework [4, 6] As a starting point, we extend the standard semantics for functional logic programs in at ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231-277, 1999.

....based on the above framework. The system is written in Prolog and accepts unconditional term rewriting systems as programs. The narrowing driven approach to PE has the same potential for specialization as positive supercompilation [29] of functional programs and conjunctive partial deduction [10] of logic programs (it has been experimentally tested in [2, 4] Unfortunately, the use of Indy within a realistic functional logic language (e.g. Curry [15] Escher [22] or Toy [24] becomes impractical since there are many facilities of these languages (e.g. higher order functions, ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231--277, 1999.

....based on the above framework. The system is written in Prolog and accepts unconditional term rewriting systems as programs. The narrowing driven approach to PE has the same potential for specialization as positive supercompilation [29] of functional programs and conjunctive partial deduction [10] of logic programs (it has been experimentally tested in [2, 4] Unfortunately, the use of Indy within a realistic functional logic language (e.g. Curry [15] Escher [22] or Toy [24] becomes impractical since there are many facilities of these languages (e.g. higher order functions, ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231-277, 1999.

....data sources. Our algorithms for merging multiple code call conditions take such invariants and cost information into account when performing the merge. Another area of research that is related to ours is partial evaluation in logic programs [Leuschel et al. 1998; Lloyd and Shepherdson 1991; De Schreye et al. 1999]. Partial evaluation takes a program and a goal and rewrites the program by using a set of transformations to optimize its performance. The rewritten program usually runs faster for the particular goal when SLD or SLD NF resolution is used for query processing. On the other hand, our framework ....

De Schreye, D. et al. 1999. Conjunctive partial deduction: foundations, control, algorithms and experiments. Journal of Logic Programming 41, 2-3, 231--277.

....example of a change of data representations is given in Section 4. 3, where we show how to transform logic programs which use lists into equivalent logic programs which use di erence lists (see Example 7 below) Conjunctive Partial Deduction Conjunctive partial deduction has been proposed in [49] as an extension of partial evaluation, whereby conjunctions of atoms, rather than single atoms (as done in [104] are taken into consideration. The techniques presented in [49] recast in the style of Lloyd and Shepherdson s [104] those for the elimination of intermediate data structures ....

....(see Example 7 below) Conjunctive Partial Deduction Conjunctive partial deduction has been proposed in [49] as an extension of partial evaluation, whereby conjunctions of atoms, rather than single atoms (as done in [104] are taken into consideration. The techniques presented in [49] recast in the style of Lloyd and Shepherdson s [104] those for the elimination of intermediate data structures described in [125] However, these techniques neither can combine partial evaluations of alternative branches of the SLD trees, nor can introduce disequalities. Thus, our de nition and ....

D. De Schreye, R. Glck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(23):231277, 1999.

....(1) The most apparent difference is that traditional techniques for partial eval uation do not handle constraints, so that our optimizations concerning constraint solving cannot be performed. 2) Partial evaluation may require post processing methods, like Redundant Argument Filtering [19], to minimize the number of variables occurring in clauses, whereas we use the folding rule during program specialization to avoid redundant occurrences of variables. 3) The use of our contextual constraint replacement rule R5 allows us to perform optimizations which cannot be performed by ....

DE SCHREYE, D., GLOCK, R., JORGENSEN, J., LEUSCHEL, M., MARTENS, B., AND SORENSEN, M. H. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Pro- gramming 41, 2-3 (1999), 231-277.

No context found.

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. Journal of Logic Programming, 1999. To appear.

....as body. Further details on correctness and control of on line partial deduction can be found in [13] and e.g. 6, 10, 15, 16] respectively. Finally, it can be noted that partial deduction automates a subset of unfold fold transformations [19] Comments on the relationship can be found in [17] and [3]. 2.3 The Problems That Be An unfolding criterion based on the partial SLD tree built so far works well if all information necessary to unfold deeply enough without endangering termination is present in that tree. For example, when building a derivation for the atom append( 1; 2; 3] Y; Z) no ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. 1998. Submitted for publication.

.... atom in S a di erent specialised predicate definition will be generated) Given closedness (all leaves are an instance of a specialised atom) and independence (no two specialised atoms have a common instance) correctness of the specialised program is guaranteed [28] Independence is usually (e.g. [25, 5]) ensured by a renaming transformation which maps dependent atoms to new predicate symbols (and often lters out constant parts as well) Closedness is more dicult to ensure, but can be satis ed using the following generic algorithm based upon [25] This algorithm structures the atoms to be ....

....following generic algorithm based upon [25] This algorithm structures the atoms to be specialised in a global tree: i.e. a tree whose nodes are labelled by atoms and where A is a descendant of B i specialising B lead to the specialisation of A. Apart from the missing treatment of conjunctions [5] the following is the algorithm implemented in the ecce system [21] which we will employ later on. Algorithm 3.1 (generic partial deduction algorithm) Input: a program P and a goal A Output: a set of atoms or conjunctions A and a global tree Initialisation: a global tree with a ....

[Article contains additional citation context not shown here]

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. The Journal of Logic Programming, 41(2 & 3):231-277, November 1999.

....consideration. Indeed, partial deduction will unfold the initial query of interest until it spots a dangerous growth, at which point it will generalise the o ending calls and restart the unfolding from the thus obtained more general call. Provided a suitably re ned control technique is used (e.g. [17, 4]) one can guarantee termination as well as a precise ow analysis. As was shown in [15] such a partial deduction approach is powerful enough to provide a decision procedure for coverability problems for (reset) Petri nets and bears resemblance to the Karp Miller procedure [12] In the context of ....

.... that a call must represent all its instances (the same holds for narrowing based partial evaluation [1] Fortunately, this restriction has been lifted, e.g. in the abstract partial deduction framework of [14] In essence, 14] extends partial deduction and conjunctive partial deduction [4] by working on abstract conjunctions on which abstract unfolding and abstract resolution operations are de ned: An abstract conjunction is linked to the concrete domain of ordinary conjunctions via a concretisation function . In contrast to classical partial deduction, can be much more re ....

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. J. Logic Program., 41(2 & 3):231-277, 1999.

....We also define the set of leaves, leaves( to be the leaf goals of . Given closedness (all leaves are an instance of a specialised atom) and independence (no two specialised atoms have a common instance) correctness of the specialised program is guaranteed [25] Independence is usually (e.g. [23, 5]) ensured by a renaming transformation. Closedness is more difficult to ensure, but can be satisfied using the following generic algorithm based upon [27, 23] This algorithm structures the atoms to be specialised in a global tree: i.e. a tree whose nodes are labeled by atoms and where A is a ....

....generic algorithm based upon [27, 23] This algorithm structures the atoms to be specialised in a global tree: i.e. a tree whose nodes are labeled by atoms and where A is a descendant of B if specialising B lead to the specialisation of A. Apart from the missing treatment of conjunctions [5] the following is basically the algorithm implemented in the ecce system [23, 5] which we will employ later on. Algorithm 3.1 (generic partial deduction algorithm) 3 An incomplete SLD tree is a SLD tree which, in addition to success and failure leaves, also contains leaves where no literal has ....

[Article contains additional citation context not shown here]

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. J. Logic Progam., 41(2 & 3):231--277, November 1999.

No context found.

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231--277, 1999.

No context found.

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231-277, 1999.

No context found.

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. Submitted for Publication, January 1997.

No context found.

D. De Schreye, R. Gluck, J. Jrgensen, M. Leuschel, B. Martens, and M.H. Srensen. Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming, 41(2&3):231-277, 1999.

No context found.

D. De Schreye, R. Gluck, Jesper Jrgensen, M. Leuschel, B. Martens, and M. H. Srensen. Conjunctive partial deduction: foundations, control, algorithms, and experiments. Journal of Logic Programming, 41(23) :231--277, 1999.

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.