A Rose Tree is Blooming (Proof Pearl)
summary
Compares two implementations of rose-tree unfolding in the Rocq prover: an inductive version requiring a well‑founded relation and accessibility proofs, and a coinductive version that yields possibly infinite trees but doubles proof effort. Proves soundness and completeness of both unfolds, demonstrates a tic‑tac‑toe state space of about 550,000 nodes (10 unrolls) to build an unbeatable AI, and shows a brute‑force SAT solver; notes coinductive proofs are longer and fuel/convert patterns are used to get finite approximations.
AI-written summary · about
chapters (11)
- 0:00Game trees and rose trees
- 1:45Game trees as rose trees in Rocq
- 3:10Building game trees recursively
- 4:12Infinite games and termination
- 5:17Co-inductive types for infinite trees
- 6:22Lessons from co-inductive game trees
- 7:04Finite trees with well-founded recursion
- 9:53Correctness of unfolded game trees
- 11:17Game tree unfolding in Rocq
- 12:21Lambda calculus as game tree
- 13:24Q&A
related talks
11mGames People Play
25mReal Algebraic Geometry in Computational Game Theory
01h 05mFunctional / Logic Programming in Verse
38mProcedural Generation at Runtime: From Basic to Complex by Example
20mSurviving State Tree: A real case study with Dinosaurs
24mSolving Ricochet Robots
06mDecoding the Maze: New Frontiers in Achieving Nash Equilibrium in AI Architectures
35mVerse - a new functional logic language