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:
“Histories are more full of examples of the fidelity of dogs than of friends.”
—Alexander Pope (1688–1744)
“No rules exist, and examples are simply life-savers answering the appeals of rules making vain attempts to exist.”
—André Breton (1896–1966)
“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)
“I hope that you live on good terms with yourself and the gods.”
—Henry David Thoreau (1817–1862)