Termalgebra

In der Mathematik und in der Informatik versteht man unter einer freien Termalgebra eine frei über eine Signatur erzeugte algebraische Struktur. Die Grundmenge der Termalgebra sind die Terme. Die Operationen der Termalgebra haben Terme als Argumente und liefern wieder Terme als Ergebnis. Termalgebren liefern u. a.

• eine Möglichkeit, den Vorgang des „Ausrechnens“, der Interpretation eines Term genauer zu betrachten und mathematisch einzuordnen,
• durch Darstellung der Terme als algebraische Struktur deren Verhältnis zu allen anderen algebraischen Strukturen aufzuhellen,
• einen Prototyp für das Konzept der freien Erzeugung von algebraischen Strukturen.

Termalgebren spielen u. a. in der universellen Algebra, der mathematischen Logik und der formalen Semantik eine zentrale Rolle.

Signatur, Term, Termalgebra, Grundtermalgebra

Für eine algebraische Struktur ist zunächst ihre Signatur ${\boldsymbol {S}}=({\mathcal {F}},\sigma )$ festgelegt, also die Menge ${\mathcal {F}}$ der Operationssymbole zusammen mit ihrer Stelligkeit $\sigma \colon {\mathcal {F}}\to \mathbb {N} _{0}$. Hat man ferner die Menge der Variablen $X$, dann erhält man die Terme $T(X)$ als kleinste Menge, für die gilt:

${\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}}$

Die fundamentalen Operationen $f_{T(x)}\in F$ der freien Termalgebra $(T(X),F)$ sind:

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

Man bezeichnet die freie Termalgebra mit $T(X)$. Für den Fall, dass die Menge $X$ leer ist, Variablen also ausgeschlossen sind, spricht man von einer Grundtermalgebra und bezeichnet sie mit $T$. Sofern nicht ausdrücklich hervorgehoben, sind Variablen immer zugelassen, wenn kürzer von einer Termalgebra anstelle einer freien Termalgebra die Rede ist. Es ist üblich, 0-stellige Operatoren als Konstanten aufzufassen. In der universellen Algebra nennt man eine Signatur auch Typ.

Wesentliche Eigenschaft der Termalgebra

Man hat nun mit der Termalgebra die über den Typ erzeugten Terme als Grundmenge einer Algebra desselben Typs vorliegen. Damit ist es möglich, die Interpretation, also die Bedeutung der Terme mit Mitteln der universellen Algebra selbst zu fassen und die Termalgebra zusammen mit ihren „Verwandten“, den Algebren gleichen Typs, gemeinsam zu betrachten. Die wesentliche Eigenschaft der Termalgebra ist, dass man eine Bedeutung der Terme als strukturverträgliche Abbildung, als Homomorphismus fassen kann. Hierbei wird zugleich der Vorgang des Ausrechnens durch folgenden Satz fassbar:

Satz: Sei $T(X)$ eine Termalgebra vom Typ $({\mathcal {F}},\sigma )$ über $X$. Dann gibt es für jede Algebra $A$ vom selben Typ und jede Abbildung $\phi \colon X\to A$ genau einen Homomorphismus ${\bar {\phi }}\colon T(X)\to A$, der $\phi$ fortsetzt, d. h. ${\bar {\phi }}_{|x}=\phi$.

Beweis: ${\bar {\phi }}\colon T(X)\to A$ wird definiert durch:

${\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}}$

Auf diese Weise ist ${\bar {\phi }}$ auf ganz $T(X)$ definiert und wegen der Eindeutigkeit der Erzeugung sogar wohldefiniert. Wegen $f_{T(X)}(t_{1},\dotsc ,t_{n}):=(1,f,t_{1},\dotsc ,t_{n})$ ist ${\bar {\phi }}$ ein Homomorphismus. $\square$

