Recently, Gavazzo has developed a relational theory of symbolic manipulation, that allows to study syntax-based rewriting systems without relying on specific notions of syntax. This theory was obtained by extending the algebra of relations with syntax-inspired operators. Within the algebras thus obtained, it is possible to encode notions of parallel and full reduction for first-order rewriting systems, as well as to prove nontrivial properties about them in an algebraic and syntax-independent fashion. Sequential reduction, however, was not explored, but it was conjectured that it could be studied through a differential relational theory of rewriting. This manuscript proves the above conjecture by defining differential algebras of term relations, viz. algebras of term relations extended with novel operators inspired by the theory of functor derivatives. We give a set of axioms and rules for such operators and show that the resulting theory is expressive enough to define notions of parallel, full, and sequential reduction. We prove fundamental results relating all these notions in a purely algebraic and syntax-independent way, and showcase the effectiveness of our theory by proving the soundness of a proof technique for weak confluence akin to the so-called Critical Pair Lemma.

翻译：最近，Gavazzo发展了一种符号操作的关联理论，该理论允许在不依赖具体语法概念的情况下研究基于语法的重写系统。这一理论通过将关系代数扩展为受语法启发的算子而建立。在由此获得的代数中，可以编码一阶重写系统的并行归约和完全归约概念，并以代数且独立于语法的方式证明其非平凡性质。然而，序列归约尚未被探索，但曾有猜想认为可通过重写的微分关联理论加以研究。本文通过定义项关系的微分代数（即项关系的代数扩展了受函子导数理论启发的新算子）证明了上述猜想。我们为这些算子给出公理和规则集，并表明由此产生的理论具有足够的表达能力以定义并行、完全和序列归约概念。我们以纯代数和独立于语法的方式证明了联系所有这些概念的基本结果，并通过证明弱合流性证明技术（类似于所谓的临界对引理）的可靠性，展示了我们理论的有效性。