Relation helper (reflexive/symmetric/transitive)

[nardi]

I was trying to write a simple transitive relation, and had a bit of a difficult time (and as I can see in previous issues I am not the first). Maybe it would be a good idea to include some extra functionality in- or outside the Relation class which allows one to easily define reflexive, symmetric and/or transitive relations? These are very common properties for relations found in mathematics, so it might be nice to support these out-of-the-box.

I've written a little helper as a start, but it still has the possibility for infinite loops when there is a cycle in the graph. However I'm not sure how to fix that neatly.

def extend_relation(rel, reflexive=True, symmetric=True, transitive=True):
    def goal(a, b):
        c = var()
        return conde(
            [eq(a, b)] if reflexive else [fail],
            [rel(a, b)],
            [rel(b, a)] if symmetric else [fail],
            [neq(a, c),
             neq(c, b),
             rel(a, c),
             Zzz(goal, c, b)] if transitive else [fail]
        )
    return goal

[brandonwillard]

Can you provide a complete example? That will help me understand the context better.

[nardi]

Well, I was trying to put together a simple subclass relation, SubclassOf (I'm trying to implement a bit of OWL using kanren :) ), which is transitive (if A is a subclass of B, and B is a subclass of C, then A is a subclass of C) and also reflexive (A is a subclass of A, seems a bit weird but you should think of it as set inclusion).

To implement this, I had to take care of a few cases. A is related to B iff:

1. A is equal to B
2. SubclassOf(A, B)
3. There is a C such that SubclassOf(A, C) and C is a subclass of B.

These three cases are implemented in the above function, with the addition of the common symmetric case (A~B implies B~A) and a few neq constraints to avoid loops.

A full example:

SubClassOf = Relation("SubClassOf")

is_subclass = extend_relation(SubClassOf, symmetric=False)

facts(SubClassOf,
    ('A', 'A'),
    ('A', 'B1'),
    ('B1', 'C'),
    ('B2', 'C'),
    ('C', 'D')
)

x = var()
set(run(0, x, is_subclass('A', x)))
# should be: {'A', 'B1', 'C', 'D'} in some order

[nardi]

I also found it useful to have an extra keyword argument equivalence=eq which specifies the relation to use to determine whether two objects are equal (in OWL's case it is possible to explicitly assert two classes are equal using an EquivalentClasses relation).

[nardi]

Another example: take this attempt to write an ancestor relation from a previous issue:

def ancestor(x,y):
    z = var()
    return conde(parent(x,y), (parent(x, z), ancestor(z, y)))

This could be accomplished using the helper as follows:

ancestor = extend_relation(parent, reflexive=False, symmetric=False)

Of course it could also be switched to having the arguments default to false, so it instead becomes:

ancestor = extend_relation(parent, transitive=True)

[brandonwillard]

I think I understand, and it sounds good, but I'll need a solid minute to think about the module in which this helper function should go, and so forth.

Otherwise, from my quick read of all this, my immediate reaction to that exact implementation of extend_relation is that neq—and other constraint-based relations/goals—are generally good to avoid, when (reasonably) possible. That's not to say there's a way to implement extend_relation without using neq, but it's something to consider (and put in a docstring).

Feel free to put in a PR, and, as long as you're willing to rebase, we can work out the details from there.

[nardi]

I put together a new version, which has an API that makes more sense, and seems to be faster somehow? Maybe because I didn't need the neqs, not sure why that is, but nice coincidence :) Anyway, you can use the separate functions as decorators as well now:

def reflexive_relation(eq=eq):
    def inner(rel):
        def goal(a, b):
            return lany(
                eq(a, b),
                rel(a, b)
            )
        return goal
    return inner

def symmetric_relation(rel):
    def goal(a, b):
        return lany(
            rel(a, b),
            rel(b, a)
        )
    return goal

def transitive_relation(rel):
    def goal(a, c):
        def transitive_step(a, c):
            b = var()
            return lall(
                rel(a, b), rel(b, c)
            )

        return lany(
            rel(a, c),
            Zzz(transitive_step, a, c)
        )
    return goal

def equivalence_relation(rel, reflexive=True, symmetric=True, transitive=True, equivalence=eq):
    if transitive:
        rel = transitive_relation(rel)
    if symmetric:
        rel = symmetric_relation(rel)
    if reflexive:
        rel = reflexive_relation(equivalence)(rel)
    return rel

[brandonwillard]

Sorry, I've been extremely busy. Anyway, these look good, so I gladly invite you to create a PR for them.