$\phi$ wird auch Belegung (der Variablen mit Werten) genannt und gelegentlich mit „ass“ (für engl. assignment) bezeichnet. Die Fortsetzung ${\bar {\phi }}$ nennt man auch Auswertungshomomorphismus und bezeichnet sie mit „eval“ (für engl. evaluation). Man findet den Satz oft begleitet von einem Diagramm wie dem rechts gezeigten. Hierin ist $i\colon X\to T(X)$ die Einbettung ($i(x)=(0,x)$) von $X$ in $T(X)$. Das Diagramm „kommutiert“, d. h., es gilt $\phi ={\bar {\phi }}\circ i$.

Kategoriale Definition

Aus obigem Satz folgt mit $\phi (x)=x$ ohne Rückgriff auf die Definition, dass eine Termalgebra isomorph zu jeder anderen Algebra gleichen Typs ist, die diesen Satz erfüllt. Man kann die wesentliche Eigenschaft der Termalgebra damit definitorisch wenden. Dadurch wird, statt einer Angabe einer konkreten „Implementierung“ der Terme und der Operationen, die Aussage des obigen Satzes zur Grundlage der Definition genommen. Die Methode hierfür liefert die Kategorientheorie. Die betrachtete Kategorie besteht aus den Algebren gleichen Typs als Objekte und deren Homomorphismen als Morphismen.

Initialität der Grundtermalgebren

Im Fall der Grundtermalgebren ist die Charakterisierung besonders einfach. Obiger Satz verkürzt sich für eine leere Variablenmenge auf die Aussage, dass es zu jeder Algebra $A$ in der Kategorie der Algebren gleichen Typs genau einen Homomorphismus von der Grundtermalgebra $T$ zu der Algebra $A$ gibt. Die Algebra der Grundterme ist also das Anfangsobjekt dieser Kategorie. In diesem Sinne nennt man die Grundtermalgebra auch die initiale Termalgebra.

Universelle Eigenschaft der freien Termalgebren

[[Hilfe:Cache|Fehler beim Thumbnail-Erstellen]]: Datei fehlt

Die freie Termalgebra lässt sich durch die im Bild rechts gezeigte universelle Eigenschaft definieren.

Dieses Diagramm weicht vom weiter oben gezeigten nur dadurch ab, dass nun die verschiedenen Kategorien, die der Algebren desselben Typs mit ihren Homomorphismen (links) sowie die Kategorie der Mengen und ihrer Abbildungen (rechts) in zwei Teildiagrammen getrennt sind. In jedem der Teildiagramme ist nun die Kompositionsoperation der jeweiligen Kategorie anwendbar. Beide Seiten werden durch den Vergissfunktor $U\colon Alg\to Set$ vermittelt. Er überträgt von den Algebren die jeweiligen Grundmengen als Objekte ($u(x)=x$) sowie deren Homomorphismen als Funktionen ($u(f)=f$).

Beweisverpflichtungen

Während eine kategoriale Fassung die besondere Lage der Algebra der Grundterme und der freien Termalgebra deutlich hervorhebt, kann sie das einleitend gegebene Versprechen, die wesentlichen Eigenschaften definitorisch darstellungsneutral zu wenden, nur zum Teil einlösen. Anderes als bei der einleitenden Definition erfordert die kategoriale Fassung als Definition einen Existenz- und einen Eindeutigkeitsbeweis, in dem zu belegen ist, dass das betreffende Objekt in der Kategorie existiert und der Morphismus eindeutig ist. Der Nachweis erfolgt dann wie oben. An dieser Stelle kommt man um die Angabe einer konkreten Präsentation also nicht herum. Allerdings kann die für den Beweis gewählte Präsentation gegebenenfalls auf diesen Nachweis beschränkt bleiben, da in ihm die wesentliche Eigenschaft der Termalgebra vollständig erfasst wird.

Rolle der Variablen, freie Konstruktion überhaupt

