Mini Kanren programming gives you a few basic constructs and you are on your way doing logic programming.

It has a run construct which looks like this

(run* (q) <goals>)

And this means that the it generates all possible values of the variable q, that can be satisfied by all goals that are part of the run.

The simples goal constructor is that of unification and is denoted as a ==. The unifier tries to bind its values together. If both values are compatible the unifications succeeds.

(== 5 5)  - this unification succeeds

(== x 10) – this succeeds and binds x to 10

             (if there was no binding for x before)

(== a b)  – this binds a to b and succeeds

(== a 10) – this binds a to 10 and succeeds, hence b is also 10

(== b 20) – this fails since the b cannot be bound to 20 in this context

So if you say

(run* (q) (== q 10))

You get 10 as the result.

The conde forms the equivalent of an ‘or’ relationship between sets of goals. It returns all the possible substitutions that are got by evaluating each of its goals sets.

(run* (q)

       (conde

             ((== q 10))

             ((== q 20))

             ((== q 5) (== q 15))))

This returns values 10 and 20. The third relation under conde fails because q cant be bound to 15 after it is already bound to 5.

The last construct is fresh. The important thing about mk over prolog is that it has a notion of lexical scope for its logical variables. ‘run’ introduces the variable whose value it will return on evaluating the its goals. Fresh introduces or defines one or more new logical variables which can then be used in relations in the scope of the fresh.

(run* (q)

       (fresh (a)

             (== a q)

             (== a 10)))

This returns 10.

There! That’s all you need to know about mini-kanren.

Embed this much into scheme and you have a full (I think) logic system. Take a closer look at more Mk here.

The real reason I wrote all this is that I had some potentially interesting random thoughts about the logic system. But I could not say it without establishing some context first.

Now, if you are using the Cw version here is the simple conversion Mk.run is run*, Mk.conde is conde. == is Mk.eq. I don’t need a fresh because I use the Cw type system and lexical scoping to create logic variables as instances of class ‘Var’. Get the Cw version is here.