论文标题
超越符号：定理的卫生宏扩展证明语言
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
论文作者
论文摘要
在交互式定理掠夺（ITP）中，可扩展的语法不仅对于降低操纵复杂数学对象的认知负担至关重要，而且在开发库中可重复使用的抽象方面起着至关重要的作用。大多数ITP以限制性的“语法糖”取代和其他临时机制的形式支持这种扩展，这些机制太基本了，无法支持许多理想的抽象。结果，图书馆充满了不必要的冗余。这些系统中的战术语言困扰着一个看似无关的问题：意外的名称捕获，通常会产生意想不到的违反直觉行为。我们从计划系列的计划家族中获取想法，并通过为ITP提出一种新颖的卫生宏观系统来同时解决这两个问题。我们进一步描述了如何扩展我们的方法以涵盖类型定向的宏观扩展，从而产生了一个均匀的系统，其提供了多个抽象水平，从支持最简单的语法糖到详细说明以前的烘焙语法。我们已经实现了新的宏系统，并将其集成到了精益定理供惯用者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.