Ebenso wie einleitend an die intuitive Vorstellung von Termen als niedergeschriebener Text appelliert wird, werden Terme in vielen Zusammenhängen zunächst als bloße syntaktische Konstruktion eingeführt. So verstanden, stellen die Variablen einfach eine (aufzählbare) Menge von Bezeichnern („a“, „b“, „c“, …) dar, um die herum dann die Funktionssymbole geschrieben werden. In Zusammenhängen, in denen mit Termen als Gegenständen gearbeitet wird, ist diese Auffassung auch vollkommen richtig. Obiger Satz beschreibt dann einfach die Möglichkeit und Weise der Auswertung oder Interpretation. Hält man aber an dieser Vorstellung der Termalgebra als eine bloß syntaktische Fassung des niedergeschriebenen Terms fest, dann wird der Begriff der freien Termalgebra als Prototyp der freien Konstruktion verpasst.

In der freien Konstruktion steht die Variablenmenge nicht für textuelle Variablen, sondern ist ein Platzhalter für die Grundmenge einer beliebigen anderen Struktur, um die herum die Termalgebra dann frei konstruiert wird.

In der Mathematik findet man eine freie Konstruktion praktisch zu jeder Struktur (freies Monoid, freie Gruppe usw.), wobei der freien Termalgebra nur die Sonderstellung zukommt, besonders einfach dahingehend zu sein, dass sie außer ihren Funktionen keine weiteren Gesetze mitbringt. Die freie Konstruktion findet in der Informatik ihre Entsprechung bei parametrischen Datentypen. Moderne Programmiersprachen stellen dieses Konzept oft in der einen oder anderen Weise zur Verfügung. So können freie Termalgebren etwa in Haskell direkt definiert werden, während in C++ die Templates eine Möglichkeit der freien Konstruktion offerieren. Die Typparameter treten dann in die Rolle, die die Variablenmenge hier hat.

So gewendet, kommt obigem Satz die Aufgabe zu, sicherzustellen, dass durch die Konstruktion die mit $X$ gegebene Struktur nicht verletzt wird, diese also frei von den Gesetzmäßigkeiten der um sie herum konstruierten Struktur bleibt.

Einordnung und Weiterführung

In der kategorialen Betrachtung wird deutlich, dass freie Termalgebren eine besondere Lage in der Kategorie der Algebren gleichen Typs insofern haben, als jede Algebra desselben Typs von ihnen ausgehend eindeutig erreichbar ist. Da sie bar jeder weiteren Struktur sind, stellen sie den idealen Ausgangspunkt dar, um andere Algebren aus ihnen zu gewinnen.

In der universellen Algebra als Teildisziplin der Mathematik wird u. a. untersucht, inwieweit dies definitorisch durch Angabe von Gleichungen möglich ist, wie dies bei vielen algebraischen Strukturen (Gruppen, Ringen) der Fall ist. Dies führt auf einen Gleichheitskalkül und Methoden, aus diesen Gleichungen zu der so beschriebenen Algebra zu gelangen, der Quotiententermalgebra, die eine Termalgebra unter der durch die Gleichungen erzeugten Kongruenz ist.

Diese Methode wurde in der Informatik unter dem Titel algebraische Spezifikation aufgegriffen und erlaubt die Spezifikation eines abstrakten Datentyps. Wenn die definierenden Gleichungen direkt über ein Termersetzungssystem ausführbar sind, liefert diese Spezifikation auch zugleich eine Implementierung.

In der mathematischen Logik wird die Grundtermalgebra im Rahmen der Herbrand-Theorie unter der Bezeichnung Herbrand-Struktur eingeführt, um zu einer Interpretation prädikatenlogischer Formeln zu gelangen.

Eine Besonderung der Termalgebren ist, dass die Gleichheit ihrer Terme mit deren Identität zusammenfällt. Jeder Term ist gleich nur mit sich selbst und verschieden von allen anderen. Diese Eindeutigkeit der Darstellung der Terme wird oft konstruktiv genutzt, siehe hierzu Erzeugungssystem, induktiver Datentyp und strukturelle Induktion.

Literatur

• Thomas Ihringer: Allgemeine Algebra. Teubner, 1988, ISBN 3-519-02083-1.
• Heinrich Werner: Einführung in die allgemeine Algebra. Bibliographisches Institut, 1978, ISBN 3-411-00120-8.
• Hartmut Ehrig u. a.: Mathematisch-strukturelle Grundlagen der Informatik. 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.