×

Checking overlaps of nominal rewriting rules. (English) Zbl 1401.68131

Benevides, Mario (ed.) et al., Proceedings of the 10th workshop on logical and semantic frameworks, with applications (LSFA 2015), Natal, Brazil, August 31 – September 1, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 323, 39-56 (2016).
Summary: Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators. In this paper, we give sufficient conditions for (local) confluence of closed nominal rewriting theories, based on the analysis of rule overlaps. More precisely, we show that closed nominal rewriting rules where all proper critical pairs are joinable are locally confluent. We also show how to refine the notion of rule overlap to derive confluence of the closed rewriting relation. The conditions that we define are easy to check using a nominal unification algorithm.
For the entire collection see [Zbl 1342.68007].

MSC:

68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader, F.; Nipkow, T., Term rewriting and all that (1998), Cambridge UP
[2] Calvès, C., Complexity and implementation of nominal algorithms (2010), King’s College: King’s College London, PhD thesis
[3] Calvès, C.; Fernández, M., Matching and alpha-equivalence check for nominal terms, J. Comput. Syst. Sci., 76, 5, 283-301 (2010) · Zbl 1206.68159
[4] Cheney, J., The complexity of equivariant unification, (Automata, Languages and Programming: 31st Int. Colloquium, ICALP 2004. Automata, Languages and Programming: 31st Int. Colloquium, ICALP 2004, LNCS, vol. 3142 (2004), Springer), 332-344 · Zbl 1098.03023
[6] Domínguez, J.; Fernández, M., Relating nominal and higher-order rewriting, (Mathematical Foundations of Computer Science 2014. Mathematical Foundations of Computer Science 2014, 39th Int. Symposium, MFCS 2014. Mathematical Foundations of Computer Science 2014. Mathematical Foundations of Computer Science 2014, 39th Int. Symposium, MFCS 2014, LNCS, vol. 8634 (2014), Springer), 244-255, Part I · Zbl 1425.68158
[7] Fernández, M.; Gabbay, M. J., Nominal rewriting, Information and Computation, 205, 6, 917-965 (June 2007)
[8] Fernández, M.; Gabbay, M. J., Closed nominal rewriting and efficiently computable nominal algebra equality, (Proc. 5th Int. Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010 (2010)), 37-51
[9] Fernández, M.; Rubio, A., Nominal Completion for Rewrite Systems with Binders, (Automata, Languages, and Programming. Automata, Languages, and Programming, LNCS, vol. 7392 (2012), Springer), 201-213 · Zbl 1367.68130
[10] Galdino, A. L.; Ayala-Rincón, M., A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem, J. Autom. Reasoning, 45, 3, 301-325 (2010) · Zbl 1207.68338
[11] Huet, G. P., Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems, J. of the ACM, 27, 4, 797-821 (October 1980)
[12] Klop, J.-W.; van Oostrom, V.; van Raamsdonk, F., Combinatory reduction systems, introduction and survey, Theoretical Computer Science, 121, 279-308 (1993) · Zbl 0796.03024
[13] Knuth, D.; Bendix, P., Simple word problems in universal algebras, (Computational Problems in Abstract Algebra (1970), Pergamon Press: Pergamon Press Oxford) · Zbl 0188.04902
[14] Mayr, R.; Nipkow, T., Higher-order rewrite systems and their confluence, Theoretical Computer Science, 192, 3-29 (1998) · Zbl 0895.68078
[15] Newman, M. H.A., On Theories with a Combinatorial Definition of “Equivalence”, The Annals of Mathematics, 43, 2, 223-243 (1942) · Zbl 0060.12501
[16] Rocha-Oliveira, A. C.; Ayala-Rincón, M., Formalizing the confluence of orthogonal rewriting systems, (Proc. 7th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012 (2012)), 145-152 · Zbl 1464.68144
[17] Rosen, B. K., Tree-manipulating systems and Church-Rosser theorems, J. of the ACM, 20, 1, 160-187 (January 1973)
[18] Stehr, M.-O., CINNI - A Generic Calculus of Explicit Substitutions and its Application to \(λ- ζ\)- and \(π\)-Calculi, The 3rd Int. Workshop on Rewriting Logic and its Applications. The 3rd Int. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, 36, 70-92 (2000)
[19] Suzuki, T.; Kikuchi, K.; Aoto, T.; Toyama, Y., Confluence of Orthogonal Nominal Rewriting Systems Revisited, (26th Int. Conf. on Rewriting Techniques and Applications (RTA 2015). 26th Int. Conf. on Rewriting Techniques and Applications (RTA 2015), LIPIcs, vol. 36 (2015)), 301-317 · Zbl 1366.68128
[20] Urban, C.; Pitts, A. M.; Gabbay, M., Nominal Unification, Theoretical Computer Science, 323, 1-3, 473-497 (2004) · Zbl 1078.68140
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.