Formalization and abstract implementation of rewriting with nested rules

ABSTRACT

This paper formalizes term rewriting systems (TRSs), called scoped, in which a rewrite rule can be nested within another rewrite rule. The right-hand side and/or the condition of a nested rule can refer to any variable in the left-hand side of a nesting rule. Nesting of rewrite rules is intended to define a lexical scope with static binding. Our work is applicable to programming languages in which programs are modeled by TRSs and computations are executed by rewriting or narrowing. In particular, we consider a class of non-confluent and non-terminating TRSs well suited for modeling modern functional logic programs. We describe an abstract implementation of rewriting and narrowing for scoped TRSs to show that scopes can be easily handled irrespective of the evaluation strategy. The efficiency of rewriting within a scoped TRS, measured using a narrowing virtual machine, is comparable to the efficiency of rewriting for non-scoped TRSs.

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. Evaluation strategies for functional logic programming. In B. Gramlich and S. Lucas, editors, Electronic Notes in Theoretical Computer Science, volume 57. Elsevier, 2001.
• 3: S. Antoy, M. Hanus, A. Tolmach, and J. Liu. Architecture of a virtual machine for functional logic computations. Preliminary draft, 2003. Available at http://www.cs.pdx.edu/~antoy/.
• 4: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
• 5: J. W. Klop , Marc Bezem , R. C. De Vrijer, Term Rewriting Systems, Cambridge University Press, New York, NY, 2001
• 6: P. Borovansky, C. Kirchner, H. Kirchner, P.-E. Moreau, and C. Ringeissen. An overview of ELAN. In C. Kirchner and H. Kirchner, editors, Electronic Notes in Theoretical Computer Science, volume 15. Elsevier, 2000.
• 7: G Boudol, Computational semantics of term rewriting systems, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 8: M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. The Maude 2.0 system. In R. Nieuwenhuis, editor, Rewriting Techniques and Applications (RTA 2003), number 2706 in Lecture Notes in Computer Science, pages 76--87. Springer-Verlag, June 2003.
• 9: Olivier Danvy , Ulrik P. Schultz, Lambda-dropping: transforming recursive equations into programs with block structure, Theoretical Computer Science, v.248 n.1-2, p.243-287, October 2000 [doi>10.1016/S0304-3975(00)00054-2 ]
• 10: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 11: M. Hanus, S. Antoy, M. Engelke, K. Höppner, J. Koj, P. Niederau, R. Sadre, and F. Steiner. PAKCS: The Portland Aachen Kiel Curry System, 2003.
• 12: M. Hanus (ed.). Curry: An integrated functional logic language (vers. 0.7.2). Available at http://www.informatik.uni-kiel.de/~curry, 2002.
• 13: Christoph M. Hoffmann , Michael J. O'Donnell, Pattern Matching in Trees, Journal of the ACM (JACM), v.29 n.1, p.68-95, Jan. 1982 [doi>10.1145/322290.322295]
• 14: 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, pages 395--443. MIT Press, Cambridge, MA, 1991.
• 15: Thomas Johnsson, Lambda lifting: transforming programs to recursive equations, Proc. of a conference on Functional programming languages and computer architecture, p.190-203, January 1985, Nancy, France
• 16: J. W. Klop, Term rewriting systems, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 17: Francisco Javier López-Fraguas , Jaime Sánchez Hernández, TOY: A Multiparadigm Declarative System, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, p.244-247, July 02-04, 1999
• 18: Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
• 19: Mark G. J. van den Brand , Arie van Deursen , Jan Heering , H. A. de Jong , Merijn de Jonge , Tobias Kuipers , Paul Klint , Leon Moonen , Pieter A. Olivier , Jeroen Scheerder , Jurgen J. Vinju , Eelco Visser , Joost Visser, The ASF+SDF Meta-environment: A Component-Based Language Development Environment, Proceedings of the 10th International Conference on Compiler Construction, p.365-370, April 02-06, 2001
• 20: E. Visser. Scoped dynamic rewrite rules. In M. van den Brand and R. Verma, editors, Electronic Notes in Theoretical Computer Science, volume 59. Elsevier, 2001.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems

General Terms:
Design, Languages, Theory

Keywords:
block structured, functional logic programming, narrowing, non-determinism, term rewriting systems