Term algebra
In universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X. Other synonyms for the notion include absolutely free algebra and anarchic algebra.

From a category theory perspective, a term algebra is the initial object for the category of all X-generated algebras of the same signature, and this object, unique up to isomorphism, is called an initial algebra; it generates by homomorphic projection all algebras in the category.

A similar notion is that of a Herbrand universe in logic, usually used under this name in logic programming, which is (absolutely freely) defined starting from the set of constants and function symbols in a set of clauses. That is, the Herbrand universe consists of all ground terms: terms that have no variables in them.

An atomic formula or atom is commonly defined as a predicate applied to a tuple of terms; a ground atom is then a predicate in which only ground terms appear. The Herbrand base is the set of all ground atoms that can be formed from predicate symbols in the original set of clauses and terms in its Herbrand universe. These two concepts are named after Jacques Herbrand.

Term algebras also play a role in the semantics of abstract data types, where an abstract data type declaration provides the signature of a multi-sorted algebraic structure and the term algebra is a concrete model of the abstract declaration.

Universal algebra
A type  is a set of function symbols along with their associated arities. For any non-negative integer , let  denote the function symbols in  of arity . A function of arity 0 is treated as a constant.

Let  be a type, and let  be a non-empty set of symbols, representing the variable symbols. (For simplicity, assume  and  are disjoint.) Then the set of terms  of type  over  is the smallest set such that:
 .
 For all  and for all function symbols  and terms , we have the string .

The term algebra  of type  over  is defined as follows:
 The domain of  is .
 For each nullary function  in ,  is defined as the string .
 For all  and for each n-ary function  in  and elements  in the domain,  is defined as the string .

A term algebra is called absolutely free because for any algebra  of type , and for any function ,  extends to a unique homomorphism , which simply evaluates each term  to its corresponding value . Formally, for each :
 If , then .
 If , then .
 If  where  and , then .

Herbrand base

The signature σ of a language is a triple <O, F, P> consisting of the alphabet of constants O, function symbols F, and predicates P. The Herbrand base of a signature σ consists of all ground atoms of σ: of all formulas of the form R(t1, …, tn), where t1, …, tn are terms containing no variables (i.e. elements of the Herbrand universe) and R is an n-ary relation symbol (i.e. predicate). In the case of logic with equality, it also contains all equations of the form t1 = t2, where t1 and t2 contain no variables.

Decidability

Term algebras can be shown decidable using quantifier elimination. The complexity of the decision problem is in NONELEMENTARY.

See also
 Answer-set programming
 Clone (algebra)
 Domain of discourse / Universe (mathematics)
 Rabin's tree theorem (the monadic theory of the infinite complete binary tree is decidable)
 Initial algebra
 Abstract data type
 Term rewriting system

References

Further reading
 Joel Berman (2005). "The structure of free algebras". In Structural Theory of Automata, Semigroups, and Universal Algebra. Springer. pp. 47-76. .

External links
 

Universal algebra
Mathematical logic
Free algebraic structures
Unification (computer science)