Sergio Antoy
Michael Hanus
ABSTRACT
Narrowing is the operational principle of languages that integrate functional and logic programming. We propose a notion of a needed narrowing step that, for inductively sequential rewrite systems, extends the Huet and Le´vy notion of a needed reduction step. We define a strategy, based on this notion, that computes only needed narrowing steps. Our strategy is sound and complete for a large class of rewrite systems, is optimal w.r.t. the cost measure that counts the number of distinct steps of a derivation, computes only independent unifiers, and is efficiently implemented by pattern matching.
- 1.S. Antoy. Definitional trees. In ALP'92, pages 143- 157. Springer LNCS 632, 1992. Google Scholar
- 2.S. Antoy. Lazy rewriting in logic programming. Technical Report 90-17, Rev~ 2, Portland State University, Portland, OR, 1992. (Submitted for publication).Google Scholar
- 3.S. Antoy, R. Echahed, and M. tIanus. A needed narrowing strategy. Technical report, MPI-I-93- 243, Max-Planck-Institut f/Jr Informatik, Saarbriicken, 1993.Google Scholar
- 4.H. Barendregt, M. van Eekelen, J. Glauert, R. Kenneway, and M. Sleep. Term graph rewriting. In PARLE'87, pages 141-158. Springer LNCS 259, 1987. Google ScholarDigital Library
- 5.M. Bellia and G. Levi. The relation between logic and functional languages: a survey. Journal of Logic Programming, 3(3):217-236, 1986. Google ScholarDigital Library
- 6.D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In ESOP-86, pages 119-132. Springer LNCS 213, 1986. Google Scholar
- 7.G. Boudol. Computational semantics of term rewriting systems. In M. Nivat and J. C. Reynolds, editors, Algebrazc methods in semantics, chapter 5. Cambridge University Press, Cambridge, UK, 1985. Google ScholarDigital Library
- 8.P. H. Cheong. Compiling lazy narrowing into Prolog. New Generation Computing, 1992. (to appear).Google Scholar
- 9.J. Darlington and Y. Guo. Narrowing and unification in functional programming- an evaluation mechanism for absolute set abstraction. In Proc. of the Conference on Rewriting Techniques and Applications, pages 92-108. Springer LNCS 355, 1989. Google ScholarDigital Library
- 10.D. DeGroot and G. Lindstrom, editors. Logic Programming, Functions, Relatzons, and Equations. Prentice Hall, 1986. Google ScholarDigital Library
- 11.N. Dershowitz and J. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243-320. North Holland, Amsterdam, 1990. Google ScholarDigital Library
- 12.R. Echahed. On completeness of narrowing strategies. In Proc. CAAP'88, pages 89-101. Springer LNCS 299, 1988. Google ScholarDigital Library
- 13.R. Echahed. Uniform narrowing strategies. In Proceedings of the Third International Conference on Algebraic and Logic Programming, pages 259-275, Volterra, Italy, September 1992. Google ScholarDigital Library
- 14.M. J. Fay. First-order unification in an equational theory, in Proc. 4th Workshop on Automated Deduction, pages 161-167, Austin (Texas), 1979. Academic Press.Google Scholar
- 15.L. Fribourg. SLOG: A logic programming language interpreter based on clausal superposition and rewriting. In Proc. IEEE Internal. Symposium on Logzc Programming, pages 172-184, Boston, 1985.Google Scholar
- 16.E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel LEAF: a logic plus functional language. The Journal of Computer and Syslem Sciences, 42:139-185, 1991. Google ScholarDigital Library
- 17.J. A. Goguen and J. Meseguer. Eqlog: Equality, types, and generic modules for logic programming. In D. DeGroot and G. Lindstrom, editors, Logzc Programming, Functzons, Relations, and Equations, pages 295-363. Prentice Hall, 1986.Google Scholar
- 18.W. Hans, R. Loogen, and S. Winkler. On the interaction of lazy evaluation and backtracking. In Proc. of the 4lh International Symposium on Programming Language Implementation and Logic Programmzng, pages 355-369. Springer LNCS 631, 1992. Google ScholarDigital Library
- 19.M. Hanus. Compiling logic programs with equality. In Proc. of the 2nd Int. Workshop on Programming Language Implementation and Logic Programmzng, pages 387-401. Springer LNCS 456, 1990. Google ScholarDigital Library
- 20.A. tterold. Narrowing techniques applied to idempotent unification. Technical Report SR-86-16, SEKI, 1986.Google Scholar
- 21.C. M. Hoffmann and M. J. O'Donnell. Implementation of an interpreter for abstract equations. In 111h A CM Symposzum on the Pmnciple of Programming Languages, Salt Lake City, 1984. Google ScholarDigital Library
- 22.S. HSlldobler. Foundations of Equational Logzc Programming. Springer LNCS 353, 1989. Google ScholarDigital Library
- 23.G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. JCSS, 25:239-266, 1982.Google ScholarCross Ref
- 24.G. Huet and J.-J. L~vy. Computations in orthogonal term rewrltln8 systems, in J.-L. Lassez and G. Plotkin, editors, Computatzonal log,c: essays ,n honour of Alan Rob,nson. MIT Press, Cambridge, MA, 1991. Previous version: Call by need computations in non-ambiguous linear term rewriting systems, Technical Report 359, INRIA, Le Chesnay, France, 1979.Google Scholar
- 25.J.-M. Hullot. Canonical forms and unification. In Proc. 5th Conference on Automated Deduclzon, pages 318-334. Springer LNCS 87, 1980. Google ScholarDigital Library
- 26.J. A. Jim~nez-Martln, J. Marifio-Carballo, and J. J. Moreno-Navarro. Efficient implementation of lazy narrowing into PROLOG. In LOPSTR'92, 1993. Previous version: Some Techniques for the Efficient Implementation of Lazy Narrowing, Technical Report-FIM.75/LyS/92, Facultad de Informatica, Universidad Politecnica de Madrid, 1992.Google Scholar
- 27.J. R. Kennaway. Sequential evaluation strategies for parallel-or and related reduction systems. Annals of Pure and Applzed Logic, 43:31-56, 1989.Google ScholarCross Ref
- 28.J. R. Kennaway. The specificity rule for lazy pattern-matching in ambiguous term rewrite systems. In Third European Symp. on Programming. pages 256-270, 1990. LNCS 432. Google ScholarDigital Library
- 29.J. W. Klop. Term Rewriting Systems. in S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Vol. H, pages 1-112. Oxford University Press, 1992. Previous version: Term rewriting systems, Technical Report CS-R9073, Stichting Mathematisch Centrum, Amsterdam, 1990.Google Scholar
- 30.J. W. Klop and A. Middeldorp. Sequentiality in orthogonal term rewriting systems. Journal of Symbolic Computatzon, pages 161-195, 1991. Previous version: Technical Report CS-R8932, Stichting Mathematisch Centrum, Amsterdam, The Netherlands, 1989. Google ScholarDigital Library
- 31.S. Krischer and A. Bockmayr. Detecting redundant narrowing derivations by the LSE-SL reducibility test. In Proc. RTA'91. Springer LNCS 488, 1991. Google ScholarDigital Library
- 32.R. Loogen, F. Lopez Fraguas, and M. Rodriguez Artalejo. A demand driven computation strategy for lazy narrowing. In Proc. of the 5th International Symposium on Programming Language Implementation and Logic Programmzng, pages 184- 200. Springer LNCS 714, 1993. Google ScholarDigital Library
- 33.L. Maranget. Optimal derivation in weak lambdacalculi and in orthogonal terms rewriting systems. In 171h Annual Syrup. on Pmnczples of Prog. Languagc~, page~ 255-269. ACM, 1990. Google ScholarDigital Library
- 34.A. Middeldorp, August 1993. Personal Communication.Google Scholar
- 35.A. Middeldorp and E. Hamoen. Counterexamples to completeness results for basic narrowing (extended abstract). In Proceedings of the Third Internatzonal Conference on Algebrazc and Logzc Programming, pages 244-258, Volterra, Italy, September 1992. Google ScholarDigital Library
- 36.J. J. Moreno-Navarro, H. Kuchen, R. Loogen, and M. Rodriguez-Artaiejo. Lazy narrowing in a graph machine. In Proc. Second International Conference on Algebraic and Logic Programmzng, pages 298- 317. Springer LNCS 463, 1990. Google ScholarDigital Library
- 37.J. J. Moreno-Navarro and M. Rodriguez-Artalejo. Logic programming with functions and predicates: The language BABEL. Journal of Logic Programruing, 12:191-223, 1992. Google ScholarDigital Library
- 38.W. Nutt, P. R~ty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7:295- 317, 1989. Google ScholarDigital Library
- 39.M. J. O'Donneli. Computing in Systems Described by Equations. Springer LNCS 58, 1977. Google ScholarDigital Library
- 40.M. J. O'Donnell. Equational Logic as a Programming Language. MIT Press, 1985. Google ScholarDigital Library
- 41.M. J. Oyamaguchi. Nv-sequentiality: A decidable condition for call-by-need computations in term rewriting systems. SIAM Journal on Computation, 22(1):114-135, 1993. Google ScholarDigital Library
- 42.P. Padawitz. Computzng in Horn Clause Theories, volume 16 of EATCS Monographs on Theoretical Computer Science. Springer, 1988. Google ScholarDigital Library
- 43.G.D. Plotkin. Building-in equational theories. Machine Intelligence, 7:73-90, 1972.Google Scholar
- 44.U. S. Reddy. Narrowing as the operational semantics of functional languages. In Proc. IEEE Internal. Symposium on Logzc Programming, pages 138-151, Boston, 1985.Google Scholar
- 45.R. C. Sekar and I. V. Ramakrishnan. Programming in equational logic: Beyond strong sequentiality. In Proceedings of the Fzflh Annual IEEE Symposium on Logic in Computer Science, pages 230-241, Philadelphia, PA, June 1990.Google ScholarCross Ref
- 46.J. R. SIagie. Automated theorem-proving for theories with simplifiers, commutativity, and associativity. Journal of the A CM, 21(4):622-642, 1974. Google ScholarDigital Library
- 47.M. R. Sleep, M. J. Plasmeijer, and M. C. J. D. van Eekelen, editors. Term Graph Rewriting Theory and Practice. J. Wiley & Sons, Chichester, UK, 1993. Google ScholarDigital Library
- 48.S. Thatte. A refinement of strong sequentiality for term rewriting with constructors. Information and Computation, 72:46-65, 1987. Google ScholarDigital Library
- 49.J.-H. You. Enumerating outer narrowing derivations for constructor-based term rewriting systems. Journal of Symbolic Computation, 7:319-341, 1989. Google ScholarDigital Library
Index Terms
- A needed narrowing strategy
Recommendations
A needed narrowing strategy
The narrowing relation over terms constitutes the basis of the most important operational semantics of languages that integrate functional and logic programming paradigms. It also plays an important role in the definition of some algorithms of ...
Refining weakly outermost-needed rewriting and narrowing
PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programmingOutermost-needed rewriting/narrowing is a sound and complete optimal demand-driven strategy for the class of inductively sequential constructor systems. Its parallel extension (known as weakly) deals with non-inductively sequential constructor systems. ...
Leftmost outside-in narrowing calculi
We present narrowing calculi that are computation models of functional-logic programming languages. The narrowing calculi are based on the notion of the leftmost outside-in reduction of Huet and Lévy. We note the correspondence between the narrowing and ...
Comments