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.

Decidability of term algebras

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

Herbrand base

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(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.

See also

References

  1. ↑ Wilifrid Hodges (1997). A Shorter Model Theory. Cambridge University Press. p. 14. ISBN 0-521-58713-1.
  2. ↑ Franz Baader; Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press. p. 49. ISBN 0-521-77920-0.
  3. ↑ Klaus Denecke; Shelly L. Wismath (2009). Universal algebra and coalgebra. World Scientific. pp. 21–23. ISBN 978-981-283-745-5.
  4. ↑ 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.
  5. ↑ 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.
  6. ↑ Dirk van Dalen (2004). Logic and structure. Springer. p. 108. ISBN 978-3-540-20879-2.
  7. ↑ M. Ben-Ari (2001). Mathematical logic for computer science. Springer. pp. 148–150. ISBN 978-1-85233-319-5.
  8. ↑ Monroe Newborn (2001). Automated theorem proving: theory and practice. Springer. p. 43. ISBN 978-0-387-95075-4.
  9. ↑ Jeanne Ferrante, Charles W. Rackoff: The computational complexity of logical theories, Springer (1979)
  10. ↑ Rogelio Davila AnsProlog, an overview

Further reading

This article is issued from Wikipedia - version of the Friday, April 08, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.