A Lean, Mean, miniKanren Machine
summary
Presents a reduction semantics for miniKanren implemented in PLT Redex with a JavaScript/Racket stepper that visualizes an executable search tree and reproduces both depth‑first and interleaved DFS by fixing a parametric scheduler. The core is a small set of rules (about 13 reduction steps for the core, ~21 total with delay and disjunction) plus three carriers for fresh‑variable provenance; the GUI shows emitted answers, pending delays, and the representation is refocusable toward an abstract machine via refocusing, transition compression, and fixed‑point fusion.
AI-written summary · about
chapters (22)
- 0:00miniKanren introduction
- 1:06Query demo and trick question
- 3:56Answer order matters
- 4:59miniKanren as reduction
- 7:35Normalized trees and values
- 9:45Search tree nodes and syntax
- 13:43Separating program and answers
- 14:46Executing search step by step
- 17:21Delay nodes and scheduler
- 20:11Adding relation calls
- 21:41Disjunction with railroad switch
- 23:07Unification in reduction
- 24:56GUEY tool features
- 26:19Comparing search semantics
- 27:07Core reduction steps
- 28:58Adding delay and disjunction
- 30:45Logic variable provenance
- 33:18Non-determinism as data
- 34:44Redex pipeline for semantics
- 37:13Multiple miniKanren representations
- 39:21miniKanren machine vision
- 40:43Q&A