Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting
Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting
复制标题
标称重写中的接地合流和强换向模 Alpha 等价
DOI：
10.1007/978-3-031-17715-6_17
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Kentaro Kikuchi
中科院分区：
文献类型：
--
作者：
可児冬弥;瀬戸信明;市原英行;岩垣剛;井上智生;Kentaro Kikuchi
名义重写作为一阶项重写的扩展，通过基于名义方法的绑定机制引入。名词性重写的一个显著特点是，对等不是在元层次上隐式处理，而是在对象层次上显式处理。本文引入了强对易模等价的概念，给出了强对易模等价的一个充分条件，并利用该条件给出了可能非终止左线性名义重写系统（在基项上）模等价的一个新的判定准则.
Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. A distinctive feature of nominal rewriting is that-equivalence is not implicitly dealt with at the meta-level but explicitly dealt with at the object-level. In this paper, we introduce the notion of strong commutation modulo-equivalence and give a sufficient condition for it. Using the condition, we present a new criterion for confluence modulo-equivalence (on ground terms) of possibly non-terminating left-linear nominal rewriting systems.