An Empirical Study of Rational Tree Unification for miniKanren

on YouTube ↗24m

" summary

Implements complete rational‑tree unification inside miniKanren for recursive type inference, replacing substitutions with equation systems instead of substitutions and defining concrete union/find/bind operations that first union variables then unify right‑hand heads to avoid hangs on cyclic terms. Adds mu‑term extraction for minimal DAG answers and evaluates three occur‑check heuristics (trivial, multiplicative, square‑root). Benchmarks show little change on many queries but reduce the slowest case from 21s to 8s, and the implementation is available as miniKanren extensions.

AI-written summary · about

" chapters (12)

1. 0:00Rational tree unification intro
2. 1:28Motivation for complete RTU
3. 3:15What are rational trees
4. 4:22Unification algorithm basics
5. 7:39First two unification rules
6. 9:51Variables vs non-variable trees
7. 12:05Conventional vs new algorithm
8. 15:01Graph representation of RTs
9. 17:34Generating mu-notation terms
10. 19:16miniKanren implementation & performance
11. 21:53Evaluation results & conclusion
12. 22:38Q&A