TY - JOUR
T1 - Checking Overlaps of Nominal Rewriting Rules
AU - Ayala-Rincón, Mauricio
AU - Fernández, Maribel
AU - Gabbay, Jamie
AU - Rocha-Oliveira, Ana Cristina
PY - 2016/7/11
Y1 - 2016/7/11
N2 - 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.
AB - 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.
U2 - 10.1016/j.entcs.2016.06.004
DO - 10.1016/j.entcs.2016.06.004
M3 - Article
SN - 1571-0661
VL - 323
SP - 39
EP - 56
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -