The unification algorithm in Prolog

Question

I'm trying to program the unification algorithm in Prolog to verify if two expressions can unify by returning boolean True/False:

EDIT. I found this implementation usefull: from: http://kti.mff.cuni.cz/~bartak/prolog/data_struct.html

unify(A,B):-
   atomic(A),atomic(B),A=B.
unify(A,B):-
   var(A),A=B.            % without occurs check
unify(A,B):-
   nonvar(A),var(B),A=B.  % without occurs check
unify(A,B):-
   compound(A),compound(B),
   A=..[F|ArgsA],B=..[F|ArgsB],
   unify_args(ArgsA,ArgsB).
   
unify_args([A|TA],[B|TB]):-
   unify(A,B),
   unify_args(TA,TB).
unify_args([],[]).```

Answer 1

Here is a partial implementation of something like the Martelli and Montanari unification algorithm described at https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm. The comments for each part refer to the corresponding rewrite rule from the algorithm. Note that there is no need for an explicit conflict rule, we can just fail if no other rule applies.

% assuming a universe with function symbols g/2, p/2, q/2

% identical terms unify (delete rule)
unify(X, Y) :-
    X == Y,
    !.

% a variable unifies with anything (eliminate rule)
unify(X, Y) :-
    var(X),
    !,
    X = Y.

% an equation Term = Variable can be solved as Variable = Term (swap rule)
unify(X, Y) :-
    var(Y),
    !,
    unify(Y, X).

% given equal function symbols, unify the arguments (decompose rule)
unify(g(A, B), g(X, Y)) :-
    unify(A, X),
    unify(B, Y).
unify(p(A, B), p(X, Y)) :-
    unify(A, X),
    unify(B, Y).
unify(q(A, B), q(X, Y)) :-
    unify(A, X),
    unify(B, Y).

Examples:

?- unify(q(Y,g(a,b)), p(g(X,X),Y)).
false.

?- unify(q(Y,g(a,b)), q(g(X,X),Y)).
false.

?- unify(q(Y,g(a,a)), q(g(X,X),Y)).
Y = g(a, a),
X = a.

One or two things remain for you to do:

• Generalize the decompose rule to deal with arbitrary terms. You might find the =.. operator useful. For example:

    ?- Term = r(a, b, c), Term =.. FunctorAndArgs, [Functor | Args] = FunctorAndArgs.
    Term = r(a, b, c),
    FunctorAndArgs = [r, a, b, c],
    Functor = r,
    Args = [a, b, c].
  

  You will need to check if two terms have the same functor and the same number of arguments, and whether all corresponding pairs of arguments unify.

• Find out if your professor would like you to implement the occurs check, and if yes, implement it.