论文标题
表格分辨率
Tabled Typeclass Resolution
论文作者
论文摘要
Typecers提供了一种优雅有效的方法，可以在编程语言和交互式证明助手中管理临时多态性。但是，在证明助手中，越来越复杂的用途越来越复杂，尤其是在Lean迅速发展的数学库Mathlib中，对现有Typeclass分辨率程序的一度理论局限性升高到了持续进展的主要障碍中。现有过程的两个最具破坏性的局限性是在存在循环的情况下存在钻石和分歧的情况下指数运行时间。我们提出了一个新的程序，即列出的类型分辨率，该程序通过调查解决了这两个问题，这是对最初引入的记忆的概括，以解决早期逻辑编程系统的类似局限性。我们已经为LEN的即将到来的版本（V4）实施了程序，并从经验上确认，在存在钻石的情况下，我们的实施速度比现有系统要快。尽管众所周知，很难实施调整，但我们的程序非常轻巧，可以轻松地在其他系统中实施。我们希望我们的新程序有助于在软件开发和交互式定理证明中更复杂的类型使用。
Typeclasses provide an elegant and effective way of managing ad-hoc polymorphism in both programming languages and interactive proof assistants. However, the increasingly sophisticated uses of typeclasses within proof assistants, especially within Lean's burgeoning mathematics library, mathlib, have elevated once-theoretical limitations of existing typeclass resolution procedures into major impediments to ongoing progress. The two most devastating limitations of existing procedures are exponential running times in the presence of diamonds and divergence in the presence of cycles. We present a new procedure, tabled typeclass resolution, that solves both problems by tabling, which is a generalization of memoizing originally introduced to address similar limitations of early logic programming systems. We have implemented our procedure for the upcoming version (v4) of Lean, and have confirmed empirically that our implementation is exponentially faster than existing systems in the presence of diamonds. Although tabling is notoriously difficult to implement, our procedure is notably lightweight and could easily be implemented in other systems. We hope our new procedure facilitates even more sophisticated uses of typeclasses in both software development and interactive theorem proving.
