Unification is the process of matching Prolog terms. The rules for determining if two terms are unifiable are as follows
- Atoms unify if and only if they are the same atom.
- Numbers unify if and only if they are the same number.
- Structures unify if and only if they have the same functor, they have the same arity (number of arguments) and their arguments unify.
- An uninstantiated variable will unify with any term. As a result the variable will become instantiated to the other term.
- An instantiated variable
Vwill only unify with another termTif the termVis instantiated to will unify withT.
Examples
Atoms unify if and only if they are the same atom.
?- atom1=atom2.
no
?- atom1=atom1.
yesNumbers unify if and only if they are the same number.
?- 1=2.
no
?- 1=1.
yesIf variable V is instantiated and term T is not a variable then V and T unify if and only if the term instantiated on V unifies with T.
?- X=atom1, X=atom2.
no
?- X=atom1, X=atom1.
X = atom1
yesIf variable V is instantiated and term T is an instantiated variable then V and T unify if and only if the term instantiated on V unifies with the term instantiated on T.
?- X=atom1, Y=atom2, X=Y.
no
?- X=atom1, Y=atom1, X=Y.
X = atom1
Y = atom1
yesIf variable V is instantiated and term T is an uninstantiated variable then V and T unifed by instantiating on T the term instantiated on V.
?- X=atom1, X=Y.
X = atom1
Y = atom1
yesStructures unify if, and only if, a) their names unify b) they have the same number of arguments and c) their arguments unify.
?- structure1(atom1,atom2,atom3)=structure2(atom1,atom2,atom3).
no
?- structure1(atom1,atom2,atom3)=structure1(atom1,atom2).
no
?- structure1(atom1,atom2,atom3)=structure1(atom1,atom2,atom4).
no
?- structure1(atom1,atom2,atom3)=structure1(atom1,atom2,atom3).
yes
?- structure1(atom1,X,atom3)=structure1(atom1,atom2,Y).
X = atom2
Y = atom3
yesLists unify if and only if both their heads and their tails unify.
?- [atom,atom2,atom3]=[atom1,atom2].
no
?- [atom1,atom2,atom3]=[atom1,atom2,atom4].
no
?- [atom1,atom2]=[atom2,X].
no
?- [atom1,atom2,atom3]=[X,Y,Z].
X = atom1
Y = atom2
Z = atom3
yes
?- [atom1]=[X|Y].
X = atom1
Y = []
yes
?- [atom1,atom2,atom3]=[X,Y|Z].
X = atom1
Y = atom2
Z = [atom3]
yes
?- [X|Y]=[atom1,atom2,atom3].
X = atom1
Y = [atom2,atom3]
yes
?- [atom1,atom2]=[atom1|X].
X = [atom2]
yes
?- [atom1|Y]=[X|atom2].
X = atom1
Y = atom2
yes
?- [[atom1,Y]|Z]=[[X,atom2],[atom3,atom4]].
X = atom1
Y = atom2
Z = [[atom3,atom4]]
yes
?- A=atom1, B=atom2, C=atom3, D=[A,B,C].
A = atom1
B = atom2
C = atom3
D = [atom1,atom2,atom3]
yes