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)
“Histories are more full of examples of the fidelity of dogs than of friends.”
—Alexander Pope (1688–1744)
“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)
“An evident principle ... is the principle of justice to all peoples and nationalities, and their right to live on equal terms of liberty and safety with one another, whether they be strong or weak.”
—Woodrow Wilson (1856–1924)