Nominal rewriting systems

ABSTRACT

We present a generalisation of first-order rewriting which allows us to deal with terms involving binding operations in an elegant and practical way. We use a nominal approach to binding, in which bound entities are explicitly named (rather than using a nameless syntax such as de Bruijn indices), yet we get a rewriting formalism which respects α-conversion and can be directly implemented. This is achieved by adapting to the rewriting framework the powerful techniques developed by Pitts et al. in the FreshML project.Nominal rewriting can be seen as higher-order rewriting with a first-order syntax and built-in α-conversion. We show that standard (first-order) rewriting is a particular case of nominal rewriting, and that very expressive higher-order systems such as Klop's Combinatory Reduction Systems can be easily defined as nominal rewriting systems. Finally we study confluence properties of nominal rewriting.

REFERENCES

• 1: M. Abadi, L. Cardelli, P-L. Curien, and J-J. Lévy, Explicit substitutions, Journal of Functional Programming (1991), no. 4, 375--416.
• 2: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
• 3: Franco Barbanera , Maribel Fernández , Herman Geuvers, Modularity of strong normalization in the algebraic-λ-cube, Journal of Functional Programming, v.7 n.6, p.613-660, November 1997 [doi>10.1017/S095679689700289X]
• 4: H. P. Barendregt, Pairing without conventional constraints, Zeitschrift für mathematischen Logik und Grundlagen der Mathematik (1974), 289--306.
• 5: C. Bertolissi, H. Cirstea, and C. Kirchner, Translating combinatory reduction systems into the rewriting calculus, 4th International Workshop on Rule-Based Programming (RULE 2003), Valencia, Spain, 2003.
• 6: Eduardo Bonelli , Delia Kesner , Alejandro Ríos, From Higher-Order to First-Order Rewriting, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, p.47-62, May 22-24, 2001
• 7: Val Breazu-Tannen , Jean Gallier, Polymorphic rewriting conserves algebraic strong normalization, Theoretical Computer Science, v.83 n.1, p.3-28, June 21, 1991
• 8: V. Breazu-Tannen and J. Gallier, Polymorphic rewriting conserves algebraic confluence, Information and Computation (1992), 3--28.
• 9: J. Cheney, The complexity of equivariant unification. Proceedings of ICALP 2004, to appear.
• 10: H. Cirstea and C. Kirchner, The Rewriting Calculus - Part I, Logic Journal of the Interest Group in Pure and Applied Logics (2001), 363--399.
• 11: H. Cirstea and C. Kirchner, The Rewriting Calculus - Part II, Logic Journal of the Interest Group in Pure and Applied Logics (2001), 401--434.
• 12: René David , Bruno Guillaume, A λ-calculus with explicit weakening and explicit substitution, Mathematical Structures in Computer Science, v.11 n.1, p.169-206, February 2001 [doi>10.1017/S0960129500003224]
• 13: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 14: M. J. Gabbay, The π-calculus in FM, Thirty-five years of Automath (Fairouz Kamareddine, ed.), Kluwer, 2003.
• 15: M. J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing, pp. 341--363, 2002. A preliminary version appeared in the Proc. LICS 1999.
• 16: M. J. Gabbay, Fresh graphs, Submitted, November 2003.
• 17: Makoto Hamana, Term rewriting with variable binding: an initial algebra approach, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.148-159, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888266]
• 18: J.-P. Jouannaud and C. Kirchner, Solving equations in abstract algebras: a rule based survey of unification, Computational Logic: Essays in Honor of Alan Robinson (J-L. Lassez and G. Plotkin, eds.), MIT Press, 1991.
• 19: Jean-Pierre Jouannaud, Executable higher-order algebraic specifications, Proceedings of the 8th annual symposium on Theoretical aspects of computer science, p.16-25, February 1991, Hamburg, Germany
• 20: Z. Khasidashvili and V. van Oostrom, Context-sensitive conditional reduction systems, Electronic Notes in Theoretical Computer Science, Proc. SEGRAGRA'95 (1995).
• 21: Z. Khasidashvili, Expression reduction systems, Proceedings of I.Vekua Institute of Applied Mathematics (Tbisili), vol. 36, 1990, pp. 200--220.
• 22: Jan Willem Klop , Vincent van Oostrom , Femke van Raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, v.121 n.1-2, p.279-308, Dec. 6, 1993 [doi>10.1016/0304-3975(93)90091-7]
• 23: J-W. Klop, Combinatory reduction systems, Mathematical Centre Tracts, vol. 127, Mathematischen Centrum, 413 Kruislaan, Amsterdam, 1980.
• 24: Pierre Lescanne, From λσ to λν: a journey through calculi of explicit substitutions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-69, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.174707]
• 25: Richard Mayr , Tobias Nipkow, Higher-order rewrite systems and their confluence, Theoretical Computer Science, v.192 n.1, p.3-29, Feb. 10, 1998 [doi>10.1016/S0304-3975(97)00143-6]
• 26: Dale Miller , Alwen Tiu, A Proof Theory for Generic Judgments: An extended abstract, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.118, June 22-25, 2003
• 27: M.H.A. Newman, On theories with a combinatorial definition of equivalence, Annals of Mathematics (1942), no. 2, 223--243.
• 28: B. Pagano, Des calculs de substitution explicite et de leur application à la compilation des langages fonctionnels, Ph.D. thesis, Université de Paris 6, 1998.
• 29: Andrew M. Pitts, Nominal Logic: A First Order Theory of Names and Binding, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.219-242, October 29-31, 2001
• 30: Andrew M. Pitts , Murdoch Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.230-255, July 03-05, 2000
• 31: F. van Raamsdonk, Confluence and normalisation for higher-order rewriting, Ph.D. thesis, Free University of Amsterdam, 1996.
• 32: Mark R. Shinwell , Andrew M. Pitts , Murdoch J. Gabbay, FreshML: programming with binders made simple, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.263-274, August 25-29, 2003, Uppsala, Sweden
• 33: C. Urban, A. M. Pitts, and M. J. Gabbay, Nominal unification, Computer Science Logic and 8th Kurt Gödel Colloquium (CSL'03 & KGC), Vienna, Austria. Proccedings (M. Baaz, ed.), Lecture Notes in Computer Science, vol. 2803, Springer-Verlag, 2003, pp. 513--527.
• 34: C. Urban, Nominal matching, preliminary report, 2004.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Theory

Keywords:
α-conversion, binders, first and higher-order rewriting