Moving from the mathematical theory of (abstract) syntax, we develop a general relational theory of symbolic manipulation parametric with respect to, and accounting for, general notions of syntax. We model syntax relying on categorical notions, such as free algebras and monads, and show that a general theory of symbolic manipulation in the style of rewriting systems can be obtained by extending such notions to an allegorical setting. This way, we obtain an augmented calculus of relations accounting for syntax-based rewriting. We witness the effectiveness of the relational approach by generalising and unifying milestones results in rewriting, such as the parallel moves and the Tait-Martin-L\"of techniques.
翻译:从(抽象)语法的数学理论出发,我们发展了一种通用的符号操作关系理论,该理论对一般语法概念具有参数化特性并予以解释。我们依赖自由代数和单子等范畴论概念为语法建模,并证明通过将此类概念扩展至讽喻框架,可构建出重写系统风格的符号操作通用理论。由此,我们获得了一个能涵盖基于语法重写的增强关系演算。通过概括并统一重写领域的里程碑式成果——如平行移动和泰特-马丁-勒夫技术——我们验证了关系方法的有效性。