# Term algebra

In universal algebra and mathematical logic, a **term algebra** is a freely generated algebraic structure over a given signature.^{[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**, **anarchic algebra**.^{[3]}

From a category theory perspective, a term algebra is the initial object for the category of all 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. 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.^{[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.

## Contents

## Decidability of term algebras[edit]

Term algebras can be shown decidable using quantifier elimination. The complexity of the decision problem is in NONELEMENTARY.^{[9]}

## Herbrand base[edit]

The **signature** σ of a language is a triple <O,F,P> consisting of the alphabet of constants *O*, the function symbols *F*, and the predicates *P*. The **Herbrand base**^{[10]} of a signature σ consists of all ground atoms of σ: of all formulas of the form *R*(*t*_{1}, …, *t*_{n}), where *t*_{1}, …, *t*_{n} 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 *t*_{1}=*t*_{2}, where *t*_{1} and *t*_{2} contain no variables.

## See also[edit]

- Clone (algebra)
- Answer-set programming
- Domain of discourse / Universe (mathematics)
- Herbrand interpretation / Herbrand structure
- Rabin's tree theorem (the monadic theory of the infinite complete binary tree is decidable)
- Universal algebra

## References[edit]

**^**Wilifrid Hodges (1997).*A Shorter Model Theory*. Cambridge University Press. p. 14. ISBN 0-521-58713-1.**^**Franz Baader; Tobias Nipkow (1998).*Term Rewriting and All That*. Cambridge University Press. p. 49. ISBN 0-521-77920-0.**^**Klaus Denecke; Shelly L. Wismath (2009).*Universal algebra and coalgebra*. World Scientific. pp. 21–23. ISBN 978-981-283-745-5.**^**T. H. Tse (1991).*A unifying framework for structured analysis and design models: an approach using initial algebra semantics and category theory*. Cambridge University Press. pp. 46–47. ISBN 978-0-521-39196-2.**^**Jean-Yves Béziau (1999). "The mathematical structure of logical syntax". In Walter Alexandre Carnielli, Itala M. L. D'Ottaviano.*Advances in contemporary logic and computer science: proceedings of the Eleventh Brazilian Conference on Mathematical Logic, May 6-10, 1996, Salvador, Bahia, Brazil*. AMS Bookstore. p. 9. ISBN 978-0-8218-1364-5. Retrieved 18 April 2011.**^**Dirk van Dalen (2004).*Logic and structure*. Springer. p. 108. ISBN 978-3-540-20879-2.**^**M. Ben-Ari (2001).*Mathematical logic for computer science*. Springer. pp. 148–150. ISBN 978-1-85233-319-5.**^**Monroe Newborn (2001).*Automated theorem proving: theory and practice*. Springer. p. 43. ISBN 978-0-387-95075-4.**^**Jeanne Ferrante, Charles W. Rackoff: The computational complexity of logical theories, Springer (1979)**^**Rogelio Davila AnsProlog, an overview

## Further reading[edit]

- Joel Berman. The structure of free algebras. In Structural theory of automata, semigroups, and universal algebra, pages 47–76. Springer, Dordrecht, 2005. MR2210125