%UNIFICATION
%Recall our discussion of reduction:
%Reduction of goal G by program P is the replacement of G
%by the body of a rule in P, whose head matches G.

%Program:
ancestor(X,Y) :- parent(X,Y).
ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y).
parent(george,jeb).
parent(george,w).
parent(herbert,george).
parent(satan,herbert).

%Query:
?- ancestor(satan,w).

%Reduction:
%_ancestor(satan,w)_
%=> _parent(satan,Z)_, ancestor(Z,w)
%=> (true,) _ancestor(herbert,w)_  [Z |-> herbert]
%...

%How are heads matched to goals?  What is this matching?
%ML uses patterns, but Prolog has something more powerful:
%unification

%A *substitution* is a function that maps variables to Prolog
%terms.  For example, [Z |-> herbert] above.

%An *instantiation* is an application of a substitution to all
%of the free variables in a formula or term.  If T is a 
%substitution and P is a formula or term, then PT denotes the
%instantiation of P by T.  Example:

%P =  ancestor(Z,w)
%T =  [Z |-> herbert]
%PT = ancestor(herbert,w)

%C is a *common instance* of formulae/terms A and B, if there
%exist substitutions T1 and T2 such that C = AT1 = BT2.

%A = ancestor(Z,w)        T1 = [Z |-> herbert]
%B = ancestor(herbert,W)  T2 = [W |-> w]
%C = AT1 = BT2 = ancestor(herbert,w)

%A and B are *unifiable* if they have a common instance.
%Examples:

%p(X,X) unifies with p(b,b)
%p(X,X) unifies with p(c,c)
%p(X,X) does NOT unify with p(b,c)

%p(X,Y) unifies with p(b,b)
%p(X,Y) unifies with p(c,c)
%p(X,Y) DOES unify with p(b,c)

%p(b,b) does NOT unify with p(c,c)

%p(f(X)) unifies with p(f(Y))
%p(f(X)) does NOT unify with p(g(Y)) (or even p(g(X)))
%p(f(X),Y) unifies with p(Z,g(X)) [ C = p(f(X),g(X)) ]
%p(f(X),X) unifies with p(Z,b) [ C = p(f(b),b)! ]
%p(b,f(X,X),c) does NOT unify with p(U,f(U,V),V)
%p(X,X) SHOULD NOT unify with p(tail(Z),Z) but it DOES in Prolog
%  [Note: not all Prolog terms are first-order terms]

:- p(b,f(X,X),c) = p(U,f(U,V),V).
:- p(Y,f(W,X),Z) = p(U,f(U,V),V), Y = b, Z = c, W = X.

%p(X,b)   unifies with p(Y,Y)
%p(X,Z,Z) unifies with p(Y,Y,b)
%p(X,b,X) does NOT unify with p(Y,Y,c)

%Some pairs of formulae/terms have many common instances, e.g.:
%p(X,f(Y)) and p(g(U),V) have common instances given by:
%T = [X |-> g(a), Y |-> b, U |-> a, V |-> f(b)]
%T = [X |-> g(c), Y |-> d, U |-> c, V |-> f(d)]
%...

%It can be proven, however, that whenever there is more than
%one common instance, one of these common instances is the
%"most general," i.e., results in the least amount of extra
%information added.  This is the one that Prolog computes.

%The substitution that results in the most general instance is called
%the *most general unifier* (mgu).  It is unique, up to consistent
%renaming of variables.

%T is the most general unifier of a set of substitutions
%{T1,...,Tn} iff there exist substitutions {S1,...,Sn} such
%that for all 1 <= i <= n, and all formulae/terms P, 
%PTi = (PT)Si.

%Example:
%f(W,g(Z),Z) unifies with f(X,Y,h(X))

%We must have:
%W = X
%Y = g(Z)
%Z = h(X)

%Working backwards from W, we have:
%Y = g(Z) = g(h(W))
%Z = h(X) = h(W)
%W = X

%So mgu is:
%[X |-> W, Y |-> g(h(W)), Z |-> h(W)]

%ARITY

%Do f(X,Y) and f(Z) unify?
%No - both arity and functor must match.  Functor alone is not enough to
%determine this.

