Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics

on YouTube ↗25m

" summary

Presents a deterministic small-step semantics that models miniKanren’s interleaving at goal-level granularity using delay/go control, left/right disjunctions (railway model), and an explicit answer stream and trail; mechanized in PLT Redex and checked with property-based testing. Ships a web-based interactive visualizer that renders the evolving search tree, supports single-step stepping, lazy relation expansion (shown on appendo and a same-count/divisible-by-3 example), and caches history for backward steps, letting users inspect substitutions, reifications, and surprising answer orders.

AI-written summary · about

" chapters (14)

1. 0:00miniKanren introduction
2. 1:49miniKanren values definition
3. 3:12Search tree components
4. 5:18Railway interleaving model
5. 7:45Delays handling
6. 9:30Related work
7. 10:14miniKanren visualizer demo
8. 13:04Interleaving visualization
9. 14:30Unification trail exploration
10. 15:34PLT Redex mechanization
11. 16:16Depth-first search extension
12. 16:57Future work
13. 17:39Contributions summary
14. 18:20Q&A