抽象重写内化
Abstract rewriting internalized
摘要：
在传统的重写理论中，人们研究的是一组项到一组重写关系。在代数重写中，人们转而研究项的向量空间，直到关系的向量空间。引人注目的是，虽然这两个理论非常相似，但大多数结果（如纽曼引理）在这两种情况下需要不同的证明。在本文中，我们发展重写理论内部的一个范畴$\mathcal C$满足一些温和的性质。在这个一般的设置中，我们定义的概念，终止，局部合流和合流使用的概念，减少战略，并证明了一个类似的纽曼引理。在$\mathcal C= \operatorname{Set}$或$\mathcal C = \operatorname{Vect}$的情况下，我们恢复了抽象和代数重写的经典结果，在一个稍微更一般的形式，更接近于冯奥斯特罗姆的概念减少图。
英文摘要：
In traditional rewriting theory, one studies a set of terms up to a set of rewriting relations. In algebraic rewriting, one instead studies a vector space of terms, up to a vector space of relations. Strikingly, although both theories are very similar, most results (such as Newman's Lemma) require different proofs in these two settings. In this paper, we develop rewriting theory internally to a category $\mathcal C$ satisfying some mild properties. In this general setting, we define the notions of termination, local confluence and confluence using the notion of reduction strategy, and prove an analogue of Newman's Lemma. In the case of $\mathcal C= \operatorname{Set}$ or $\mathcal C = \operatorname{Vect}$ we recover classical results of abstract and algebraic rewriting in a slightly more general form, closer to von Oostrom's notion of decreasing diagrams.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
