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)
“In the examples that I here bring in of what I have [read], heard, done or said, I have refrained from daring to alter even the smallest and most indifferent circumstances. My conscience falsifies not an iota; for my knowledge I cannot answer.”
—Michel de Montaigne (1533–1592)
“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)
“If men do not keep on speaking terms with children, they cease to be men, and become merely machines for eating and for earning money.”
—John Updike (b. 1932)