Attempt to understand micro-Kanren's search order through machine semantics

[Phil Nguyen]

Hi,

I'm relatively new to mini-Kanren, and trying to get intuition about the interleaving search order. Would it be accurate to say that conceptually there's a queue, and each right disjunct or explicitly delayed relation call is pushed back to the end of the queue?

I made a PLT-redex model here of a "machine" semantics the way I understand the order. Each "machine state" is a queue of "configurations", each of which is a pair of substitution and list of remaining goals. There's an example at the end visualizing the execution of (appendo l r '(1 2 3)).

I made one slight twist in the rule `zzz` for applying a delayed call, putting the new goal to the back of the list. By doing this, the search space for `appendo` becomes finite even though in the source code, the recursive call happens before the unification. Would it be easy to express this goal re-ordering in the standard implementation that "compiles" micro-Kanren to the host language?

With the machine semantics, it might be cool to have a touch interface to interactively explore the state space and choose which configuration to try or which goal to solve next.