Unification and Pattern Matching

 The Logical Model  Introduction Backtracking  Unification Programming

Unification is the way variables are bound to a value.


What will be cover ?


When are two terms equals (equivalent)?  How does Prolog bind values to a variable?

Example: When do two terms rel(X ,b) rel(a, Y) match?

The term , rel(a ,b) is called an instance of rel(X ,b)

"The unification rules for Prolog state that
 
1. Explicitly through the use of "=" operator
 
rel(X ,b) = rel(a, Y)

2. Unification occurs implicitly when a rule is applied

identity(Z,Z).  %clause in file

?- identity(rel(X ,b), rel(a, Y))  %query
X = a
Y = b


  • Which of  the following unify?  What are the instantiated value of the variables for the successful unification?

  • 1?- one = one .

    2?- one  = two .

    3?- one  = X .

    4?-r( a, X ) =  r( Y, b).

    5?- r( X )  = f( X ).

    6?- [ a | Tail ] = [ Head | [ x , y ] ] .

    7?- [ a | T ] = [ a ] .

    8?- r( a, f( X ) )  =  r( Y , b )

    9?- r( a, f ( X ) ) = r( Y,  f( b ) ).

    10?-  r( X ) = r( X , Y ).

    11?– f(a) = f( X ,a).

    12?– X = f( X  ).

    13?– [A, B | X] = [2, 1].

    14? – p( X , X ) = p(Y, f(Y )).

    15? – f( X , g( X  )) = f(a, Y ).

    16? – f( X , b, g( X  )) = f(A, A, g(a)). 

    17? - (X,R) = (a,b,c,d).

    18? - [X] = [a,b,c,d].

    19? - (X) = (a,b,c,d).


    (help(unify_with_occurs_check).
    unify_with_occurs_check(+Term1, +Term2)                             [ISO]
        As  =/2, but  using sound-unification.    That is,  a variable  only unifies  to  a term  if  this term  does  not contain  the  variable itself.  To illustrate this, consider the two goals below:

        1 ?- A = f(A).

        A = f(f(f(f(f(f(f(f(f(f(...))))))))))
        2 ?- unify_with_occurs_check(A, f(A)).

        false.

        I.e.   the  first  creates  a  cyclic-term,  which  is   printed  as  an  infinitely   nested  f/1  term  (see  the  max_depth  option  of  write_term/2).  The second executes logically sound unification and thus  fails.  Note that the behaviour of unification through  =/2 as well  as implicit unification in the  head can be changed using  the     Prolog flag occurs_check.

    For more information see Occurs check - Wikipedia, the free encyclopedia

    Arithmetic in Prolog


     How can we construct loops in Prolog?


    Fall, 2016