Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics
Abstract
We present a deterministic small-step operational semantics for miniKanren that explicitly represents the evolving search tree during execution. This semantics models interleaving and goal scheduling at fine granularity, allowing each evaluation step-goal activation, suspension, resumption, and success -- to be visualized precisely. Building on this model, we implement an interactive visualizer that renders the search tree as it develops and lets users step through execution. The tool acts as a pedagogical notional machine for reasoning about miniKanren's fair search behavior, helping users understand surprising answer orders and operational effects. Our semantics and tool are validated through property-based testing and illustrated with several examples.
Cite
@article{arxiv.2510.15178,
title = {Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics},
author = {Brysen Pfingsten and Jason Hemann},
journal= {arXiv preprint arXiv:2510.15178},
year = {2025}
}
Comments
2025 miniKanren Workshop