一句话：为带绑定语法和规则系统提出通用强规则归纳准则，支持 Barendregt 变量约定并覆盖无穷语法。
本文研究带绑定语法（如 λ 演算和逻辑系统）的元理论，旨在为归纳定义的规则系统提供一种通用规则归纳原理，使证明可以利用 Barendregt 变量约定，即保持绑定变量与自由变量不相交。方法上，作者采用 Knaster–Tarski 不动点式的定义，而非强加句法格式，从而获得更高的一般性；该准则无需修改即可刻画感兴趣的系统，并能处理无穷语法与非等变谓词。结果是为此类系统建立更强的归纳证明工具，扩展了现有工作适用范围，并统一了若干此前需特殊处理的场景。
This paper is a contribution to the meta-theory of systems featuring syntax with bindings, such as λ-calculi and logics. It provides a general criterion that targets inductively defined rule-based systems , enabling for them inductive proofs that leverage Barendregt’s variable convention of keeping the bound and free variables disjoint. It improves on the state of the art by (1) achieving high generality in the style of Knaster-Tarski fixed point definitions (as opposed to imposing syntactic formats), (2) capturing systems of interest without modifications, and (3) accommodating infinitary syntax and non-equivariant predicates.
@article{BruggeMPT25,
title = {Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings},
author = {Jan van Brügge and James McKinna and Andrei Popescu and Dmitriy Traytel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704893}
}