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)
“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)
“Books have their destinies like men. And their fates, as made by generations of readers, are very different from the destinies foreseen for them by their authors. Gulliver’s Travels, with a minimum of expurgation, has become a children’s book; a new illustrated edition is produced every Christmas. That’s what comes of saying profound things about humanity in terms of a fairy story.”
—Aldous Huxley (1894–1963)