paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Allegories of Symbolic Manipulations

符号操作的寓言(Allegory)理论
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 2/10 · 论文是范畴论/关系代数下的符号操作与重写系统理论,属于形式语义与证明工程的基础理论,未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与当前 PL+AI 交叉方向匹配度低。引用 1 inbox
Francesco Gavazzo
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出基于 allegory 与范畴语法的通用关系式符号操作理论,统一并行移动与 Tait–Martin-Löf 技术。

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

问题
如何为任意语法概念建立统一的符号操作与重写理论,并解释并行移动与 Tait–Martin-Löf 等经典重写结果。
方法
以自由代数、单子等范畴结构建模语法,并将其扩展到 allegory 设定,构造增强的关系演算来刻画基于语法的重写。
评估
通过推广和统一重写理论中的并行移动与 Tait–Martin-Löf 技术等里程碑结果来展示该理论的有效性。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{abs-2305-01772,
  title = {Allegories of Symbolic Manipulations},
  author = {Francesco Gavazzo},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175807}
}