Constructor-based conditional narrowing

ABSTRACT

We define a transformation from a left-linear constructor-based conditional rewrite system into an overlapping inductively sequential rewrite system. This transformation is sound and complete for the computations in the source system. Since there exists a sound and complete narrowing strategy for the target system, the combination of these results offers the first procedure for provably sound and complete narrowing computations for the whole class of the leftlinear constructor-based conditional rewrite systems. We address the differences between demand driven and lazy strategies and between narrowing strategies and narrowing calculi. In this context, we analyze the efficiency and practicality of using our transformation for the implementation of functional logic programming languages. The results of this paper complement, extend, and occasionally rectify, previously published results in this area.

REFERENCES

• 1: S. Antoy. Non-determinism and lazy evaluation in logic programming. In T. P. Clement and K.-K. Lau, editors, Logic Programming Synthesis and Transformation (LOPSTR'91), pages 318--331, Manchester, UK, July 1991. Springer-Verlag.
• 2: Sergio Antoy, Definitional Trees, Proceedings of the Third International Conference on Algebraic and Logic Programming, p.143-157, September 02-04, 1992
• 3: Sergio Antoy, Optimal Non-deterministic Functional Logic Computations, Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming, p.16-30, September 03-05, 1997
• 4: S. Antoy, R. Echahed, and M. Hanus. Parallel evaluation strategies for functional logic languages. In Proc. of the Fourteenth International Conference on Logic Programming (ICLP'97), pages 138--152. MIT Press, 1997.
• 5: Sergio Antoy , Rachid Echahed , Michael Hanus, A needed narrowing strategy, Journal of the ACM (JACM), v.47 n.4, p.776-822, July 2000 [doi>10.1145/347476.347484]
• 6: Sergio Antoy , Bart Massey , Michael Hanus , Frank Steiner, An implementation of narrowing strategies, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.207-217, September 05-07, 2001, Florence, Italy [doi>10.1145/773184.773206]
• 7: Sergio Antoy , Aart Middeldorp, A sequential reduction strategy, Theoretical Computer Science, v.165 n.1, p.75-95, Sept. 30, 1996
• 8: J A Bergstra , J W Klop, Conditional rewrite rules: Confluence and termination, Journal of Computer and System Sciences, v.32 n.3, p.323-362, June 1986 [doi>10.1016/0022-0000(86)90033-4]
• 9: G Boudol, Computational semantics of term rewriting systems, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 10: 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]
• 11: J. C. González Moreno, F. J. López Fraguas, M. T. Hortalá González, and M. Rodríguez Artalejo. An approach to declarative programming based on a rewriting logic. The Journal of Logic Programming, 40:47--87, 1999.
• 12: M. Hanus. On extra variables in (equational) logic programming. In Proc. Twelfth International Conference on Logic Programming, pages 665--679. MIT Press, 1995.
• 13: Michael Hanus, A unified computation model for functional and logic programming, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.80-93, January 15-17, 1997, Paris, France [doi>10.1145/263699.263710]
• 14: Michael Hanus , Salvador Lucas , Aart Middeldorp, Strongly sequential and inductively sequential term rewriting systems, Information Processing Letters, v.67 n.1, p.1-8, July 16, 1998 [doi>10.1016/S0020-0190(98)00016-7]
• 15: G. Huet and J.-J. Lévy. Computations in orthogonal term rewriting systems. In J.-L. Lassez and G. Plotkin, editors, Computational logic: essays in honour of Alan Robinson. MIT Press, Cambridge, MA, 1991.
• 16: Tetsuo Ida , Koichi Nakahara, Leftmost outside-in narrowing calculi, Journal of Functional Programming, v.7 n.2, p.129-161, March 1997 [doi>10.1017/S0956796897002645]
• 17: 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
• 18: Massimo Marchiori, Unravelings and Ultra-properties, Proceedings of the 5th International Conference on Algebraic and Logic Programming, p.107-121, September 25-27, 1996
• 19: Aart Middeldorp , Satoshi Okui, A deterministic lazy narrowing calculus, Journal of Symbolic Computation, v.25 n.6, p.733-757, June 1998 [doi>10.1006/jsco.1997.0197]
• 20: Aart Middeldorp , Satoshi Okui , Tetsuo Ida, Lazy narrowing: strong completeness and eager variable elimination, Theoretical Computer Science, v.167 n.1-2, p.95-130, Oct. 30, 1996
• 21: Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
• 22: R. C. Sekar , I. V. Ramakrishnan, Programming in equational logic: beyond strong sequentiality, Information and Computation, v.104 n.1, p.78-109, May 1993 [doi>10.1006/inco.1993.1026]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.6 Logic Programming
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation
          Subjects: Simplification of expressions
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming

General Terms:
Algorithms, Languages, Performance, Theory

Keywords:
call-by-need, functional logic programming languags, narrowing strategies, rewrite systems