Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems
Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems
复制标题
左线性标称重写系统的并行闭包定理
DOI：
10.1007/978-3-319-66167-4_7
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Takahito Aoto and Yoshihito Toyama
中科院分区：
文献类型：
--
作者：
Kentaro Kikuchi;Takahito Aoto and Yoshihito Toyama
名义重写是一阶项重写的扩展，通过基于名义方法的绑定机制引入。在本文中，我们推广Huet的并行闭包定理及其推广的左线性项重写系统的合流的情况下，名义重写。该定理的证明遵循之前的正交均匀标称重写系统的归纳汇合证明，但临界对的存在需要一个更微妙的论点。结果包括左线性统一名义重写系统的不稳定，因此不表示在传统的高阶重写框架中的任何系统的汇合。
Nominal rewriting has been introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. In this paper, we extend Huet’s parallel closure theorem and its generalisation on confluence of left-linear term rewriting systems to the case of nominal rewriting. The proof of the theorem follows a previous inductive confluence proof for orthogonal uniform nominal rewriting systems, but the presence of critical pairs requires a much more delicate argument. The results include confluence of left-linear uniform nominal rewriting systems that are not-stable and thus are not represented by any systems in traditional higher-order rewriting frameworks.