µKanren.NET - Featherweight Relational Logic Programming in C#

The µKanren paper is a nice introduction to a lightweight logic programming language which is a simplification of the miniKanren family of languages. The existing µKanren implementation in C# was a translation from Scheme, and thus is verbose, untyped with lots of casts, and non-idiomatic. I also found most of the other Kanren implementations unnecessarily obscure, heavily relying on native idioms that aren't clear to newcomers.

uKanren.NET provides a clear presentation of the core principles of µKanren using only IEnumerable<T> and lambdas, showing that µKanren's search is fundamentally just a set of combinators for transforming sequences of states. The values of the sequence are sets of bound variables that satisfy a set of equations. For instance, given the following expression:

Kanren.Exists(x => x == 5 | x == 6)

You can read it off as saying there exists an integer value to which we can bind variable x, such that x equals either 5 or 6 [1]. Solving this equation produces this sequence of values:

x[0] = 5,
x[0] = 6,

where each line represents a different value that satisfies the equation. These equations can be arbitrarily nested or chained using | and &, just like ordinary logical expressions, and µKanren will find a solution for all variables, if a solution exists. A further benefit of this implementation, is that you cannot accidentally mix up boolean equality expressions with relational logic expressions, because relational equality, conjunction and disjunction operators all operate on non-boolean types.

Logic Variables, Goals & States

We start with the simple core, which is just a logic variable identified uniquely by an integer, and with a convenient local name:

public sealed class Kanren
{
    internal int id;

    // the variable's public name, extracted from the delegate parameter
    public string Name { get; internal set; }

    public static Goal operator ==(object left, Kanren right)
    {
        return Equals(left, right);
    }

    public static Goal operator ==(Kanren left, object right)
    {
        return Equals(left, right);
    }

    public static Goal operator ==(Kanren left, Kanren right)
    {
        return Equals(left, right);
    }
    ...
}

µKanren.NET variables override the equality operators to generate "Goals". A Goal is represented by a delegate that takes a State and generates a sequence of States:

public delegate IEnumerable<State> Goal(State state);

A State is simply a set of variable bindings that satisfy the equations described by the Goal:

public sealed class State
{
    internal Trie<Var, Kanren> subs;
    internal int next = 0;
    internal Func<Goal> incomplete;

    internal Kanren Get(Var x)
    {
        Kanren v;
        return subs.TryGetValue(x, out v) ? v : null;
    }

    internal State Extend(Var x, Kanren v)
    {
        return new State
        {
            subs = subs.Add(x, v),
            next = next,
            incomplete = incomplete,
        };
    }

    internal State Next()
    {
        return new State
        {
            subs = subs,
            next = next + 1,
            incomplete = incomplete,
        };
    }
    ...
}

Each new variable introduced by Kanren.Exists increments the unique variable index we track in State.next, so each variable gets a unique number. Variable bindings are tracked in an immutable hash map provided by Sasa.Collections.Trie<T> (a fast immutable IDictionary).

µKanren Operators

There are 3 core operations on Goals, constructing a Goal with Kanren.Exists, and combining Goals using either disjunction or conjunction:

public sealed class Kanren
{
    ...
    public static Goal Exists(Func<Kanren, Goal> body)
    {
        var arg = body.Method.GetParameters()[0].Name;
        return state =>
        {
            var goal = body(new Kanren { id = state.next, Name = arg });
            return goal(state.Next());
        };
    }

    public static Goal Conjunction(Goal left, Goal right)
    {
        return state => left(state).SelectMany(x => right(x));
    }

    public static Goal Disjunction(Goal left, Goal right)
    {
        return state => left(state).Concat(right(state));
    }

    public static Goal Recurse(Func<Kanren, Goal> body, Kanren x)
    {
        return state => new[]
        {
            new State
            {
                subs = state.subs,
                next = state.next,
                incomplete = () => body(x)
            }
        };
    }
    ...
}

Kanren.Exists just creates a fresh variable using the next number in the sequence, and invokes the function body that produces the Goal. The Goal is then evaluated using the given State, but with an updated variable counter to ensure variables are unique.

