Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911216388014080 |
|---|---|
| author | Pfingsten, Brysen Hemann, Jason |
| author_facet | Pfingsten, Brysen Hemann, Jason |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_15178 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics Pfingsten, Brysen Hemann, Jason Programming Languages 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. |
| title | Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2510.15178 |