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

Universal algebra

edit

A type   is a set of function symbols, with each having an associated arity (i.e. number of inputs). For any non-negative integer  , let   denote the function symbols in   of arity  . A constant is a function symbol of arity 0.

Let   be a type, and let   be a non-empty set of symbols, representing the variable symbols. (For simplicity, assume   and   are disjoint.) Then the set of terms   of type   over   is the set of all well-formed strings that can be constructed using the variable symbols of   and the constants and operations of  . Formally,   is the smallest set such that:

  •     — each variable symbol from   is a term in  , and so is each constant symbol from  .
  • For all   and for all function symbols   and terms  , we have the string     — given   terms  , the application of an  -ary function symbol   to them represents again a term.

The term algebra   of type   over   is, in summary, the algebra of type   that maps each expression to its string representation. Formally,   is defined as follows:[9]

  • The domain of   is  .
  • For each nullary function   in  ,   is defined as the string  .
  • For all   and for each n-ary function   in   and elements   in the domain,   is defined as the string  .

A term algebra is called absolutely free because for any algebra   of type  , and for any function  ,   extends to a unique homomorphism  , which simply evaluates each term   to its corresponding value  . Formally, for each  :

  • If  , then  .
  • If  , then  .
  • If   where   and  , then  .

Example

edit

As an example type inspired from integer arithmetic can be defined by  ,  ,  , and   for each  .

The best-known algebra of type   has the natural numbers as its domain and interprets  ,  ,  , and   in the usual way; we refer to it as  .

For the example variable set  , we are going to investigate the term algebra   of type   over  .

First, the set   of terms of type   over   is considered. We use red color to flag its members, which otherwise may be hard to recognize due to their uncommon syntactic form. We have e.g.

  •  , since   is a variable symbol;
  •  , since   is a constant symbol; hence
  •  , since   is a 2-ary function symbol; hence, in turn,
  •   since   is a 2-ary function symbol.

More generally, each string in   corresponds to a mathematical expression built from the admitted symbols and written in Polish prefix notation; for example, the term   corresponds to the expression   in usual infix notation. No parentheses are needed to avoid ambiguities in Polish notation; e.g. the infix expression   corresponds to the term  .

To give some counter-examples, we have e.g.

  •  , since   is neither an admitted variable symbol nor an admitted constant symbol;
  •  , for the same reason,
  •  , since   is a 2-ary function symbol, but is used here with only one argument term (viz.  ).

Now that the term set   is established, we consider the term algebra   of type   over  . This algebra uses   as its domain, on which addition and multiplication need to be defined. The addition function   takes two terms   and   and returns the term  ; similarly, the multiplication function   maps given terms   and   to the term  . For example,   evaluates to the term  . Informally, the operations   and   are both "sluggards" in that they just record what computation should be done, rather than doing it.

As an example for unique extendability of a homomorphism consider   defined by   and  . Informally,   defines an assignment of values to variable symbols, and once this is done, every term from   can be evaluated in a unique way in  . For example,

 

In a similar way, one obtains  .

Herbrand base

edit

The signature σ of a language is a triple <O, F, P> consisting of the alphabet of constants O, function symbols F, and 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.

Decidability

edit

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.[11]

See also

edit

References

edit
  1. ^ Wilfrid Hodges (1997). A Shorter Model Theory. Cambridge University Press. pp. 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 (2010). A Unifying Framework for Structured Analysis and Design Models: An Approach Using Initial Algebra Semantics and Category Theory. Cambridge University Press. pp. 46–47. doi:10.1017/CBO9780511569890. ISBN 978-0-511-56989-0.
  5. ^ Jean-Yves Béziau (1999). "The mathematical structure of logical syntax". In Carnielli, Walter Alexandre; D'Ottaviano, Itala M. L. (eds.). Advances in Contemporary Logic and Computer Science: Proceedings of the Eleventh Brazilian Conference on Mathematical Logic, May 6-10, 1996, Salvador, Bahia, Brazil. American Mathematical Society. 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. ^ Stanley Burris; H. P. Sankappanavar (1981). A Course in Universal Algebra. Springer. pp. 68–69, 71. ISBN 978-1-4613-8132-7.{{cite book}}: CS1 maint: multiple names: authors list (link)
  10. ^ Rogelio Davila. Answer Set Programming Overview.
  11. ^ Jeanne Ferrante; Charles W. Rackoff (1979). The Computational Complexity of Logical Theories. Springer, Chapter 8, Theorem 1.2.

Further reading

edit
edit