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.

翻译：本文提出了一种确定性小步操作语义模型，用于显式表示miniKanren执行过程中动态演化的搜索树。该语义模型以细粒度方式对交错执行和目标调度进行建模，使得每个评估步骤——包括目标激活、挂起、恢复和成功——都能被精确可视化。基于此模型，我们实现了一个交互式可视化工具，可实时渲染搜索树的构建过程并允许用户单步跟踪执行。该工具作为教学概念机，有助于推理miniKanren的公平搜索行为，帮助用户理解异常答案顺序和操作效应。我们通过基于属性的测试验证了语义模型与工具的正确性，并通过多个示例进行了演示。