Commutative rational term rewriting
Commutative rational term rewriting
复制标题
可交换有理项重写
DOI：
10.1007/978-3-030-68195-1_15
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Takahito Aoto and Munehiro Iwami
中科院分区：
文献类型：
--
作者：
Mamoru Ishizuka;Takahito Aoto and Munehiro Iwami
有理项的项重写，即具有有限数量的不同子项的无限项，已经在Corradini & Gadducci（1998）和Aoto & Ketema（2012）中被考虑过。本文基于Aoto & Ketema（2012）的框架，考虑了通过一组交换性规则（即形式的规则）进行有理项重写。具有交换性规则的重写步骤通过redex位置的常规集合来指定，因此通过有限自动机。我们提出了一些有限的自动机结构，对应于（特别是）采取逆重写步骤，合并两个分支重写步骤，并合并两个连续的重写步骤。作为一个推论，我们表明，合理的重写步骤的交换规则下，采取等价的重写步骤是封闭的。
Term rewriting for rational terms, i.e. infinite terms with a finite number of different subterms, has been considered e.g. in Corradini & Gadducci (1998) and Aoto & Ketema (2012). In this paper, we consider rational term rewriting by a set of commutativity rules i.e. rules of the form, based on the framework of Aoto & Ketema (2012). A rewrite step with a commutativity rule is specified via a regular set of redex positions, thus via a finite automaton. We present some finite automata constructions that correspond to (in particular) taking inverse rewrite steps, merging two branching rewrite steps, and merging two consecutive rewrite steps. As a corollary, we show that rational rewrite steps by the commutativity rules are closed under taking equivalence of the rewrite steps.