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 <https://gist.github.com/philnguyen/ee4b6bb4a142941889d11cbf8fbf82ef> 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. -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/minikanren/574929ba-a993-4235-a6e2-6d7d6dbe90e1%40googlegroups.com.
