Guarded recursion support embedded in Lean for safer programming
Garlene: Guarded Recursion in Lean
Logic in Computer ScienceProgramming Languages
Summary
Extending recursion rules in formal systems can cause serious errors, but a technique called guarded recursion helps prevent these problems. The authors created a tool inside the Lean theorem prover that allows writing and reasoning about guarded recursive definitions more safely. They built a special model to prove their tool works correctly and let users move their guarded recursion work into standard Lean code. This makes it easier to work with infinite structures and advanced programming concepts in Lean.
What this means in practice
- •For functional programmers: Write and verify programs with infinite data structures like streams safely inside Lean using guarded recursion.
- •For programming language developers: Use the embedded guarded recursion language in Lean to model and reason about advanced language features involving recursion soundly.
Authors
Sergei Stepanenko, Patrick Bahr, Rasmus Ejlers Møgelberg
Abstract
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.