A Fine-Grained Small-Step Semantics for Interleaving Search
摘要
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 with fine granularity, exposing each evaluation step—goal activation, suspension, resumption, and success. This approach supports reasoning about miniKanren’s interleaving search behavior, helping users understand surprising answer orders and operational effects. A reference implementation undergirds an interactive visualizer that renders the search tree as it develops and lets users step through execution; we treat this tool as a consumer and demonstration of the semantics. Our semantics and tool are illustrated by example and validated through property-based testing.