I'm trying to implement Unification, but having problems.. already got dozen of examples,but all they do is to muddy the water. I get more confused than enlightened :
http://www.cs.trincoll.edu/~ram/cpsc352/notes/unification.html
https://www.doc.ic.ac.uk/~sgc/teaching/pre2012/v231/lecture8.html [code below is based on this intro]
http://www.cs.bham.ac.uk/research/projects/poplog/paradigms_lectures/lecture20.html#representing
https://norvig.com/unify-bug.pdf
How can I implement the unification algorithm in a language like Java or C#?
The art of Prolog one ...and several others. The biggest problem is that I could not figure clear statement of the problem. More mathy or lispy explanations are confusing me even more.
As a good start it seems a good idea to follow the representation to be list based (like in the lispy cases) i.e. :
pred(Var, val) =becomes=> [pred, Var, val]
p1(val1, p2(val2, Var1)) ==> [p1, val1, [p2, val2, Var1]]
except how do you represent lists themselves !? i.e. [H|T]
I would love if you can show me a Python pseudo code and/or more detailed algorithm description or a pointer to one.
Some points I grasp is the need to separate the code in general-unifier and var-unification, but then I cant see the mutual-recusive case ! ... and so on.
As a side note : I would also love for you to mention how would you handle Unification on Backtracking. I think I have backtracking squared-away, but I know something has to happen to substitution-frame on backtracking.
Added an answer with the current code.
http://www.igrok.site/bi/Bi_language.html
I will quickly summarize the chapter about Unification Theory by Baader and Snyder from the Handbook of Automated Reasoning:
Terms are built from constants (starting with a lower case letter) and variables (starting with an upper case letter):
cardate(1,10,2000)Date (variables never have arguments)A substitution is a map assigning terms to variables. In the literature, this is often written as {f(Y)/X, g(X)/Y} or with arrows {X→f(Y), Y→g(X)}. Applying a substitution to a term replaces each variable by the corresponding term in the list. E.g. the substitution above applied to tuple(X,Y) results in the term tuple(f(Y),g(X)).
Given two terms s and t, a unifier is a substitution that makes s and t equal. E.g. if we apply the substitution {a/X, a/Y} to the term date(X,1,2000), we get date(a,1,2000) and if we apply it to date(Y,1,2000) we also get date(a,1,2000). In other words, the (syntactic) equality date(X,1,2000) = date(Y,1,2000) can be solved by applying the unifier {a/X,a/Y}. Another, simpler unifier would be X/Y. The simplest such unifier is called the most general unifier. For our purposes it's enough to know that we can restrict ourselves to the search of such a most general unifier and that, if it exists, it is unique (up to the names of some variables).
Mortelli and Montanari (see section 2.2. of the article and the references there) gave a set of rules to compute such a most general unifier, if it exists. The input is a set of term pairs (e.g. { f(X,b) = f(a,Y), X = Y } ) and the output is a most general unifier, if it exists or failure if it does not exist. In the example, the substitution {a/X, b/Y} would make the first pair equal (f(a,b) = f(a,b)), but then the second pair would be different (a = b is not true).
The algorithm nondeterministically picks one equality from the set and applies one of the following rules to it:
s = s (or X=X) is already equal and can be safely removed.f(u,v) = f(s,t) is replaced by the equalities u=s and v=t.a=b or f(X) = g(X) terminates the process with failure.t=X where t is not another variable is flipped to X=t such that the variable is on the left side.X=t, t is not X itself and if X occurs somewhere within t, we fail. [1]X=t where X does not occur in t, we can apply the substitution t/X to all other problems.When there is no rule left to apply, we end up with a set of equations {X=s, Y=t, ...} that represents the substitution to apply.
Here are some more examples:
{f(a,X) = f(Y,b)} is unifiable:
decompose to get {a=Y, X=b} and flip to get {Y=a, X=b}{f(a,X,X) = f(a,a,b)} is not unifiable:
decompose to get {a=a,X=a, X=b}, eliminate a=a by triviality, then eliminate the variable X to get {a=b} and fail with symbol clash{f(X,X) = f(Y,g(Y))} is not unifiable:
decompose to get {X=Y, X=g(Y)}, eliminate the variable X to get {Y=g(Y)}, fail with occurs checkEven though the algorithm is non-deterministic (because we need to pick a equality to work on), the order does not matter. Because you can commit to any order, it is never necessary to undo your work and try a different equation instead. This technique is usually called backtracking and is necessary for the proof search in Prolog, but not for unification itself.
Now you're only left to pick a suitable data-structure for terms and substitutions and implement the algorithms for applying a substitution to a term as well as the rule based unification algorithm.
[1] If we try to solve X = f(X), we would see that X needs to be of the form f(Y) to apply decomposition. That leads to solving the problem f(Y) = f(f(Y)) and subsequently Y = f(Y). Since the left hand side always has one application of f less than the right hand side, they can not be equal as long we see a term as a finite structure.