Gluey

Gluey is a bare-bones unification framework. It defines low-level primitives for unifying objects including support for recursive unfication and backtracking. Though it does not define tree-like unification types, it does define primitives that make these very simple to build. For a full-featured logic framework (built on top of Gluey!), check out Axiomatic.

Your handy unification primitive.

A Binding is a sort of variable that can be linked to another binding such that they will always have the same value. The unification of two Bindings will always succeed unless both already have values, and these values are not equal. If the two are incompatible, a UnificationError is thrown. Behind the scenes, Bindings are held together by sharing a common Glue, but you don't need to worry about this. All you need to know is that once two Bindings are bound, they will always have the same value.

let a = Binding<Int>()
let b = Binding<Int>()
let c = Binding<Int>()

try Binding.unify(a, b) // all good
try Binding.unify(b, c) // we're cool

a.value = 10
print(c.value) // -> 10

let d = Binding<Int>()
try Binding.unify(a, d) // no problem
print(d.value) // -> 10
// Since d.value = nil, it will take on a's value.

let e = Binding<Int>()
e.value = 20
try Binding.unify(a, e) // UNIFICATION ERROR!!!
// Since a.value = 10 and b.value = 20, they cannot be unified.

The recursive unification superstar!

Gluey also defines a generic enum Unifiable<Element> with cases Variable(Binding<Element>) and Literal(Element) making it easy to unify known literals with unknown variables. A very useful property of Unifiable is that it will also attempt to recurisvely unify the literal case if Element: UnifiableType. This allows Unifiable to be used to create powerful tree-like structures that can be easily unified.

// Unification of literal and variable
let a = Unifiable.Literal(10)
let b = Unifiable.Variable(Binding<Int>())
try Unifiable.unify(a, b)
print(b.value) // -> 10

// Recursive unification
let c = Unifiable.Literal(Unifiable.Literal(10))
let d = Unifiable.Literal(Unifiable.Variable(Binding<Int>()))
try Unifiable.unify(c, d)
print(d.value?.value) // -> 10

Still confused? Read more about Gluey in the documentation, check out some of the test cases, or maybe check out how its used in Axiomatic! Or tweet me if you still need some help. :)