[1][2] 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.
[3] 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.
[4][5] A similar notion is that of a Herbrand universe in logic, usually used under this name in logic programming,[6] which is (absolutely freely) defined starting from the set of constants and function symbols in a set of clauses.
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.
[7][8] 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.
is a set of function symbols, with each having an associated arity (i.e. number of inputs).
denote the function symbols in
A constant is a function symbol of arity 0.
is the set of all well-formed strings that can be constructed using the variable symbols of
is the smallest set such that: The term algebra
that maps each expression to its string representation.
: As an example type inspired from integer arithmetic can be defined by
has the natural numbers as its domain and interprets
We use red color to flag its members, which otherwise may be hard to recognize due to their uncommon syntactic form.
corresponds to a mathematical expression built from the admitted symbols and written in Polish prefix notation; for example, the term
in usual infix notation.
No parentheses are needed to avoid ambiguities in Polish notation; e.g. the infix expression
To give some counter-examples, we have e.g. Now that the term set
is established, we consider the term algebra
as its domain, on which addition and multiplication need to be defined.
; similarly, the multiplication function
As an example for unique extendability of a homomorphism consider
defines an assignment of values to variable symbols, and once this is done, every term from
The signature σ of a language is a triple
In the case of logic with equality, it also contains all equations of the form t1 = t2, where t1 and t2 contain no variables.
Term algebras can be shown decidable using quantifier elimination.
The complexity of the decision problem is in NONELEMENTARY because binary constructors are injective and thus pairing functions.