Termalgebra

In mathematics and computer science, a free term algebra is understood to be an algebraic structure freely generated using a signature . The basic set of term algebra are the terms . The operations of term algebra have terms as arguments and return terms as result. Termalgebras provide u. a.

• an opportunity to look more closely at the process of "calculating" and interpreting a term and classifying it mathematically,
• to clarify their relationship to all other algebraic structures by displaying the terms as an algebraic structure,
• a prototype for the concept of free generation of algebraic structures.

Term algebras play a central role in universal algebra , mathematical logic and formal semantics .

Signature, term, termalgebra, basic termgebra

For an algebraic structure , its signature is first defined, i.e. the set of operation symbols together with their arity . If one also has the set of variables , then the terms are obtained as the smallest set for which the following applies: ${\displaystyle {\boldsymbol {S}}=({\mathcal {F}},\sigma )}$ ${\displaystyle {\mathcal {F}}}$ ${\displaystyle \sigma \colon {\mathcal {F}}\to \mathbb {N} _{0}}$ ${\displaystyle X}$ ${\displaystyle T(X)}$

${\displaystyle {\begin{array}{lll}x\in X\quad &\Rightarrow \quad (0,x)&\in T(X)\\t_{1},\dotsc ,t_{n}\in T(X)\quad \wedge \quad \sigma (f)=n&\Rightarrow \quad (1,f,t_{1},\dotsc ,t_{n})&\in T(X)\end{array}}}$

The fundamental operations of free term algebra are: ${\displaystyle f_{T(x)}\in F}$ ${\displaystyle (T(X),F)}$

${\displaystyle f_{T(X)}(t_{1},\dotsc ,t_{n}):=(1,f,t_{1},\dotsc ,t_{n})}$

The free term algebra is called . In the event that the set is empty, i.e. variables are excluded, one speaks of a basic termgebra and denotes it . Unless expressly emphasized, variables are always permitted if a term algebra is used more briefly than a free term algebra. It is common to think of 0-digit operators as constants. In universal algebra, a signature is also called a type. ${\displaystyle T(X)}$ ${\displaystyle X}$ ${\displaystyle T}$

Essential property of termalgebra

With the term algebra one now has the terms generated via the type as a basic set of an algebra of the same type. This makes it possible to grasp the interpretation, i.e. the meaning of the terms, using the means of universal algebra and to consider the term algebra together with its "relatives", the algebras of the same type. The essential property of term algebra is that one can grasp the meaning of the terms as a structurally compatible mapping, as a homomorphism . At the same time, the process of calculating can be grasped by the following sentence:

Theorem: Let be a term algebra of the type about . Then for every algebra of the same type and every mapping there is exactly one homomorphism which continues , i.e. H. . ${\displaystyle T(X)}$ ${\displaystyle ({\mathcal {F}},\sigma )}$ ${\displaystyle X}$ ${\displaystyle A}$ ${\displaystyle \phi \colon X\to A}$ ${\displaystyle {\bar {\phi }}\colon T(X)\to A}$ ${\displaystyle \phi }$ ${\displaystyle {\bar {\phi }}_{|x}=\phi }$

Proof: is defined by: ${\displaystyle {\bar {\phi }}\colon T(X)\to A}$

${\displaystyle {\begin{array}{ll}{\bar {\phi }}((0,x))&:=\phi (x)\\{\bar {\phi }}((1,f,t_{1},\dotsc ,t_{n}))&:=f_{A}({\bar {\phi }}(t_{1}),\dotsc ,{\bar {\phi }}(t_{n}))\end{array}}}$

In this way it is completely defined and, because of the uniqueness of the generation, is even well-defined . Because of is a homomorphism. ${\displaystyle {\bar {\phi }}}$ ${\displaystyle T(X)}$ ${\displaystyle f_{T(X)}(t_{1},\dotsc ,t_{n}):=(1,f,t_{1},\dotsc ,t_{n})}$ ${\displaystyle {\bar {\phi }}}$ ${\displaystyle \square }$

${\displaystyle \phi }$is also called assignment (of the variables with values) and is sometimes referred to as "ass" (for assignment). The continuation is also called evaluation homomorphism and denotes it with "eval" (for English evaluation). The sentence is often found accompanied by a diagram like the one shown on the right. Herein, the embedding ( ) of in . The diagram "commutes", i.e. i.e., it applies . ${\displaystyle {\bar {\phi }}}$ ${\displaystyle i\colon X\to T(X)}$ ${\displaystyle i(x)=(0,x)}$ ${\displaystyle X}$ ${\displaystyle T(X)}$ ${\displaystyle \phi ={\bar {\phi }}\circ i}$

Categorical definition

From the above theorem it follows, without resorting to the definition, that a term algebra is isomorphic to any other algebra of the same type that satisfies this theorem. The essential property of term algebra can thus be used in a definition. As a result, instead of specifying a concrete “implementation” of the terms and operations, the statement of the above sentence is taken as the basis of the definition. The method for this is provided by category theory . The category under consideration consists of the algebras of the same type as objects and their homomorphisms as morphisms. ${\displaystyle \phi (x)=x}$

