超越记号：定理证明语言中的卫生宏展开
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
AI总结：
针对定理证明器中语法扩展不足与名称捕获问题，借鉴Scheme提出卫生宏系统，统一支持多级抽象，已集成于Lean 4且易于移植。
摘要：
在交互式定理证明器（ITP）中，可扩展语法不仅对于降低操作复杂数学对象的认知负担至关重要，而且在开发库中可复用的抽象方面发挥着关键作用。大多数ITP以限制性的“语法糖”替换和其他临时机制的形式支持此类扩展，这些机制过于简陋，无法支持许多理想的抽象。因此，库中充斥着不必要的冗余。这些系统中的策略语言受到一个看似无关的问题的困扰：意外的名称捕获，这常常产生出乎意料且违反直觉的行为。我们从Scheme编程语言家族中汲取思想，通过提出一种专为ITP定制的新型卫生宏系统，同时解决这两个问题。我们进一步描述了如何将我们的方法扩展到覆盖类型导向的宏展开，从而形成一个统一的系统，提供从支持最简单的语法糖到精化先前内建语法的多个抽象层次。我们已实现新的宏系统，并将其集成到新版本的Lean定理证明器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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
