Prolog has a particularly simple idea of equality, namely structural equality by pattern matching. This means that two terms are equal if and only if they have exactly the same structure. No evaluation of any kind is perfomed on them:
?- 3 = 3. Yes. ?- 3 = 4. No. ?- hello = hello. Yes. ?- hello = 3. No. ?- foo(a,2) = foo(a,2). Yes. ?- foo(a,2) = foo(b,2). No. ?- foo(a,2) = foo(a,2,c). No. ?- foo(3,4) = 7. No. ?- +(3,4) = 7. No. ?- 3 + 4 = 7. No.
Note in particular the last two examples (which are equivalent): there is no automatic arithmetic evaluation. The term +(3,4) is simply a data structure with two arguments, and therefore of course different from any number.
Note also that we have used the built-in predicate =/2, which exactly implements this idea of equality.
So far we have only performed tests, giving only Yes/No results. How can we compute more interesting results? The solution is to introduce Logical Variables. It is very important to understand that Logical Variables are variables in the mathematical sense, not in the usual programming language sense. Logical Variables are simply placeholders for values which are not yet known, like in mathematics. In conventional programming languages on the other hand, variables are labels for storage locations. The important difference is that the value of a logical variables is typically unknown at the beginning, and only becomes known in the course of the computation. Once it is known, the variable is just an alias for the value, i.e. it refers to a term. Once a value has been assigned to a logical variable, it remains fixed and cannot be assigned a different value.
Logical Variables are written beginning with an upper-case letter or an underscore, for example
X Var Quark _123 R2D2
If the same name occurs repeatedly in the same input term (e.g. the same query or clause), it denotes the same variable.
With logical variables, the above equality tests become much more interesting, resulting in the concept of Unification. Unification is an extension of the idea of pattern matching of two terms. In addition to matching, unification also causes the binding (instantiation, aliasing) of variables in the two terms. Unification instantiates variables such that the two unified terms become equal. For example
X = 7 is true with X instantiated to 7 X = Y is true with X aliased to Y (or vice versa) foo(X) = foo(7) is true with X instantiated to 7 foo(X,Y) = foo(3,4) is true with X instantiated to 3 and Y to 4 foo(X,4) = foo(3,Y) is true with X instantiated to 3 and Y to 4 foo(X) = foo(Y) is true with X aliased to Y (or vice versa) foo(X,X) = foo(3,4) is false because there is no possible value for X foo(X,4) = foo(3,X) is false because there is no possible value for X
- Predicate
- Something that is true or false, depending on its definition and its arguments. Defines a relationship between its arguments.
- Goal
- A logical formula whose truth value we want to know. A goal can be a conjunction or disjunction of other (sub-)goals.
- Query
- The initial Goal given to a computation.
- Unification
- An extension of pattern matching which can bind logical variables (placeholders) in the matched terms to make them equal.
- Clause
- One alternative definition for when a predicate is true. A clause is logically an implication rule.
Figure 3.2: Basic Terminology