Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics
Brysen Pfingsten, Jason Hemann
TL;DR
The paper tackles the challenge of understanding miniKanren's non-deterministic, fair interleaving search by delivering a deterministic small-step semantics that preserves the evolving search tree and exposes intra-goal evaluation steps. It couples this semantic foundation with a Mixed Redex-JS visualizer and a pedagogical notional machine to enable precise stepping through evaluation, including an Explicit Answer Stream, a railway-style pointed disjunction, and delayed relation expansion. The work is validated via property-based testing and demonstrated with concrete miniKanren queries, illustrating intuitive and unintuitive answer orders and enabling targeted debugging and optimization. Practically, the approach offers a reusable framework for visualizing and diagnosing logic-program execution, with potential extensions to full debugging, user studies, and exploration of alternative interleaving strategies.
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.