一句话:提出基于 allegory 与范畴语法的通用关系式符号操作理论,统一并行移动与 Tait–Martin-Löf 技术。
本文从抽象语法的数学理论出发,建立一种参数化于一般语法概念的通用关系式符号操作理论。作者用自由代数、单子等范畴概念刻画语法,并将这些概念提升到 allegory(寓言范畴)框架,从而得到一种可表达基于语法的重写的增强关系演算。该关系视角能够推广并统一重写理论中的若干里程碑结果,例如并行移动(parallel moves)与 Tait–Martin-Löf 技术,展示其在符号计算与归约分析中的有效性。
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öf techniques.