论文标题
抽象重写内部化
Abstract rewriting internalized
论文作者
论文摘要
在传统的重写理论中，人们研究了一组术语，直到一组重写关系。在代数重写中，人们改为研究术语的矢量空间，直到关系的矢量空间。令人惊讶的是，尽管这两种理论都非常相似，但大多数结果（例如纽曼的引理）在这两个设置中都需要不同的证据。在本文中，我们内部开发了重写理论，可满足某些轻度属性的类别$ \ Mathcal C $。在这种一般环境中，我们使用还原策略的概念来定义终止，局部汇合和汇合的概念，并证明了纽曼引理的类似物。在$ \ Mathcal c = \ operatoTorname {set} $或$ \ mathcal c = \ operatatorName {vect} $的情况下，我们以稍微通用的形式恢复了摘要和代数重写的经典结果，更接近von oostrom的减少图的记录。
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.
