Term algebra
From Wikipedia, the free encyclopedia
In universal algebra and mathematical logic, a term algebra or Herbrand universe is a freely generated algebraic structure. For example, in a signature consisting of a single binary relation, the term algebra over a set X of variables is exactly the free magma generated by X.
Term algebras 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.
The Herbrand base is analogous to the Herbrand universe, but consists of formulas. It is the set of all ground atoms.
Contents |
[edit] Definition
Given a signature σ and a set X of variables, the term algebra over X (of signature σ) consists of all σ-terms that contain at most the variables in X. Formally, it is the smallest set Tσ(X) with the following properties:
- Tσ(X) contains X as a subset.
- For every n-ary function f in σ and all strings a1, …, an in Tσ(X), the string f(a1, …, an) is also in Tσ(X).
It follows from the second condition that Tσ(X) contains the constants of σ as a subset.
If X is empty and σ contains no constant symbols, the term algebra over X is also empty. The term algebra over X is finite if and only if σ and X are finite and σ contains no function symbols other than constant symbols.
The Herbrand universe of signature σ is the term algebra over the empty set, i.e. it consists of all ground terms of the signature. Instead of working with the term algebra over a set X, it is customary in mathematical logic to treat the elements of X as constants and use the Herbrand universe of the extended signature σ 
X. The Herbrand universe is named after Jacques Herbrand.
[edit] Decidability of term algebras
Term algebras can be shown decidable using quantifier elimination. The complexity of the decision problem is in NONELEMENTARY.[1]
[edit] Herbrand base
The Herbrand base of 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. In the case of logic with equality, it also contains all equations of the form t1=t2, where t1 and t2 contain no variables.
[edit] See also
[edit] References
- ^ Jeanne Ferrante, Charles W. Rackoff: The computational complexity of logical theories, Springer (1979)
- Anatolii Ivanovic Mal'cev: "The Metamathematics of Algebraic Systems". North-Holland, 1971. (Studies in Logic and The Foundations of Mathematics, Volume 66)
- Weistein, Eric W., "Herbrand Universe" from MathWorld.
[edit] External links
The Herbrand Universe, Herbrand Base and Herbrand Interpretations Some examples.
 |
This logic-related article is a stub. You can help Wikipedia by expanding it. |
