Term algebra

{{Short description|Freely generated algebraic structure over a given signature}} In universal algebra and mathematical logic, a '''term algebra''' is a freely generated algebraic structure over a given signature.<ref>{{cite book|author1=Wilfrid Hodges|title=A Shorter Model Theory|url=https://archive.org/details/shortermodeltheo00hodg|url-access=limited|year=1997|publisher=Cambridge University Press|isbn=0-521-58713-1|pages=[https://archive.org/details/shortermodeltheo00hodg/page/n61 14]}}</ref><ref>{{cite book|author1=Franz Baader|author2-link=Tobias Nipkow|author2=Tobias Nipkow|title=Term Rewriting and All That|year=1998|publisher=Cambridge University Press|isbn=0-521-77920-0|pages=49|url=https://books.google.com/books?id=N7BvXVUCQk8C&q=%22Term+algebra%22|author1-link=Franz Baader}}</ref> 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'''.<ref name="DeneckeWismath2009">{{cite book|author1=Klaus Denecke|author2=Shelly L. Wismath|title=Universal Algebra and Coalgebra|url=https://books.google.com/books?id=NgTAzhC8jVAC&pg=PA21|year=2009|publisher=World Scientific|isbn=978-981-283-745-5|pages=21–23}}</ref>

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.<ref name="Tse2010">{{cite book|author=T.H. Tse|title=A Unifying Framework for Structured Analysis and Design Models: An Approach Using Initial Algebra Semantics and Category Theory|year=2010|publisher=Cambridge University Press|isbn=978-0-511-56989-0|pages=46–47|doi=10.1017/CBO9780511569890|author-link=T.H. Tse}}</ref><ref name="CarnielliD'Ottaviano1999">{{cite book|editor1-first=Walter Alexandre|editor1-last=Carnielli|editor2-first=Itala M. L.|editor2-last=D'Ottaviano|editor2-link=Itala D'Ottaviano|title=Advances in Contemporary Logic and Computer Science: Proceedings of the Eleventh Brazilian Conference on Mathematical Logic, May 6-10, 1996, Salvador, Bahia, Brazil|chapter-url=https://books.google.com/books?id=tEU9OcjwhXUC&pg=PA9|access-date=18 April 2011|year=1999|publisher=American Mathematical Society|isbn=978-0-8218-1364-5|page=9|chapter=The mathematical structure of logical syntax|author=Jean-Yves Béziau|author-link=Jean-Yves Béziau}}</ref>

A similar notion is that of a ''Herbrand universe'' in logic, usually used under this name in logic programming,<ref name="Dalen2004">{{cite book|author=Dirk van Dalen|title=Logic and Structure|url=https://books.google.com/books?id=4u9gQ6pctuIC&pg=PA108|year=2004|publisher=Springer|isbn=978-3-540-20879-2|page=108}}</ref> 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.<ref name="Ben-Ari2001">{{cite book|author=M. Ben-Ari|title=Mathematical Logic for Computer Science|url=https://books.google.com/books?id=hzWlEy1qqR8C&pg=PA148|year=2001|publisher=Springer|isbn=978-1-85233-319-5|pages=148–150}}</ref><ref name="Newborn2001">{{cite book|author=Monroe Newborn|title=Automated Theorem Proving: Theory and Practice|url=https://books.google.com/books?id=Kwv1_UXYE8QC&pg=PA43|year=2001|publisher=Springer|isbn=978-0-387-95075-4|page=43}}</ref> 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''' <math>\tau</math> is a set of function symbols, with each having an associated arity (i.e. number of inputs). For any non-negative integer <math>n</math>, let <math>\tau_n</math> denote the function symbols in <math>\tau</math> of arity <math>n</math>. A constant is a function symbol of arity 0.

Let <math>\tau</math> be a type, and let <math>X</math> be a non-empty set of symbols, representing the variable symbols. (For simplicity, assume <math>X</math> and <math>\tau</math> are disjoint.) Then the '''set of terms''' <math>T(X)</math> of type <math>\tau</math> over <math>X</math> is the set of all well-formed strings that can be constructed using the variable symbols of <math>X</math> and the constants and operations of <math>\tau</math>. Formally, <math>T(X)</math> is the smallest set such that: * <math>X \cup \tau_0 \subseteq T(X)</math>   — each variable symbol from <math>X</math> is a term in <math>T(X)</math>, and so is each constant symbol from <math>\tau_0</math>. * For all <math>n \geq 1</math> and for all function symbols <math>f \in \tau_n</math> and terms <math>t_1, ..., t_n \in T(X)</math>, we have the string <math>f(t_1, ..., t_n) \in T(X)</math>   — given <math>n</math> terms <math>t_1, ..., t_n</math>, the application of an <math>n</math>-ary function symbol <math>f</math> to them represents again a term.

The '''term algebra''' <math>\mathcal{T}(X)</math> of type <math>\tau</math> over <math>X</math> is, in summary, the algebra of type <math>\tau</math> that maps each expression to its string representation. Formally, <math>\mathcal{T}(X)</math> is defined as follows:<ref name="Burris1981">{{cite book|author=Stanley Burris; H. P. Sankappanavar|title=A Course in Universal Algebra |url=https://link.springer.com/book/9781461381327|year=1981|publisher=Springer|isbn=978-1-4613-8132-7|pages=68–69, 71}}</ref> * The domain of <math>\mathcal{T}(X)</math> is <math>T(X)</math>. * For each nullary function <math>f</math> in <math>\tau_0</math>, <math>f^{\mathcal{T}(X)}()</math> is defined as the string <math>f</math>. * For all <math>n \geq 1</math> and for each ''n''-ary function <math>f</math> in <math>\tau</math> and elements <math>t_1, ..., t_n</math> in the domain, <math>f^{\mathcal{T}(X)}(t_1, ..., t_n)</math> is defined as the string <math>f(t_1, ..., t_n)</math>.

A term algebra is called ''absolutely free'' because for any algebra <math>\mathcal{A}</math> of type <math>\tau</math>, and for any function <math>g : X \to \mathcal{A}</math>, <math>g</math> extends to a unique homomorphism <math>g^\ast : \mathcal{T}(X) \to \mathcal{A}</math>, which simply evaluates each term <math>t \in \mathcal{T}(X)</math> to its corresponding value <math>g^\ast(t) \in \mathcal{A}</math>. Formally, for each <math>t \in \mathcal{T}(X)</math>: * If <math>t \in X</math>, then <math>g^\ast(t) = g(t)</math>. * If <math>t = f \in \tau_0</math>, then <math>g^\ast(t) = f^\mathcal{A}()</math>. * If <math>t = f(t_1, ..., t_n)</math> where <math>f \in \tau_n</math> and <math>n \geq 1</math>, then <math>g^\ast(t) = f^\mathcal{A}(g^\ast(t_1), ..., g^\ast(t_n))</math>.

==Example== An example type inspired by integer arithmetic can be defined by <math>\tau_0 = \{ 0,1 \}</math>, <math>\tau_1=\{\}</math>, <math>\tau_2=\{ +,* \}</math>, and <math>\tau_i=\{\}</math> for each <math>i > 2</math>.

The best-known algebra of type <math>\tau</math> has the natural numbers as its domain and interprets <math>0</math>, <math>1</math>, <math>+</math>, and <math>*</math> in the usual way; we refer to it as <math>\mathcal{A}_{nat}</math>.

For the example variable set <math>X = \{ x,y \}</math>, we are going to investigate the term algebra <math>\mathcal{T}(X)</math> of type <math>\tau</math> over <math>X</math>.

First, the set <math> T(X)</math> of terms of type <math>\tau</math> over <math>X</math> is considered. We use {{color|red|red color}} to flag its members, which otherwise may be hard to recognize due to their uncommon syntactic form. We have e.g. * <math>{\color{red}x} \in T(X)</math>, since <math>x \in X</math> is a variable symbol; * <math>{\color{red}1} \in T(X)</math>, since <math>1 \in \tau_0</math> is a constant symbol; hence * <math>{\color{red}+x1} \in T(X)</math>, since <math>+</math> is a 2-ary function symbol; hence, in turn, * <math>{\color{red}*+x1x} \in T(X)</math> since <math>*</math> is a 2-ary function symbol. More generally, each string in <math>T(X)</math> corresponds to a mathematical expression built from the admitted symbols and written in Polish prefix notation; for example, the term <math>{\color{red}*+x1x}</math> corresponds to the expression <math>(x+1)*x</math> in usual infix notation. No parentheses are needed to avoid ambiguities in Polish notation; e.g. the infix expression <math>x+(1*x)</math> corresponds to the term <math>{\color{red}+x*1x}</math>.

To give some counter-examples, we have e.g. * <math>{\color{red}z} \not\in T(X)</math>, since <math>z</math> is neither an admitted variable symbol nor an admitted constant symbol; * <math>{\color{red}3} \not\in T(X)</math>, for the same reason, * <math>{\color{red}+1} \not\in T(X)</math>, since <math>+</math> is a 2-ary function symbol, but is used here with only one argument term (viz. <math>{\color{red}1}</math>).

Now that the term set <math> T(X)</math> is established, we consider the term algebra <math>\mathcal{T}(X)</math> of type <math>\tau</math> over <math>X</math>. This algebra uses <math>T(X)</math> as its domain, on which addition and multiplication need to be defined. The addition function <math>+^{\mathcal{T}(X)}</math> takes two terms <math>p</math> and <math>q</math> and returns the term <math>{\color{red}+}pq</math>; similarly, the multiplication function <math>*^{\mathcal{T}(X)}</math> maps given terms <math>p</math> and <math>q</math> to the term <math>{\color{red}*}pq</math>. For example, <math>*^{\mathcal{T}(X)}( {\color{red}+x1} , {\color{red}x} )</math> evaluates to the term <math>{\color{red}*+x1x}</math>. Informally, the operations <math>+^{\mathcal{T}(X)}</math> and <math>*^{\mathcal{T}(X)}</math> 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 <math>g: X \to \mathcal{A}_{nat}</math> defined by <math>g(x) = 7</math> and <math>g(y) = 3</math>. Informally, <math>g</math> defines an assignment of values to variable symbols, and once this is done, every term from <math>T(X)</math> can be evaluated in a unique way in <math>\mathcal{A}_{nat}</math>. For example, :<math>\begin{array}{lll} & g^*({\color{red}+x1}) \\ = & g^*({\color{red}x}) + g^*({\color{red}1}) & \text{ since } g^* \text{ is a homomorphism } \\ = & g({\color{red}x}) + g^*({\color{red}1}) & \text{ since } g^* \text{ coincides on } X \text{ with } g \\ = & 7 + g^*({\color{red}1}) & \text{ by definition of } g \\ = & 7 + 1 & \text{ since } g^* \text{ is a homomorphism } \\ = & 8 & \text{ according to the well-known arithmetical rules in } \mathcal{A}_{nat} \\ \end{array}</math> In a similar way, one obtains <math>g^*({\color{red}*+x1x}) = ... = 8 * g({\color{red}x}) = ... = 56</math>.

==Herbrand base== {{Main| Herbrand interpretation | Herbrand structure}} 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'''<ref>Rogelio Davila. [http://www.rogeliodavila.com.mx/Programacion%20Logica/PL%20Notas/AnsProlog%20Overview.ppt Answer Set Programming Overview].</ref> of a signature ''σ'' consists of all ground atoms of ''σ'': 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.

==Decidability== {{Confusing|talk=|date=October 2018}}

The first-order theory of any term algebra can be shown to be decidable using quantifier elimination. The complexity of the decision problem is in NONELEMENTARY because binary constructors are injective and thus pairing functions.<ref>Jeanne Ferrante; Charles W. Rackoff (1979). ''The Computational Complexity of Logical Theories''. Springer, Chapter 8, Theorem 1.2.</ref>

==See also== * Answer-set programming * Clone (algebra) * Domain of discourse / Universe (mathematics) * Rabin's tree theorem (the monadic theory of the infinite complete binary tree is decidable) * Initial algebra * Abstract data type * Term rewriting system

==References== {{Reflist}} {{Refbegin}}

==Further reading== * Joel Berman (2005). [http://homepages.math.uic.edu/~berman/structure-free.pdf "The structure of free algebras"]. In ''Structural Theory of Automata, Semigroups, and Universal Algebra''. Springer. pp. 47–76. {{MR|2210125}}.

==External links== * {{mathworld|urlname=HerbrandUniverse|title=Herbrand Universe}}

Category:Universal algebra Category:Mathematical logic Category:Free algebraic structures Category:Unification (computer science)