A Functional Proof Pearl: Inverting the Ackermann Heirarchy
summary
Claim: a certified algorithm computes the inverse Ackermann function for all n without constructing huge Ackermann values, formalized in Coq as a compact development. Key tools are a repeater/kowtow inversion that builds inverse towers from lower levels and a worker/budgeted recursion that guarantees termination. Implementation returns alpha(n) correctly and provably runs in linear time in the size of the input (with small constant factors); proofs and code live in the paper/github.
AI-written summary · about
chapters (9)
- 0:00Start
- 0:45The Inverse Ackermann Function
- 3:00Roadmap
- 9:43A Coq Computation of Countdown
- 11:01The Inverse Hyperoperation Hierarchy
- 11:37The Inverse Ackermann Hierarchy
- 12:55Implementation Idea
- 13:45The Worker Function
- 18:04Conclusion
related talks
23mEfficient Dual-Numbers Reverse AD via Well-Known Program Transformations
15mA systematic approach to "Well-founded recursion done right"
21mWell-founded recursion done right
32mA Finite Alternation Result for Reversible Boolean Circuits
21mIntrinsically Correct Algorithms and Recursive Coalgebras
55mNon-commutative Computation
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
53mNew Lower Bounds and Derandomization for ACC, and a...