Abstract
We design a completion procedure for nominal rewriting systems, based on a generalisation of the recursive path ordering to take into account alpha equivalence. Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators. Completion of rewriting systems with binders is a notably difficult problem; the completion procedure presented in this paper is the first to deal with binders in rewrite rules.
Partially supported by the Spanish MICINN under grant TIN 2010-21062-C02-01
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arts, T., Giesl, J.: Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236, 133–178 (2000)
Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Great Britain (1998)
Bachmair, L., Dershowitz, N., Hsiang, J.: Orderings for equational proofs. In: Proc. Symp. Logic in Computer Science, Boston, pp. 346–357 (1986)
Blanqui, F.: Termination and Confluence of Higher-Order Rewrite Systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 47–61. Springer, Heidelberg (2000)
Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion Without Failure. In: Ait-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol. 2, ch. 1. Academic Press, New York (1989)
Blanqui, F., Jouannaud, J.-P., Rubio, A.: The Computability Path Ordering: The End of a Quest. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 1–14. Springer, Heidelberg (2008)
Borralleras, C., Ferreira, M., Rubio, A.: Complete Monotonic Semantic Path Orderings. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 346–364. Springer, Heidelberg (2000)
Breazu-Tannen, V., Gallier, J.: Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science 83(1) (1991)
Calvès, C., Fernández, M.: Matching and Alpha-Equivalence Check for Nominal Terms. Journal of Computer and System Sciences, Special issue: Selected papers from WOLLIC 2008 (2009)
Cheney, J.: A Dependent Nominal Type Theory. Logical Methods in Computer Science 8(1) (2012)
Clouston, R.A., Pitts, A.M.: Nominal Equational Logic. In: Cardelli, L., Fiore, M., Winskel, G. (eds.) Computation, Meaning and Logic. Articles dedicated to Gordon Plotkin. Electronic Notes in Theoretical Computer Science, vol. 1496. Elsevier (2007)
Dershowitz, N.: Orderings for Term-Rewriting Systems. Theoretical Computer Science 17(3), 279–301 (1982)
Fernández, M., Gabbay, M.J.: Nominal rewriting. Information and Computation 205(6) (2007)
Fernández, M., Gabbay, M.J.: Closed nominal rewriting and efficiently computable nominal algebra equality. In: Proc. 5th Int. Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2010). EPTCS, vol. 34 (2010)
Fernández, M., Gabbay, M.J., Mackie, I.: Nominal rewriting systems. In: Proceedings of the 6th ACM-SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2004), Verona, Italy. ACM Press (2004)
Gabbay, M.J., Mathijssen, A.: Nominal universal algebra: equational logic with names and binding. Journal of Logic and Computation 19(6), 1455–1508 (2009)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2001)
Hamana, M.: Semantic Labelling for Proving Termination of Combinatory Reduction Systems. In: Escobar, S. (ed.) WFLP 2009. LNCS, vol. 5979, pp. 62–78. Springer, Heidelberg (2010)
Jouannaud, J.-P., Okada, M.: Executable higher-order algebraic specification languages. In: Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 350–361. IEEE Computer Society Press (1991)
Jouannaud, J.-P., Rubio, A.: Polymorphic Higher-Order Recursive Path Orderings. Journal of ACM 54(1) (2007)
Khasidashvili, Z.: Expression reduction systems. In: Proceedings of I. Vekua Institute of Applied Mathematics, Tbilisi, vol. 36, pp. 200–220 (1990)
Klop, J.-W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems, introduction and survey. Theoretical Computer Science 121, 279–308 (1993)
Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Kusakari, K., Chiba, Y.: A higher-order Knuth-Bendix procedure and its applications. IEICE Transactions on Information and Systems E90-D(4), 707–715 (2007)
Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science 192, 3–29 (1998)
Newman, M.H.A.: On theories with a combinatorial definition of equivalence. Annals of Mathematics 43(2), 223–243 (1942)
Nipkow, T., Prehofer, C.: Higher-Order Rewriting and Equational Reasoning. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction — A Basis for Applications. Volume I: Foundations. Applied Logic Series, vol. 8, pp. 399–430. Kluwer (1998)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)
Pitts, A.M.: Structural Recursion with Locally Scoped Names. Journal of Functional Programming 21(3), 235–286 (2011)
van de Pol, J.C.: Termination of higher-order rewrite systems. PhD thesis, Utrecht University, Utrecht, The Netherlands (December 1996)
Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)
Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoretical Computer Science 323, 473–497 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fernández, M., Rubio, A. (2012). Nominal Completion for Rewrite Systems with Binders. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds) Automata, Languages, and Programming. ICALP 2012. Lecture Notes in Computer Science, vol 7392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31585-5_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-31585-5_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31584-8
Online ISBN: 978-3-642-31585-5
eBook Packages: Computer ScienceComputer Science (R0)