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 τ {\displaystyle \tau } is a set of function symbols, with each having an associated arity (i.e. number of inputs). For any non-negative integer n {\displaystyle n} , let τ n {\displaystyle \tau _{n}} denote the function symbols in τ {\displaystyle \tau } of arity n {\displaystyle n} . A constant is a function symbol of arity 0. Let τ {\displaystyle \tau } be a type, and let X {\displaystyle X} be a non-empty set of symbols, representing the variable symbols. (For simplicity, assume X {\displaystyle X} and τ {\displaystyle \tau } are disjoint.) Then the set of terms T ( X ) {\displaystyle T(X)} of type τ {\displaystyle \tau } over X {\displaystyle X} is the set of all well-formed strings that can be constructed using the variable symbols of X {\displaystyle X} and the constants and operations of τ {\displaystyle \tau } . Formally, T ( X ) {\displaystyle T(X)} is the smallest set such that:
X ∪ τ 0 ⊆ T ( X ) {\displaystyle X\cup \tau _{0}\subseteq T(X)} — each variable symbol from X {\displaystyle X} is a term in T ( X ) {\displaystyle T(X)} , and so is each constant symbol from τ 0 {\displaystyle \tau _{0}} . For all n ≥ 1 {\displaystyle n\geq 1} and for all function symbols f ∈ τ n {\displaystyle f\in \tau _{n}} and terms t 1 , . . . , t n ∈ T ( X ) {\displaystyle t_{1},...,t_{n}\in T(X)} , we have the string f ( t 1 , . . . , t n ) ∈ T ( X ) {\displaystyle f(t_{1},...,t_{n})\in T(X)} — given n {\displaystyle n} terms t 1 , . . . , t n {\displaystyle t_{1},...,t_{n}} , the application of an n {\displaystyle n} -ary function symbol f {\displaystyle f} to them represents again a term. The term algebra T ( X ) {\displaystyle {\mathcal {T}}(X)} of type τ {\displaystyle \tau } over X {\displaystyle X} is, in summary, the algebra of type τ {\displaystyle \tau } that maps each expression to its string representation. Formally, T ( X ) {\displaystyle {\mathcal {T}}(X)} is defined as follows:
… excerpt ends here. Continue reading the full article.
