Efficient Rational Unification for miniKanren
summary
Presents an algorithm that performs rational-term unification with performance close to conventional miniKanren triangular substitution on Herbrand terms, optimized for persistent settings and derived from Martelli-Rossi with practical adjustments. Provides a working implementation, an optimized variant used for benchmarks, and a fully certified in Rocq formalization. Evaluation shows the algorithm matches ephemeral baselines, beats the common instance-linking approach in persistent contexts, and incurs only a logarithmic overhead on many workloads.
AI-written summary · about
chapters (13)
- 0:00Rational unification intro
- 1:59Finite automata example
- 4:12Rational terms matter
- 7:29Fast unification primitives
- 9:23Removing occurs check
- 12:01Two unification approaches
- 13:32Variable-only tracking
- 16:29Common part algorithm
- 19:28Evaluation methodology
- 21:43Performance comparison
- 23:13Rational benchmarks
- 24:59Summary of findings
- 26:53Q&A