It's probably time for me to try to get my head around microKanren again, since it's where all the logic programming seems to be happening, and it's at least possible to implement it.

Something I didn't grasp last time I looked at it: there is a tiny but subtle magic in the Kanren search algorithm. "Interleaving Depth-First Search", as the (rather murky) 2013 microKanren paper hints abut but this 2017 paper makes clear:

<< Prologs default to depth-first search, whereas Kanrens rely on an unguided, interleaving depth-first search, based on Kiselyov et al.’s Logic monad [24], that is both complete and more useful in practice than are breadth-first or iterative deepening depth-first search. Other than Kanrens, this style of search is not currently available in any logic language of which we are aware. >>

I want to know more about this! As efficient as depth-first, yet complete?


The microKanren paper:

<< The complete μKanren search strategy amounts to something on the order of a tree of trampolines. Results emerge ordered roughly by the number of trampoline bounces required tofind them in a search tree, and approximates performing the search in parallel. Another analogy is that of a juggler juggling jugglers, where each juggler is an mplus, and the act of juggling is represented by the handoff of control in the second cond line of mplus. >>

· · Web · 1 · 2 · 0

(I warned you the 2013 paper is murky).

Since "mplus" is what "disj" does, I *think* what's going on is this:

A relation in Kanren is a function from a state to a state. A state is a list of variable bindings. A state is wrapped in a stream which is a lazy-list using a thunk as its cdr.

There are only four operations: fresh, unify, conj, disj. Fresh only operates on states, not streams, and makes a new variable. Unify binds a variable to a name or flunks out. Disj forks a stream, conj juggles

(like, it patches the first part of the stream onto what else is there)

Both conj and disj call 'mplus' to add a new goal onto a stream, and mplus has been fiddled with to *swap* its elements, which is where the deep magic happens that makes search complete.

It's going through multiple indirects each time which makes it a little hard to follow, as higher-order functions always are.

The thing about Kanren is that even though this is all very nice and I like it, what we still have is a multi-layer cake of

* a functional language
* relations which are a kind of function from state to state
* operators which are functions of relations
* interface functions which take states/streams and return actual values

It's hard to see how to close this loop so that here are *only* relations, not functions. Prolog achieves this, but at the cost of side effects; Kanren hasn't quite.

One thing I've wondered is if we could have relational operators which - more like SQL or especially Kusto queries - operate on relations directly. (With relations being potentially infinitely large, so, like Kanren streams... but of data, not streams of environments).

That way, we would have output always being data, but perhaps data marked up with an environment.

But that language I think would not be quite like Kanren. A dual of it, I think. A Forth to its Lisp, with stack-like operators.

(Not really stacklike... they would operate on relations. But relations might not necessarily have named columns. They might be numeric-indexed tuples, and they might come in blocks of numeric-indexed rows plus a variable-mapping environment (also a relation) plus function-like things (also relations) which would represent delayed parts of the computation.)

Anyway, that's about as far as I can put my head without it starting to hurt. I feel that there's something there worth exploring. But it's probably several PhDs worth of exploration for someone who really knows the adjacent territory.

Kanren at least is marking out a chunk of that adjacent territory and making logic programming cool for the functional people.

But think about the intersection of Kanren and Kusto, if you can. What could you get if you made *everything* to be a relation?

Sign in to participate in the conversation

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!