发表机构
IT University of Copenhagen; Aarhus University（哥本哈根信息技术大学; 奥胡斯大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出 Garlene，一种在 Lean 中实现保护递归的嵌入式语言，提供直观语法与专用证明模式，并通过预层模型证明其可靠性，支持导出至标准 Lean 开发，以解决主流定理证明器缺乏保护递归支持的问题。
AI 中文摘要
扩展形式系统的递归原理是一个诱人但危险的尝试，其导致一致性错误的历史已有充分记录。Nakano 的保护递归是一种优雅的、基于类型的方法，能够以强大的递归原理合理地扩展类型理论。这使得保护递归在许多应用中非常有用，从使用流等无限结构进行编程，到使用合成保护域理论推理高级编程语言特性。遗憾的是，任何主流交互式定理证明器都不直接支持保护递归，这使得保护递归的用户只能依赖未机械化的纸笔证明，或依赖未维护的定理证明器的机械化实现。在本文中，我们提出了一种将保护递归作为 Lean 中的嵌入式语言的实现，该语言由用于定义的简单类型 lambda 演算和用于推理的高阶逻辑组成。利用 Lean 对元编程的出色支持，我们的语言允许用户以直观的语法编写保护递归定义，并使用专用的证明模式证明其性质。我们为我们的语言提供了一个预层模型，我们用它来证明我们语言的可靠性，并允许用户将保护递归定义及其定理导出到标准的 Lean 开发中。为了展示我们语言的实用性，我们提出了几个关于使用保护递归进行编程和推理的案例研究。
英文摘要
Extending the recursion principles of a formal system is an enticing but dangerous endeavour with a well-documented history of leading to consistency bugs. Nakano's guarded recursion is an elegant, type-based approach to soundly extend type theory with a powerful recursion principle. This makes guarded recursion useful for many applications, from programming with infinite structures such as streams to reasoning about advanced programming language features using synthetic guarded domain theory. Sadly, guarded recursion is not directly supported by any major interactive theorem prover, which leaves users of guarded recursion with unmechanised pen-and-paper proofs or mechanisations that depend on unmaintained theorem provers. In this paper, we present an implementation of guarded recursion as an embedded language in Lean consisting of a simply-typed lambda calculus for definitions and a higher-order logic for reasoning. Using Lean's excellent support for metaprogramming, our language allows users to write guarded recursive definitions in an intuitive syntax and to prove properties about them using a dedicated proof mode. We give our language a presheaf model, which we use to prove the soundness of our language and to allow users to export guarded recursive definitions and their theorems into standard Lean developments. To demonstrate the usefulness of our language, we present several case studies for programming and reasoning with guarded recursion.
