Prolog Notes

A. C. Brett acbrett@uvic.ca Department of Linguistics University of Victoria Clearihue C139

Unification in Prolog

Unification is essentially a pairwise matching process. This process is straightforward in the case of simple or elementary terms such as atoms, numbers, and strings. For example, two atoms match, and are said to unify, if and only if they are the same atom. Similarly, pairs of numbers or strings unify just in case they are the same. Pairs consisting of lists or structures also unify just in case they are the same; but, the unification process becomes somewhat more complicated with these more complex terms.

Unification of Structures

If all the arguments of the two structures are elementary terms such as atoms or numbers, the process of unifying the structures ends with the matching of the pairs of elementary terms comprising their arguments. If, however, at least one of pair of arguments is complex, consisting for example of two structures, then the procedure for unifying structures must then be applied to this pair of arguments. One or more of the argument pairs in these structures may in turn be structures themselves so that the structure unification procedure must also be applied to them. Thus, the procedure for unifying structures can be recursive.

The structure unification procedure is applied recursively or, in other words, it is re-entered, until the arguments being compared consist only of elementary terms such as atoms and numbers. The recursive application of the structure unification procedure therefore ends with the unification process being reduced to just the comparison of elementary terms. If all these elementary terms match, the two structures unify. If at any stage of the process, however, one pair of arguments is encountered that do not unify, then the structures cannnot be unified.

Unification of Lists

The items of a list can be complex terms, including lists or structures. If a pair of items in the lists being unified are themselves lists, then the procedure for unifying lists is re-entered. If the items are structures, then the procedure for unifying structures is applied. Since an argument of a structure can be a list, the procedure for unifying lists might be applied during the unification of a pair of structures. Thus, during the unification of either lists or structures, the level of recursion can, in principle, be unbounded.

Unification with Variables

Variables are instantiated during the unification process. In fact, unification is the process, and the only means, whereby variables are instantiated. For example, if an argument of one structure is an uninstantiated variable, and the corresponding argument of the second structure is an atom, then the arguments are unified by instantiating the atom on the variable in the first structure. The argument in the second structure might also be a list or a structure, in which case, the list or structure gets instantiated on the variable in the corresponding argument of the first structure. If both arguments are uninstantiated variables, then they are still unified, but the two variable names become synonyms for the same variable, notwithstanding they may (and usually do) have different names.

Unification in the Processing of Queries or Claims

The process of unifying a goal with a fact is straightforward, and proceeds as described above for the unification of two structures. When pairs of arguments being unified consist of lists, or variables, then the procedures discussed above for the unification of lists, or variables, are employed. If the goal and the fact can be unified, then the Listener has succeeded in proving the goal, and it responds "yes". If the goal cannot be unified with the fact, the Listener will attempt to find another structure, either another fact or the head of a rule, with which the goal might unify. If no such structure can be found when the Listener encounters the end of the program, it will respond "no".

If the Listener can unify a goal that has been typed with the head of a rule in the program, it will then attempt to prove each goal in the tail of this rule, beginning with the first. The process of proving of these goals is conducted as if they had been typed to pose a query or to assert a claim; that is, the Listener attempts to unify each goal with a fact or with the head of another rule. The Listener tests the goals in the order in which they appear in the tail of the rule, and for each goal, it begins the testing process with the first statement in the program. If a goal unifies with the head of another rule, the Listens attempts to prove the goals in the tail of this rule. If the rule is recursive, one of the goals will in fact unify with its head. One or more of the goals might also unify with the heads of other rules. This process of unifying a goal with the head of a rule, and then proving the goals in the tail, might be repeated a number of times. The process normally ends when a goal can be unified with a fact, and consequently is proved. If all the goals being proved during the course of this process can be unified with facts, then the initial query can be answered affirmatively, or the claim has been proved, and the Listener will respond "yes". While other proofs or routes to the affirmative response might be available, because there could well be alternative facts or rules in the program that will also yield a proof, the Listener will find only the first.

It can also happen that, although the Listener is able to prove a goal in the tail of a rule, it may fail to prove another goal that follows it in the tail of the same rule. Under these circumstances, the Listener will backtrack and attempt to find another proof for the goal it has already succeeded in proving. If it can find another solution for this gaol, it will then attempt to prove the goal that had failed previously. If this attempt fails, the Listener will backtrack again. The Listener may backtrack a number of times, and backtracking might occur during the processing of a number of different rules. The Listener will continue to backtrack, as necessary, until either it succeeds in proving all the goals in each of the rules invoked during the proof, or it exhausts all the alternatives. Under the latter circumstances, the Listener must respond "no"; under the former, it will have succeeded in proving the initial claim, or it has obtained a positive response to the query, and it can respond "yes".

Throughout the foregoing processes, the Listener employs the procedure for unifying structures and, as necessary, the procedures for unifying other Prolog terms such as lists, atoms, and numbers, and for instantiating variables. A summary of these procedures appears in the following section.

Summary

• Atoms unify if and only if they are the same atom.
• Numbers unify if and only if they are the same number.
• Strings unify if and only if they are the same string.
• Lists unify if and only if
  1. their heads unify, and
  2. their tails unify.
• Structures unify if and only if
  1. their names unify,
  2. they have the same number of arguments, and
  3. their arguments unify.
• Variable V unifies with Term T just in case one of the following conditions is satisfied:
  • V is an instantiated variable.
    • If T is not a variable, then V and T unify if and only if the term instantiated on V unifies with T.
    • If 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.
    • If T is an uninstantiated variable, then V and T are unified by instantiating on T the term that is instantiated on V.
  • V is an uninstantiated variable.
    • If T is not a variable, then V and T are unified by instantiating T on V.
    • If T is an instantiated variable, then V and T are unified by instantiating on V the term that is instantiated on T.
    • If T is an uninstantiated variable, then V and T unify and become synonyms for the same variable.