The DOI matches its Crossref record.
Ensuring Global Termination of Partial Deduction While Allowing Flexible Polyvariance
Open accessAbstract
The control of polyvariance is a key issue in partial deduction of logic programs.Certainly, only nitely many specialised versions of any procedure should be generated, while, on the other hand, overly severe limitations should not be imposed.In this paper, well-founded orderings serve as a starting point for tackling this so-called \global termination" problem.Polyvariance is determined by the set of distinct \partially deduced" atoms generated during partial deduction.Avoiding ad-hoc techniques, we formulate a quite general framework where this set is represented as a tree structure.Associating weights with nodes, we de ne a well-founded order among such structures, thus obtaining a foundation for certi ed global termination of partial deduction.We include an algorithm template, concrete instances of which can be used in actual implementations, prove termination and correctness, and report on the results of some experiments.Finally, we conjecture that the proposed framework can support further advances towards (fully automatic) optimal program specialisation.
Overview
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Partial evaluation of functional-logic programs already features the use of homeomorphic embedding and m-trees.
“Indeed, partial evaluation of functional-logic programs [Alpuente et al. 1996;1997;Lafave and Gallagher 1997] already features the use of homeomorphic embedding and m-trees [Martens and Gallagher 1995].”
From Controlling generalization and polyvariance in partial deduction of normal logic programs (1998) · cites this paper as Martens and Gallagher 1995
Section 3 presents an m-tree-based algorithm for partial deduction, supporting the m-tree part of the attribution. The passages on termination and the algorithm do not describe using homeomorphic embedding; searches for that term and its use in termination found no supporting passage. The paper addresses logic-program partial deduction, while the functional-logic-program context is attached to the other citations in the sentence. (LLM, conf=0.85)
Experimental — accuracy not yet measuredNeighborhoods of order n, forming the basis for generalization in full supercompilation [Turchin 1988], are essentially the same as classes of atoms or goals with an identical depth-n characteristic tree.
“It is also interesting to return to an observation already made in Section 4 of Martens and Gallagher [1995]: neighborhoods of order”
From Controlling generalization and polyvariance in partial deduction of normal logic programs (1998) · cites this paper as Martens and Gallagher [1995]
Section 4 (page unavailable) says that supercompilation neighborhoods reflect a computation history of order n and that this “seems to be related” to characteristic trees with depth bound n. It does not establish that neighborhoods are essentially the same as classes of atoms or goals with identical depth-n characteristic trees; the claim states the relationship more strongly than the source does. (LLM, conf=0.86)
Experimental — accuracy not yet measuredIf A and B are expressions such that B is strictly more general than A, then h(A) > h(B).
“Lemma C.2. If A and B are expressions such that B is strictly more general than A, then h(A) > h(B).”
From Controlling generalization and polyvariance in partial deduction of normal logic programs (1998) · cites this paper as Martens and Gallagher [1995]
Lemma 3.23 states the inequality for atoms: if B is strictly more general than A, then h(A) > h(B). The citing sentence broadens “atoms” to “expressions,” which the lemma does not establish. The supplied copy gives no page number for the lemma. (LLM, conf=0.88)
Experimental — accuracy not yet measuredBlending the general framework in Martens and Gallagher [1995] with the framework developed in Section 3 yields an apparatus for on-line global control of partial deduction.
“In Section 4 we then solve the second problem, blending the general framework in Martens and Gallagher [1995] with the framework developed in Section 3. We thus obtain an elegant, sophisticated, and precise apparatus for on-line global control of partial deduction.”
From Controlling generalization and polyvariance in partial deduction of normal logic programs (1998) · cites this paper as Martens and Gallagher [1995]
Importing and adapting m-trees of Martens and Gallagher [1995] overcomes the need for a depth bound on characteristic trees to guarantee termination of partial deduction.
“Importing and adapting m-trees of Martens and Gallagher [1995], we have overcome the need for a depth bound on characteristic trees to guarantee termination of partial deduction.”
From Controlling generalization and polyvariance in partial deduction of normal logic programs (1998) · cites this paper as Martens and Gallagher [1995]
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Citations
Cites
No references could be resolved yet.
Research works printed but not linked: 32
- K. Benkerimi and P. M. Hill. Supporting transformations for the partial evaluation of logic programs. Journal of Logic and Computation, 3(5):469{486, 1993.
- K. Benkerimi and J. W. Lloyd. A partial evaluation procedure for logic programs. In S. Debray and M. Hermenegildo, editors, Proceedings NACLP'90, pages 343{358, Austin, Texas, October 1990. MIT Press.
- R. Bol. Loop checking in partial deduction. Journal of Logic Programming, 16(1&2):25{ 46, 1993.
- M. Bruynooghe, D. De Schreye, and B. Martens. A general criterion for avoiding in nite unfolding during partial deduction. New Generation Computing, 11(1):47{79, 1992.
- C. Consel and O. Danvy. Tutorial notes on partial evaluation. In Proceedings POPL'93, Charleston, South Carolina, January 1993. ACM.
- D. A. de Waal and J. Gallagher. The applicability of logic program analysis and transfor- mation to theorem proving. In A. Bundy, editor, Proceedings CADE-12, pages 207{221, Nancy, France, June/July 1994. Springer-Verlag, LNAI 814.
- N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communi- cations of the ACM, 22(8):465{476, 1979.
- M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.
- J. Gallagher. Specialisation of logic programs: A tutorial. In Proceedings PEPM'93, ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Ma- nipulation, pages 88{98, Copenhagen, June 1993. ACM Press.
- J. Gallagher and M. Bruynooghe. Some low-level source transformations for logic pro- grams. In M. Bruynooghe, editor, Proceedings Meta'90, pages 229{244, Leuven, April 1990.
- R. Gl uck and M. H. Srensen. Driving and partial deduction are equivalent. In M. Hermenegildo and J. Penjam, editors, Proceedings PLILP'94, pages 165{181, Madrid, Spain, 1994. Springer-Verlag, LNCS 844.
- N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.
- J. Komorowski. A Speci cation of an Abstract Prolog Machine and its Application to Partial Evaluation. PhD thesis, Department of Computer and Information Science, Link oping University, Link oping, Sweden, 1981.
- J. Komorowski. An introduction to partial deduction. In A. Pettorossi, editor, Proceed- ings Meta'92, pages 49{69. Springer-Verlag, LNCS 649, 1992.
- P. Kursawe. Pure partial evaluation and instantiation. In D. Bjrner, A. P. Ershov, and N. D. Jones, editors, Partial Evaluation and Mixed Computation, pages 279{290. North-Holland, 1988.
- M. Leuschel. Partial evaluation of the \real thing". In F. Turini, editor, Proceedings LOPSTR'94. Springer-Verlag, Workshops in Computing Series, 1995.
- J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.
- J. W. Lloyd and J. C. Shepherdson. Partial evaluation in logic programming. Journal of Logic Programming, 11(3&4):217{242, 1991.
- B. Martens. On the Semantics of Meta-Programming and the Control of Partial De- duction in Logic Programming. PhD thesis, Departement Computerwetenschappen, K.U.Leuven, Belgium, February 1994.
- B. Martens, D. De Schreye, and T. Horv ath. Sound and complete partial deduction with unfolding based on well-founded measures. Theoretical Computer Science, 122(1-2):97{ 117, 1994.
- T. Mogensen and A. Bondorf. Logimix: A self-applicable partial evaluator for Prolog. In K.-K. Lau and T. Clement, editors, Proceedings LOPSTR'92, pages 214{227. Springer- Verlag, Workshops in Computing Series, 1993.
- A. Pettorossi and M. Proietti. Transformation of logic programs: Foundations and tech- niques. Journal of Logic Programming, 19/20:261{320, 1994.
- D. L. Poole and R. Goebel. Gracefully adding negation and disjunction to Prolog. In E. Shapiro, editor, Proceedings ICLP'86, pages 635{641, London, U.K., July 1986. Springer-Verlag, LNCS 225.
- S. Prestwich. Online partial deduction of large programs. In Proceedings PEPM'93, pages 111{118, Copenhagen, Denmark, June 1993. ACM.
- S. Safra. Partial evaluation of concurrent prolog and its implications. Technical Report Master's Thesis, CS86-24, Weizmann Institute, Department of Computer Science, 1986.
- D. Sahlin. Mixtus: An automatic partial evaluator for full Prolog. New Generation Computing, 12(1):7{51, 1993.
- M. H. Srensen, R. Gl uck, and N. D. Jones. Towards unifying partial evaluation, defor- estation, supercompilation, and GPC. In D. Sanella, editor, Proceedings ESOP'94, pages 485{500, Edinburgh, U.K., April 1994. Springer-Verlag, LNCS 788.
- L. Sterling and R. D. Beer. Meta interpreters for expert system construction. Journal of Logic Programming, 6(1&2):163{178, 1989.
- A. Takeuchi and K. Furukawa. Partial evaluation of Prolog programs and its application to metaprogramming. In H.-J. Kugler, editor, Information Processing 86, pages 415{420, 1986.
- V. F. Turchin. The concept of a supercompiler. ACM Transactions on Programming Languages and Systems, 8(3):292{325, 1986.
- V. F. Turchin. The algorithm of generalization in the supercompiler. In D. Bjrner, A. P. Ershov, and N. D. Jones, editors, Partial Evaluation and Mixed Computation, pages 531{549. North-Holland, 1988.
- D. Weise, R. Conybeare, E. Ruf, and S. Seligman. Automatic online partial evaluation. In J. Hughes, editor, Proceedings of the 3rd ACM Conference on Functional Programming Languages and Computer Architecture, pages 165{191, Cambridge, Massachusets, USA, August 1991. Springer-Verlag, LNCS 523.
Cited by
Sorted by citations
Controlling generalization and polyvariance in partial deduction of normal logic programs
Leuschel, M., Martens, B., & De Schreye, D. (1998) · ACM Transactions on Programming Languages and Systems · doi:10.1145/271510.271525 · Cited by 88
Self-citationNarrowing-driven partial evaluation of functional logic programs
Alpuente, M., Falaschi, M., & Vidal, G. (1996) · Lecture Notes in Computer Science · doi:10.1007/3-540-61055-3_28 · Cited by 40
Efficiently generating efficient generating extensions in prolog
Jørgensen, J., & Leuschel, M. (1996) · Lecture Notes in Computer Science · doi:10.1007/3-540-61580-6_12 · Cited by 26
Metadata
- Authors
- Martens, B., & Gallagher, J.
- Affiliations
- University of Bristol (GB)
- Corresponding author
- Gallagher, John
- ORCID
- Gallagher, John
- Venue
- Logic Programming
- Publisher
- The MIT Press
- Published
- 1995-06-16
- Pages
- 597-612
- OpenAlex
- W1530237295
- Cited by
- 69
- References
- 0
- Citations by year
- 2023: 1 · 2022: 1 · 2021: 2 · 2019: 3 · 2015: 2 · 2012: 2
- FWCI
- 23.74
- Type
- book chapter
- Language
- en
- Open access
- green
- lirias.kuleuven.be
- Licence
- other-oa
- Locations
- The MIT Press eBooks (publishedVersion)
- Lirias (submittedVersion, other-oa)
- Bristol Research (University of Bristol) (submittedVersion)
- Topics
- Physical Sciences › Computer Science › Software › Logic, programming, and type systems
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Advanced Algebra and Logic
- Keywords
- partial deduction, logic programs, well-founded orderings, tree structure
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
