Terms, substitutions and the MGU

Resolution needs a richer notion of goal. In the Empowering resolution picture:

• goals are 0-ary, 1-ary, 2-ary, ... relations between terms;
• terms are the values of the Prolog language, and are (finite) trees; they can have logic variables in the leaves;
• goal matching is done by so-called unification: essentially a substitution of variables by terms that makes two goals identical;
• unification could also provide a declarative form of side effect;
• computation goes on by evolving a resolvent and the substitution collected so far. The substitution is the computed result.

Prolog terms

The syntax of goals and terms (terms.pl):

Goal ::= Predicate | Predicate ( Term1, ..., Termn )
Term ::= Variable | Number | Functor | Functor ( Term1, ..., Termn )

• predicate and functor names are literals starting with lower case, variables start with upper case;
• predicates and functors are said to have arity 0, 1, 2, ..., n;
• the syntax of goals is a subset of that of terms;
• a term with no variables in it is called ground.

Three unrelated programs in one listing show what a lower-case name is in each position:

What does pred define? Ask it: it relates a cons/nil list with its last element.

Interpretations of Prolog programs

Logic interpretation (the classical one): a program is a logic theory, and computing is proving that a goal is a theorem under that theory. To prove that GF is the grandfather of GS, first prove that ...

Relational interpretation (the idiomatic one, which we shall use): a program is a set of predicates over terms, and computing is querying for a relation. For example, 10 is in the element relation with cons(10, nil).

Procedural interpretation (the operational one): a program is a set of procedures, and computing is calling predicates. The call element(10, cons(20, nil)) causes the call element(10, nil).

Terms as trees

A term is a tree of atoms, with atoms, numbers and variables in the leaves:

• a is an atom, 21 is a number, X is a variable;
• cons(10, cons(20, cons(30, nil))) is a compound (ground) term;
• student(mario, rossi, 1990) is a compound (ground) term;
• student(X, Y, Z) is a compound (non-ground) term.

cons                          student                    student
├── 10                        ├── mario                  ├── X
└── cons                      ├── rossi                  ├── Y
    ├── 20                    └── 1990                   └── Z
    └── cons
        ├── 30
        └── nil

Substitutions

A substitution θ = {X1/T1, ..., Xn/Tn} maps variables to terms, where the terms Tj should contain no variable Xk.

• valid: {}, {Y/10}, {X/a(1,Z), Y/10, W/Z};
• invalid: {X/a(1,Z), Y/10, Z/W} (it should be rewritten as {X/a(1,Z), Y/10, W/Z}).

Related concepts:

• application to terms: p(X,a){X/10} is p(10,a); p(X,a){Y/X} is p(X,a) (equivalent to p(Y,a) under that substitution);
• equivalence of substitutions: {X/Y, Z/10} ≡ {Y/X, Z/10};
• generality: {X/10} is more general than {X/10, Y/2};
• composition of substitutions: {X/10}{Y/X} ≡ {X/10, Y/10}, while {X/10}{X/5} is impossible;
• instance: p(10, b) is an instance of p(X, b);
• term cloning: clone(p(10,X,X,Y)) = p(10,X2,X2,Y2), with X2 and Y2 fresh (this is variable renaming).

Prolog lets you try all of these:

Most General Unifier (MGU)

mgu(T1, T2) is any substitution θ such that

• it is a unifier of T1 and T2, namely θT1 = θT2;
• it is the most general one: out of many unifiers, we exclude the less general ones.

An MGU might not exist, and if many MGUs seem to exist, they are actually all equivalent substitutions. Unification is a symmetrical pattern matching mechanism: it binds variables to non-variable terms, and puts some other variables into groups.

Some examples, tried with =/2:

• mgu(a(1,2), a(X,Y)) = {X/1, Y/2}
• mgu(a(1,2), a(X,X)) = ⊥
• mgu(a(1,b(X)), a(Y,b(Z))) = {X/Z, Y/1}
• mgu(a(X,Y,A,b(W)), a(Z,Z,B,b(1))) = {X/Z, Y/Z, W/1, A/B}: W/1, and the groups (X, Y, Z) and (A, B)

The last two lines are a quick test: ?- p(X,1) = p(2,Y). answers yes with X/2, Y/1, and the opposite test ?- p(X,1) \= p(2,Y). answers no.

The unification algorithm

The algorithm of Martelli and Montanari (1982) works by transformation rules on a set G of term equations:

The check rule is the occurs check: X cannot be unified with a term that contains X. Most Prolog systems skip it for speed in =/2, but unify_with_occurs_check/2 implements it.