一句话：为线性、仿射、相关和笛卡尔子结构下的带变量绑定抽象语法建立统一的范畴论，并刻画单变量替换。
本文针对带变量绑定的抽象语法，在交换、弱化、收缩及其组合所对应的线性、仿射、相关和笛卡尔四种上下文结构规则下，发展统一的范畴论理论。作者将抽象语法定义为变量上 binding-signature 自函子的自由代数，并给出替换律的有限代数公理化。在此基础上，通过广义结构递归统一构造避免捕获的单变量替换操作，证明其正确性，并证明所得结构具有初始替换代数的普遍抽象特征。该工作为不同子结构设置中的语法与替换提供统一语义框架。
We develop a unified categorical theory of substructural abstract syntax with variable binding and single-variable (capture-avoiding) substitution. This is done for the gamut of context structural rules given by exchange (linear theory) with weakening (affine theory) or with contraction (relevant theory) and with both (cartesian theory). Specifically, in all four scenarios, we uniformly: define abstract syntax with variable binding as free algebras for binding-signature endofunctors over variables; provide finitary algebraic axiomatisations of the laws of substitution; construct single-variable substitution operations by generalised structural recursion; and prove their correctness, establishing their universal abstract character as initial substitution algebras.
DOI 原文 ·
@inproceedings{paperbot8616,
title = {Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution},
author = {Marcelo Fiore and Sanjiv Ranchod},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00022}
}