Examples of Syntactic Unification of First-order Terms
In the Prolog syntactical convention a symbol starting with an upper case letter is a variable name; a symbol that starts with a lowercase letter is a function symbol; the comma is used as the logical and operator. In maths the convention is to use lower case letters at the end of the alphabet as variable names (e.g. x,y,z); letters f,g,h as function symbols, and letters a,b,c as constants, and constants are often regarded as functions that take no arguments; logical "and" is represented by & or
| Prolog Notation | Maths Notation | Unifying Substitution | Explanation |
|---|---|---|---|
| a = a | a = a | Succeeds. (tautology) | |
| a = b | a = b | fail | a and b do not match |
| X = X | x = x | Succeeds. (tautology) | |
| a = X | a = x | x is unified with the constant a | |
| X = Y | x = y | x and y are aliased | |
| f(a,X) = f(a,b) | f(a,x) = f(a,b) | function and constant symbols match, x is unified with the constant b | |
| f(a) = g(a) | f(a) = g(a) | fail | f and g do not match |
| f(X) = f(Y) | f(x) = f(y) | x and y are aliased | |
| f(X) = g(Y) | f(x) = g(y) | fail | f and g do not match |
| f(X) = f(Y,Z) | f(x) = f(y,z) | fail | Fails. The terms have different arity |
| f(g(X)) = f(Y) | f(g(x)) = f(y) | Unifies y with the term g(x) | |
| f(g(X),X) = f(Y,a) | f(g(x),x) = f(y,a) | Unifies x with constant a, and y with the term g(a) | |
| X = f(X) | x = f(x) | should fail | Fails in strict first-order logic and many modern Prolog dialects (enforced by the occurs check).
Succeeds in traditional Prolog, unifying x with infinite expression x=f(f(f(f(...)))) which is not strictly a term. |
| X = Y, Y = a | x = y & y = a | Both x and y are unified with the constant a | |
| a = Y, X = Y | a = y & x = y | As above (unification is symmetric, and transitive) | |
| X = a, b = X | x = a & b = x | fail | Fails. a and b do not match, so x can't be unified with both |
Read more about this topic: Unification (computer Science)
Famous quotes containing the words examples of, examples, syntactic and/or terms:
“There are many examples of women that have excelled in learning, and even in war, but this is no reason we should bring ‘em all up to Latin and Greek or else military discipline, instead of needle-work and housewifry.”
—Bernard Mandeville (1670–1733)
“There are many examples of women that have excelled in learning, and even in war, but this is no reason we should bring ‘em all up to Latin and Greek or else military discipline, instead of needle-work and housewifry.”
—Bernard Mandeville (1670–1733)
“The syntactic component of a grammar must specify, for each sentence, a deep structure that determines its semantic interpretation and a surface structure that determines its phonetic interpretation.”
—Noam Chomsky (b. 1928)
“One of your biggest jobs as a parent of multiples is no bigger than simply talking to your children individually and requiring that they respond to you individually as well. The benefits of this kind of communication can be enormous, in terms of the relationship you develop with each child, in terms of their language development, and eventually in terms of their sense of individuality, too.”
—Pamela Patrick Novotny (20th century)