%More examples:
:- f(X,a)      = f(a,Y).
:- f(h(X,a),b) = f(h(g(a,b),Y),b).
:- g(a,W,h(X)) = g(Y,f(Y,Z),Z).
:- f(X,g(X),Z) = f(Z,Y,h(Y)).
:- f(X,h(b,X)) = f(g(P,a),h(b,g(Q,Q))).

%ANONYMOUS VARIABLES

%Sometimes, we don't care what the value of a particular
%variable is - only that some value exists.

%Normally, Prolog treats identically named variables as
%identical variables, e.g., p(X,X) does not unify with
%p(b,c), but p(X,Y) does because the Xs must refer to the
%same entity.

%But p(_,_) also unifies with p(b,c).  Every instance of
%'_' refers to a different, unique variable.  It is called
%an "anonymous variable."

%Example:
person(X) :- parent(_,X).

%"For all X, X is a person if X has a parent (we don't care
%who)."

%This is equivalent to:

person(X) :- parent(Y,X).

%Y only occurs once here - it is called a *singleton variable*.
%Prolog warns us about singleton variables in our programs,
%because there is no reason to used a named variable only once
%- we could have used an anonymous one.

%In general, any variable beginning with '_' will not result
%in a warning if used only once (so don't do this except to
%comment your anonymous variables).

%ARITHMETIC
%This is one of the few corners of Prolog where it makes sense to talk of
%well-typing or evaluation.

%Prolog terms can either be interpreted as arithmetic expressions or not.
%Those that can can appear on the RHS of is/2, which we have already seen:

:- X is 2+3.

%This:
% - _evaluates_ the RHS, and then
% - _unifies_ the result with the LHS.

%If the LHS is also an arithmetic expression, then it may not succeed:

:- 2+3 is 5.

%This failed because 5 evaluates to the term '5', which is not the same _term_
%as 2+3.

%There is a predicate that evaluates both sides:

:- 2+3 =:= 1+4.

%but you can't use this one to instantiate variables:

:- X =:= 2+3.

%X is *uninstantiated* (not bound to a non-variable term), so it has no
%arithmetic value to give =:=/2.

%Equality Predicates in Prolog:
%is      evaluation and unification
%=:=     symmetric evaluation and equality testing
%=       unification (no arithmetic!)
%==      identity test (no unification!)

%Example: for-loop
:- p(0,A,...).  % for I = 1 to A

p(A,A,...) :- !.
p(I,A,...) :-
  NewI is I + 1,
  ...
  p(NewI,A,...).

%NON-MONOTONICITY

%Prolog's equational theory is called an *extensional* language, which
%means that two identical ground terms are considered equal, even if they
%occupy different locations in memory:

:- X = f(a,b),
   Y = f(a,b),
   X == Y.

%Not so with uninstantiated variables:

:- X == Y.

%nor with other non-ground terms:

:- f(a,X) == f(a,Y).

%Variable identity is completely determined by location in memory.
%But this means that we have a problem:

:- X = f(a,b),
   Y = f(a,b),
   X == Y.

%and yet:

:- X == Y,
   X = f(a,b),
   Y = f(a,b).

%With predicates like ==/2, our very declarative view of Prolog programming
%falls apart.  Now, unlike conjuncts in a logical formula, order matters for
%truth value.  Sometimes, predicates like ==/2 are called *non-monotonic*.

%*Monotonicity* is a property of functions that maintain some sort of
%consistency or constant as their independent variables vary.  Logical
%terms vary in how specific our knowledge about them is.  So in logic 
%programming, monotonic predicates remain either true or false of a term
%as we learn more about that term during some computation.  Terms become
%more specific as a result of successive unifications that they participate
%in.  =/2 is monotonic.

%Non-monotonic predicates lack this property.  That means that we have to
%keep checking them to make sure that they're still true.  Prolog doesn't
%do this, even with non-monotonic predicates, because it's too computationally
%expensive, so non-monotonic predicates must be used with a great deal
%of caution.  ==/2 is non-monotonic.

%Now what about this:

:- X = f(a,b),
   Y = f(c,d),
   X = Y.

%and yet:

:- X = Y,
   X = f(a,b),
   Y = f(c,d).

%Actually, X=Y is false in _both_ cases.  Success doesn't mean truth
%in Prolog until Prolog's resolution procedure has finished - until then,
%it just means that there's still a chance that it's true, depending on
%how the variables work out.