Checking Overlaps of Nominal Rewriting Rules

详细信息    查看全文

• 作者：Mauricio Ayala-Rincó ; n^a ; ¹ ; ^{ayala@unb.br" class="auth_mail" title="E-mail the corresponding author} ; Maribel Ferná ; ndez^b ; ² ; ^{maribel.fernandez@kcl.ac.uk" class="auth_mail" title="E-mail the corresponding author} ; Murdoch James Gabbay^c ; ; Ana Cristina Rocha-Oliveira^a ; ³ ; ^{anacrismarie@gmail.com" class="auth_mail" title="E-mail the corresponding author}
• 关键词：nominal syntax ; rewriting ; confluence ; binding
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2016
• 出版时间：11 July 2016
• 年：2016
• 卷：323
• 期：Complete
• 页码：39-56
• 全文大小：367 K

文摘

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.