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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Fine-Grained Small-Step Semantics for Interleaving Search

  • Brysen Pfingsten,
  • Jason Hemann

摘要

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.