超越符号：定理证明语言的卫生宏展开
摘要：交互式定理证明器（ITP）中的可扩展语法不仅对于降低操作复杂数学对象的认知负担至关重要，而且在开发可重用的库中起着至关重要的作用。大多数ITP支持以限制性的“语法糖”替换和其他临时机制形式的扩展，这些扩展过于简单，无法支持许多理想的抽象。因此，库中充斥着不必要的冗余。这些系统中的策略语言常常受到看似无关的问题的困扰：意外的名称捕获，这经常导致意外和反直觉的行为。我们借鉴了Scheme编程语言家族的思想，并通过提出一种专门为ITP定制的新型卫生宏系统同时解决了这两个问题。我们还描述了如何扩展我们的方法以涵盖基于类型的宏展开，从而提供一个统一的、多层次的系统，从支持最简单的语法糖到扩展先前内置语法的详细阐述。我们已经实现了我们的新宏系统，并将其整合到Lean定理证明器的新版本Lean 4中。尽管宏系统具有表达能力，但其简单性使其可以轻松地集成到其他系统中。
作者：Sebastian Ullrich and Leonardo de Moura
论文ID：2001.10490
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22