A needed narrowing strategy

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.

REFERENCES

• 1: Sergio Antoy, Definitional Trees, Proceedings of the Third International Conference on Algebraic and Logic Programming, p.143-157, September 02-04, 1992
• 2: S. Antoy. Lazy rewriting in logic programming. Technical Report 90-17, Rev~ 2, Portland State University, Portland, OR, 1992. (Submitted for publication).
• 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.
• 4: H P Barendregt , M C J D Eekelen , J R W Glauert , J R Kennaway , M J Plasmeijer , M R Sleep, Term graph rewriting, Volume II: Parallel Languages on PARLE: Parallel Architectures and Languages Europe, p.141-158, March 1987, Eindhoven, The Netherlands
• 5: M Bellia , G Levi, The relation between logic and functional languages: A survey, Journal of Logic Programming, v.3 n.3, p.217-236, Oct. 1986 [doi>10.1016/0743-1066(86)90014-2]
• 6: D Bert , R Echahed, Design and implementation of a generic, logic and functional programming language, Proc. of the European symposium on programming on ESOP 86, p.119-132, March 1986, Saarbru:9Aicken, Germany
• 7: G Boudol, Computational semantics of term rewriting systems, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 8: P. H. Cheong. Compiling lazy narrowing into Prolog. New Generation Computing, 1992. (to appear).
• 9: J. Darlington , Y.-K. Guo, Narrowing and unification in functional programming mechanism for absolute set a bstraction, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.92-108, January 1989
• 10: Doug DeGroot , Gary Lindstrom, Logic programming: functions, relations, and equations, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 11: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 12: Rachid Echahed, On Comleteness of Narrowing Strategies, Proceedings of the 13th Colloquium on Trees in Algebra and Programming, p.89-101, March 21-24, 1988
• 13: Rachid Echahed, Uniform Narrowing Strategies, Proceedings of the Third International Conference on Algebraic and Logic Programming, p.259-275, September 02-04, 1992
• 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.
• 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.
• 16: Elio Giovannetti , Giorgio Levi , Corrado Moiso , Catuscia Palamidessi, Kernel-LEAF: a logic plus functional language, Journal of Computer and System Sciences, v.42 n.2, p.139-185, April 1991 [doi>10.1016/0022-0000(91)90009-T]
• 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.
• 18: Werner Hans , Rita Loogen , Stephan Winkler, On the Interaction of Lazy Evaluation and Backtracking, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.355-369, August 26-28, 1992
• 19: Michael Hanus, Compiling Logic Programs with Equality, Proceedings of the 2nd International Workshop on Programming Language Implementation and Logic Programming, p.387-400, August 20-22, 1990
• 20: A. tterold. Narrowing techniques applied to idempotent unification. Technical Report SR-86-16, SEKI, 1986.
• 21: Christoph M. Hoffmann , Michael J. O`Donnell, Implementation of an interpreter for abstract equations, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-121, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800522]
• 22: Steffen Hölldobler, Foundations of Equational Logic Programming, Springer-Verlag New York, Inc., New York, NY, 1989
• 23: G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. JCSS, 25:239-266, 1982.
• 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.
• 25: Jean-Marie Hullot, Canonical Forms and Unification, Proceedings of the 5th Conference on Automated Deduction, p.318-334, July 08-11, 1980
• 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.
• 27: J. R. Kennaway. Sequential evaluation strategies for parallel-or and related reduction systems. Annals of Pure and Applzed Logic, 43:31-56, 1989.
• 28: R. Kennaway, The specificity rule for lazy pattern-matching in ambiguous term rewrite systems, Proceedings of the third European symposium on programming on ESOP '90, p.256-270, May 1990, Copenhagen, Denmark
• 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.
• 30: J. W. Klop , A. Middeldorp, Sequentiality in orthogonal term rewriting systems, Journal of Symbolic Computation, v.12 n.2, p.161-195, Aug. 1991 [doi>10.1016/S0747-7171(08)80124-1]
• 31: Stefan Krischer , Alexander Bockmayr, Detecting redundant narrowing derivations by the LSE-SL reducibility test, Proceedings of the 4th international conference on Rewriting techniques and applications, p.74-85, March 1991, Como, Italy
• 32: Rita Loogen , Francisco Javier López-Fraguas , Mario Rodríguez-Artalejo, A Demand Driven Computation Strategy for Lazy Narrowing, Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, p.184-200, August 25-27, 1993
• 33: Luc Maranget, Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.255-269, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99618]
• 34: A. Middeldorp, August 1993. Personal Communication.
• 35: Aart Middeldorp , Erik Hamoen, Counterexamples to Completeness Results for Basic Narrowing (Extended Abstract), Proceedings of the Third International Conference on Algebraic and Logic Programming, p.244-258, September 02-04, 1992
• 36: Juan José Moreno-Navarro , Herbert Kuchen , Rita Loogen , Mario Rodríguez-Artalejo, Lazy Narrowing in a Graph Machine, Proceedings of the Second International Conference on Algebraic and Logic Programming, p.298-317, October 01-03, 1990
• 37: Juan Jose Moreno-Navarro , Mario Rodriguez-Artalejo, Logic programming with functions and predicates: the language Babel, Journal of Logic Programming, v.12 n.3, p.191-223, Feb. 1992 [doi>10.1016/0743-1066(92)90024-W]
• 38: Werner Nutt , Pierre Réty , Gert Smolka, Basic narrowing revisited, Journal of Symbolic Computation, v.7 n.3-4, p.295-317, March/April 1989 [doi>10.1016/S0747-7171(89)80014-8]
• 39: Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
• 40: Michael J. O'Donnell, Equational logic as a programming language, Massachusetts Institute of Technology, Cambridge, MA, 1985
• 41: Michio Oyamaguchi, NV-sequentiality: a decidable condition for call-by-need computations in term-rewriting systems, SIAM Journal on Computing, v.22 n.1, p.114-135, Feb. 1993 [doi>10.1137/0222010]
• 42: Peter Padawitz, Computing in Horn clause theories, Springer-Verlag New York, Inc., New York, NY, 1988
• 43: G.D. Plotkin. Building-in equational theories. Machine Intelligence, 7:73-90, 1972.
• 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.
• 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.
• 46: James R. Slagle, Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity, Journal of the ACM (JACM), v.21 n.4, p.622-642, Oct. 1974 [doi>10.1145/321850.321859]
• 47: M. R. Sleep , M. J. Plasmeijer , M. C. J. D. van Eekelen, Term graph rewriting: theory and practice, John Wiley and Sons Ltd., Chichester, UK, 1993
• 48: Satish Thatte, A refinement of strong sequentiality for term rewriting with constructors, Information and Computation, v.72 n.1, p.46-65, Jan. 1987 [doi>10.1016/0890-5401(87)90050-2]
• 49: Jia-Huai You, Enumerating outer narrowing derivations for constructor-based term rewriting systems, Journal of Symbolic Computation, v.7 n.3-4, p.319-341, March/April 1989 [doi>10.1016/S0747-7171(89)80015-X]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

General Terms:
Theory