Herbrand Terms

Herbrand terms are a representation of finite trees. Technically, they are non-interpreted function symbols of first-order logic, but their main use, and the approach we will follow in presenting them, is as constructors of data structures. They are interesting because they are present in all the CLP languages, which means that data structuring and abstraction is handled uniformly in all CLP languages. Moreover, Herbrand terms themselves can be viewed as a constraint system itself, where the only constraint allowed is the syntactic equality (very similar to the one in the first language we presented--actually, the data in that language was a simplification of Herbrand terms).

A formal definition of a Herbrand term is:

• A variable is a Herbrand term
• A constant is a Herbrand term
• A function symbol f with arity n applied to n terms is a Herbrand term: $f(t_1, t_2,\ldots t_n)$

For example, following the syntax for variables and constants presented in Section 2.1, the following are examples of Herbrand terms (which we will call henceforth only ``terms''):

X
mum
45
identity(Name, Number)
task(Start, End, window(front), needs_carpenter)
f(a, X, g(Y, t))

Terms represent trees in a flattened, text-only form. Figure 3.3 shows a tree-like depiction for the last term in the previous list. The function symbols in the written form correspond to nodes of the tree; their arity correspond to the number of subtrees rooted at that node. From a data structures point of view, the atoms correspond to closed nodes, where the tree cannot grow, and the variables represent open nodes, which can be further instantiated (i.e., bound to another term) to produce a larger tree.

  

Figure 3.3: A tree corresponding to a term