Well-founded recursion done right
summary
Defines non-structural recursion by adding an extra accessibility proof argument and making recursion structural on that proof, so a function like gcd recurses on a mod b via a proof that b is accessible. Uses Coq’s Acc elimination (e.g. Acc_inv) to produce transparent subproofs, calls the function with a well‑foundedness proof, and relies on proof erasure so extraction erases proofs. Works for widening‑iteration examples and needs no axioms.
AI-written summary · about
chapters (7)
- 0:00Well-founded recursion intro
- 2:03Coq programming requirements
- 3:05Standard recursion problems
- 6:18Accessibility predicates
- 9:49Tarski iteration example
- 12:38Advantages of the approach
- 13:21Q&A
related talks
15mA systematic approach to "Well-founded recursion done right"
21mIntrinsically Correct Algorithms and Recursive Coalgebras
24mA Type-Based Approach to Divide-and-Conquer Recursion in Coq
56mAn introduction to recursion schemes
29mIntroduction to Recursion Schemes
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
27mTail Recursion Modulo Context: An Equational Approach
19mMutually Iso-Recursive Subtyping