从非直谓类型系统到直谓类型系统的证明翻译

由于形式化证明的开发是一项耗时的工作，设计共享已写好的证明的方法以防止重复劳动浪费时间十分重要。该领域的一个挑战是：当非直谓性未被本质性地使用时，将基于非直谓逻辑（如 Coq、Matita 和 HOL 系列）的证明助手中所写的证明翻译到基于直谓逻辑（如 Agda）的证明助手中。本文我们提出一种算法，用于在允许类似 Agda 中前缀宇宙多态的核心非直谓类型系统与核心直谓类型系统之间进行此类翻译。它在于尝试将一个潜在非直谓的项转化为尽可能一般的宇宙多态项。使用宇宙多态的理由在于：在大多数情况下，将非直谓宇宙映射到某个固定的直谓宇宙是不够的。在算法过程中，我们需要求解关于宇宙层级上 max-后继代数的合一问题。但在该代数中，存在无可最一般解的可解问题。我们仍提供了一个不完备算法，其解在成功时是最一般的解。所提出的翻译当然是部分的，但在实践中允许翻译许多未本质使用非直谓性的证明。事实上，它已在工具 Predicativize 中实现，并随后用于半自动地将 Matita 算术库中的许多非平凡开发翻译到 Agda，包括伯特兰假设和费马小定理，而这些在 Agda 中尚不可用。