Implementation of MGU

mgu.py

# Most General Unifier implementation
# - Tavish Armstrong


class Pred(object):
    def __init__(self, name, args):
        self.name = name
        self.args = args

    def apply(self, sub):
        for i in range(self.arity()):
            arg = self.args[i]
            if arg == sub.old:
                self.args[i] = sub.new

    def arity(self):
        return len(self.args)

    def __repr__(self):
        assert len(self.args) > 0
        argsjoined = ", ".join(repr(a) for a in self.args)
        return "{}({})".format(self.name, argsjoined)


class Var(object):
    def __init__(self, name):
        self.name = name

    def __eq__(self, other):
        if not isinstance(other, Var):
            return False
        return self.name == other.name

    def __repr__(self):
        return "{}".format(self.name)


class Const(object):
    def __init__(self, val):
        self.val = val

    def __eq__(self, other):
        if not isinstance(other, Const):
            return False
        return self.val == other.val

    def __repr__(self):
        return "{}".format(self.val)


class Sub(object):
    def __init__(self, old, new):
        self.old = old
        self.new = new

    def __repr__(self):
        return "{}/{}".format(self.new, self.old)


def isin(e, target):
    if e == target:
        return True

    if isinstance(target, Pred):
        for a in target.args:
            if isin(e, a):
                return True
    elif isinstance(target, Var):
        if isin(e, target.val):
            return True
    elif isinstance(target, Const):
        if e == target:
            return True


def unify(e1, e2):
    print e1, e2
    subs = []
    if isinstance(e1, Const) and e1 == e2:
        return []
    elif isinstance(e1, Var) and not isin(e1, e2):
        return [Sub(e2, e1)]
    elif isinstance(e2, Var) and not isin(e2, e1):
        return [Sub(e1, e2)]
    else:
        if not (isinstance(e1, Pred) and isinstance(e2, Pred)):
            return []
        if e1.name != e2.name:
            return []
        if e1.arity() != e2.arity():
            return []
        print e1, e2
        for i in range(e1.arity()):
            t1 = e1.args[i]
            t2 = e2.args[i]
            new_subs = unify(t1, t2)
            for s in new_subs:
                e1.apply(s)
                e2.apply(s)
            subs.extend(new_subs)
    return subs


# wow so predicate
#              such solution
#   very unified

p1 = Pred('doge', [Var('X'), Const('very')])
p2 = Pred('doge', [Const('tim'), Var('Y')])

print unify(p1, p2)

p1 = Pred('doge', [Var('X'), Const('very')])
p2 = Pred('granddoge', [Const('tim'), Var('Y')])

print unify(p1, p2)

p1 = Pred('doge',
          [Var('X'),
           Pred('father', [Var('X')]),
           Pred('mother', [Const('bill')])])

p2 = Pred('doge', [Const('bill'), Pred('father', [Const('bill')]), Var('Y')])

print unify(p1, p2)