Linguistics 482 - Computational Linguistics Prolog Notes A. C. Brett acbrett@uvic.ca
Department of Linguistics
University of Victoria
Clearihue C139
Last updated: 3 October 1999

Unification in Prolog

Unification is the principal operation that the Prolog interpreter undertakes to prove claims and respond to queries. To understand how the interpreter, or Listener, employs unification to process queries or claims, one must first understand how unification is applied to the different Prolog terms.

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

Complex terms such as structures are actually composed of elementary terms, and the process unifying structures is based upon the unification of these elementary constituents. For example, a structure is composed of a name, which is an atom, together with a sequence of arguments, which may be any terms. Hence, the unification of a pair of structures is performed on the basis of their names, the number of their arguments, and the arguments themselves; that is, two structures can be said to unify if their names match, they have the same number of arguments, and their arguments unify.

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 procedure for unifying lists is essentially recursive. The heads of two lists are compared, and if they unify, then their tails are compared. Since the tail of a list is itself a list, the procedure for unifying lists is re-entered. The recursion is ultimately terminated when the tails of both lists are null, or empty, because all the items have been compared and have been found to unify. If the items in both lists are elementary terms, then the unification of each pair of terms from the two lists consists just of matching the elementary terms. The two lists then unify if all their items can be unified. If, however, a pair of items is encountered that do not unify, then no further pairs of items, should there be any, are compared. In this event, the lists cannot be unified.

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

The unification procedures outlined so far proceed as has been described when an item of a list, or an argument of a structure, is a bound or instantiated variable. For example, if an argument of one structure is a variable that has been previously instantiated with an atom, and the corresponding argument of the second structure is an atom, then the arguments unify if the atom in the second structure matches the atom instantiated on the variable in the first structure. The arguments also unify if the argument in the second structure is a variable that has been instantiated with the same atom as has been instantiated on the variable in the first structure. The process is the same when the variables have been instantiated with lists or structures; but, the appropriate procedure for unifying lists or structures must be invoked.

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 unification of structures is the principal operation undertaken by the Prolog interpreter. The interpreter, or Listener, employs the unification of structures to answer queries and to test or prove claims. A query or claim consists of one or more structures called goals, and the statements of a Prolog program consist of sequences of structures. Facts consist just of a structure (followed by a period, of course); rules consist of a head structure, and a neck, followed by a tail comprised of a sequence of goal structures. In responding to a query, or in proving a claim, the Listener first attempts to unify each goal structure in the query or claim with a structure comprising a fact or the head of a rule among the statements of a Prolog program. In undertaking this process, the Listener begins with the first statement of the program, and works its way through the statements until it succeeds in unifying the goal with the head of a rule, or with a fact, or until it encounters the end of the program.

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

Linguistics 482 Prolog Introductory Notes Top of Page