一句话：提出面向交互式定理证明器的卫生宏系统，同时解决意外名称捕获与语法扩展能力不足，并集成到 Lean 4。
交互式定理证明器中，可扩展语法对降低复杂数学对象操作负担和构建可复用库抽象至关重要。但多数系统仅支持受限的语法糖替换与临时机制，难以表达许多理想抽象，导致库中充斥冗余；其策略语言还常遭遇意外名称捕获，产生反直觉行为。本文借鉴 Scheme 的卫生宏思想，为 ITP 设计了一种新的卫生宏系统，同时解决上述两个问题。作者进一步将其扩展到类型导向的宏展开，从而用统一系统提供从简单语法糖到原先内建语法 elaboration 的多层次抽象。该系统已实现并集成到 Lean 4。尽管表达力强，其设计仍足够简单，便于集成到其他系统。
In interactive theorem provers (ITPs), extensible syntax is not only crucial to lower the cognitive burden of manipulating complex mathematical objects, but plays a critical role in developing reusable abstractions in libraries. Most ITPs support such extensions in the form of restrictive "syntax sugar" substitutions and other ad hoc mechanisms, which are too rudimentary to support many desirable abstractions. As a result, libraries are littered with unnecessary redundancy. Tactic languages in these systems are plagued by a seemingly unrelated issue: accidental name capture, which often produces unexpected and counterintuitive behavior. We take ideas from the Scheme family of programming languages and solve these two problems simultaneously by proposing a novel hygienic macro system custom-built for ITPs. We further describe how our approach can be extended to cover type-directed macro expansion resulting in a single, uniform system offering multiple abstraction levels that range from supporting simplest syntax sugars to elaboration of formerly baked-in syntax. We have implemented our new macro system and integrated it into the new version of the Lean theorem prover, Lean 4. Despite its expressivity, the macro system is simple enough that it can easily be integrated into other systems.
@article{paperbot1710,
title = {Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages},
author = {Sebastian Ullrich and Leonardo de Moura},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:1)2022}
}