Initiality of the basic terms

In the case of the basic termgebras, the characterization is particularly simple. For an empty set of variables, the above sentence is reduced to the statement that for every algebra in the category of algebras of the same type there is exactly one homomorphism from the basic termgebra to the algebra . So the algebra of the basic terms is the initial object of this category. In this sense, the basic term algebra is also called the initial term algebra. ${\displaystyle A}$ ${\displaystyle T}$ ${\displaystyle A}$

Universal property of free term algebras

The free term algebra can be defined by the universal property shown in the picture on the right .

This diagram only differs from the one shown above in that the various categories, the algebras of the same type with their homomorphisms (left) and the category of sets and their mappings (right) are now separated into two sub-diagrams. The composition operation of the respective category can now be used in each of the sub-diagrams. Both sides are mediated by the forget function . It transfers the respective basic sets from the algebras as objects ( ) and their homomorphisms as functions ( ). ${\displaystyle U\colon Alg\to Set}$ ${\displaystyle u(x)=x}$ ${\displaystyle u(f)=f}$

Evidence

While a categorical version clearly emphasizes the special situation of the algebra of the basic terms and the free term algebra, it can only partially fulfill the promise given in the introduction to make the essential properties neutral in terms of definition. In contrast to the introductory definition, the categorical version requires as a definition a proof of existence and a proof of uniqueness, in which it must be proven that the object in question exists in the category and that the morphism is unambiguous. The proof is then carried out as above. At this point there is no way around specifying a specific presentation. However, the presentation chosen for the proof can be limited to this proof, since it completely captures the essential property of termalgebra.

Role of variables, free construction in general

Just as the intuitive idea of ​​terms as written text is initially appealed to, in many contexts terms are initially introduced as a mere syntactic construction. Understood in this way, the variables simply represent an (enumerable) set of identifiers ("a", "b", "c", ...) around which the function symbols are then written. In contexts in which terms are used as objects, this view is completely correct. The above sentence then simply describes the possibility and manner of evaluation or interpretation . But if one sticks to this idea of ​​termalgebra as a mere syntactic version of the written term, then the concept of free termalgebra as a prototype of free construction will be missed.

In free construction, the set of variables does not stand for textual variables, but is a placeholder for the basic set of any other structure around which the termalgebra is then freely constructed.

In mathematics you can find a free construction for practically every structure ( free monoid , free group , etc.), whereby free term algebra only has the special position of being particularly simple in that it brings along no further laws apart from its functions. The free construction finds its equivalent in computer science with parametric data types . Modern programming languages ​​often provide this concept in one way or another. For example, free termalgebras can be defined directly in Haskell , while the templates in C ++ offer a possibility of free construction. The type parameters then take on the role that the variable set has here.

Turned this way, the above sentence has the task of ensuring that the construction does not violate the given structure, i.e. that it remains free from the laws of the structure constructed around it. ${\displaystyle X}$

Classification and continuation

In the categorical consideration it becomes clear that free term algebras have a special position in the category of algebras of the same type insofar as every algebra of the same type can be uniquely reached from them. Since they are devoid of any further structure, they are the ideal starting point to extract other algebras from them.

In universal algebra as a sub-discipline of mathematics, a. investigates to what extent this is possible in terms of definition by specifying equations, as is the case with many algebraic structures ( groups , rings ). This leads to an equality calculus and methods to get from these equations to the algebra thus described, the quotient term algebra, which is a term algebra under the congruence generated by the equations .

This method was taken up in computer science under the title algebraic specification and allows the specification of an abstract data type . If the defining equations can be executed directly via a term rewriting system , this specification also provides an implementation at the same time .

In mathematical logic the basic termgebra is introduced within the framework of the Herbrand theory under the name Herbrand structure in order to arrive at an interpretation of predicate logic formulas.

A specialty of term algebras is that the equality of their terms coincides with their identity. Each term is the same only with itself and different from all others. This uniqueness of the representation of the terms is often used constructively, see generation system , inductive data type and structural induction .

literature

• Thomas Ihringer: General Algebra. Teubner, 1988, ISBN 3-519-02083-1 .
• Heinrich Werner: Introduction to general algebra. Bibliographical Institute, 1978, ISBN 3-411-00120-8 .
• Hartmut Ehrig among others: Mathematical-structural basics of computer science. Springer, 2001, ISBN 3-540-41923-3 .
• H. Ehrig, B. Mahr: Fundamentals of Algebraic Specification 1. Equations and Initial Semantics. Springer, 1985, ISBN 3-540-13718-1 .

Remarks

1. ↑ The definition of the terms given here differs from the one given in Term §Formal Definition, Notes as follows:
   • Notation without brackets ( Polish notation ) is used here, but tuple notation ,
   • a number preceding each tuple indicates whether a variable follows (0) or not (1). The quantities and are therefore freely selectable. ${\displaystyle T(X)}$ ${\displaystyle X}$ ${\displaystyle {\mathcal {F}}}$
   • The set of variables is denoted here with , there with . ${\displaystyle X}$ ${\displaystyle {\mathcal {V}}}$