Conjunction consists of equations like x == 6 & y == 7. For every State generated by the 'left' Goal, conjunction generates a set of States built from applying the 'right' Goal to that same state. So, x == 6 produces a binding assigning x to 6, which is then passed to the Goal for y == 7, which then adds a binding for y = 7. Thus, "x[0] = 6, y[1] = 7" is produced.

Disjunction consists of equations like x == 6 | x == 7. These Goals are independent and don't interfere with each other, and so any States generated by 'right' are simply appended to the States generated by 'left'. The 'left' Goal produces x = 6, and 'right' produce x = 7, so the result will be:

x[0] = 6,
x[0] = 7,

Because C# features eager evaluation, we have to handle recursion in Kanren expressions manually. We do this via Kanren.Recurse, which takes a Goal constructor and a kanren variable, and returns an "incomplete" State, which basically means a State that was only partially evaluated and may produce further states if you resume evaluation:

public sealed class State
{
    ...
    // True if this state is final, such that all bindings have values,
    // false if some computation remains to be done.
    public bool IsComplete
    {
        get { return incomplete == null; }
    }

    // Get the pairs of bound variables and their values.
    public IEnumerable<KeyValuePair<Kanren, object>> GetValues()
    {
        return subs;
    }

    // Return the remaining stream of states, if any.
    public IEnumerable<State> Continue()
    {
        if (IsComplete) throw new InvalidOperationException("State is complete.");
        return incomplete()(this);
    }
}

The Kanren client is currently responsible for handling incomplete States while iterating over the results. It's possible to handle this in a more uniform manner with a little more execution overhead, but uKanren.NET doesn't currently do so.

Unification

Finally, the real meat of logic programming is resolving equality between logic variables and values. Logic programming solves equations using an algorithm called "unification":

public sealed class Kanren
{
    ...
    static object Walk(object uvar, State env)
    {
        // search for final Kanren binding in env
        Kanren v;
        while (true)
        {
            v = uvar as Kanren;
            if (ReferenceEquals(v, null)) break;
            var tmp = env.Get(v);
            if (ReferenceEquals(tmp, null)) break;
            uvar = tmp;
        }
        return uvar;
    }

    static State Unify(object uorig, object vorig, State s)
    {
        var u = Walk(uorig, s);
        var v = Walk(vorig, s);
        var uvar = u as Kanren;
        var vvar = v as Kanren;
        if (!ReferenceEquals(uvar, null) && !ReferenceEquals(vvar, null)
            && uvar.Equals(vvar))
            return s;
        if (!ReferenceEquals(uvar, null))
            return s.Extend(uvar, v);
        if (!ReferenceEquals(vvar, null))
            return s.Extend(vvar, u);
        if (u.Equals(v))
            return s;
        return null;
    }
    ...
}

Unification brings together all equality declarations between variables and values and ensures they are all consistent. If two variables are unified, then they are either the same variable, or the variable values must unify. If a variable and value are unified, then that value is bound to that variable in the State by extending it. If two values are unified, then they must be equal to each other. If none of these conditions hold, then a null State is returned, indicating an inconsistent set of equality conditions.

Wrap Up

The real uKanren.NET implementation provides a few tweaks to interleave certain streams, and to provide convenient operators on Goals so you can easily combine more sophisticated expressions:

static Goal Fives(Kanren x)
{
    return x == 5 | Kanren.Recurse(Fives, x);
}

static Goal Sixes(Kanren x)
{
    return 6 == x | Kanren.Recurse(Sixes, x);
}

static Goal FivesAndSixes()
{
    return Kanren.Exists(x => Fives(x) | Sixes(x));
}

// output of FivesAndSixes:
// x[0] = 5,
// x[0] = 6,
// x[0] = 5, x[0] = 5, ... [infinite stream of fives]
// x[0] = 6, x[0] = 6, ... [infinite stream of sixes]

However, the implementation described above covers the core operation of µKanren, and the rest is just syntactic sugar to make it nice in C#.

[1] The "Exists" operator was called "call/fresh" in the original paper and in most other implementations. I found it easier to read off uKanren expressions as English with the form I settled on.