论文标题
代数重写系统的汇合
Confluence of algebraic rewriting systems
论文作者
论文摘要
代数结构上的收敛重写系统提供了解决决策问题，证明连贯结果并计算同源不变的方法。这些方法基于关键分支引理的较高维度扩展，该扩展证明了关键分支的汇合处证明局部汇合。在代数结构（例如组或线性代数）上重写系统的局部汇合的分析由于基础代数公理而变得复杂。本文介绍了代数测谎仪模量的结构，该模量正式化了代数重写系统规则与固有的代数公理之间的相互作用，我们显示了代数聚集器的关键分支引理。我们推断出在代数模型上重写系统的关键分支引理，其公理由收敛模型重写系统指定。我们说明了字符串，线性和组重写系统的构造。
Convergent rewriting systems on algebraic structures give methods to solve decision problems, to prove coherence results, and to compute homological invariants. These methods are based on higher-dimensional extensions of the critical branching lemma that proves local confluence from confluence of the critical branchings. The analysis of local confluence of rewriting systems on algebraic structures, such as groups or linear algebras, is complicated because of the underlying algebraic axioms. This article introduces the structure of algebraic polygraph modulo that formalizes the interaction between the rules of an algebraic rewriting system and the inherent algebraic axioms, and we show a critical branching lemma for algebraic polygraphs. We deduce a critical branching lemma for rewriting systems on algebraic models whose axioms are specified by convergent modulo rewriting systems. We illustrate our constructions for string, linear, and group rewriting systems.
