Merging Inductive Relations
summary
Algorithm takes two inductive relations over the same data type and produces a single relation provably equivalent to their conjunction by constructor-pair unification, substitution, and rewriting that eliminates duplicated constraints so constructors become recursive in the merged relation. Applied to BST and balance it yields an AVL relation that QuickChick uses to generate orders-of-magnitude larger trees than naïve filter-based generation; handles trickier cases (less-than-between) by detecting non-changing indices and adds derived constructors; implementation emits soundness/completeness proofs and ships in QuickChick 2.0.
AI-written summary · about
chapters (9)
- 0:00Merging inductive relations
- 2:33Inductive relations for testing
- 4:18Composing inductive relations
- 6:02Merging algorithm
- 9:13BST and Bal results
- 10:17Less-than relations merge
- 12:50Other merges and proofs
- 13:10QuickChick 2.0
- 13:39Q&A
related talks
21mNested Inductive Types for Rocq and Lean
13mInductive Synthesis of Inductive Heap Predicates
22mA Calculus of Inductive Linear Constructions
14mOn Fair Relational Conjunction
24mChoice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...
20mThe Functional Essence of Imperative Binary Search Trees
24mAll for one and none forall: Compiling polymorphic relations without(…)
21mRelational Abstractions Based on Labeled Union-Find