Termalgebra

Kernidee und Definition

Eine freie Termalgebra ist in Mathematik und Informatik eine algebraische Struktur, die frei über eine Signatur erzeugt wird. Ihre Grundmenge besteht aus Termen. Die Operationen nehmen Terme als Argumente und liefern wieder Terme als Ergebnis.

Termalgebren sind wichtig, weil sie den Vorgang des Ausrechnens oder Interpretierens eines Terms mathematisch beschreiben, Terme selbst als algebraische Struktur behandeln und als einfacher Prototyp freier Erzeugung dienen. Sie spielen eine zentrale Rolle in der universellen Algebra, der mathematischen Logik und der formalen Semantik.

Signatur, Terme und Grundtermalgebra

Für eine algebraische Struktur wird zuerst ihre Signatur festgelegt: S = (F, σ). Dabei ist F die Menge der Operationssymbole und σ: F → N₀ ordnet jedem Operationssymbol seine Stelligkeit zu, also die Anzahl seiner Argumente. In der universellen Algebra heißt eine Signatur auch Typ.

Mit einer Variablenmenge X erhält man die Terme T(X) als kleinste Menge mit folgenden Regeln: Ist x ∈ X, dann ist (0,x) ∈ T(X). Sind t₁, …, tₙ ∈ T(X) und gilt σ(f)=n, dann ist (1,f,t₁,…,tₙ) ∈ T(X).

Die fundamentalen Operationen der freien Termalgebra (T(X),F) sind durch f_T(X)(t₁,…,tₙ) := (1,f,t₁,…,tₙ) definiert. Man bezeichnet die freie Termalgebra mit T(X). Ist X leer, sind also keine Variablen zugelassen, spricht man von einer Grundtermalgebra und schreibt T. 0-stellige Operatoren werden üblicherweise als Konstanten aufgefasst.

Auswertung als Homomorphismus

Die wesentliche Eigenschaft der Termalgebra ist, dass die Bedeutung von Termen als strukturverträgliche Abbildung beschrieben werden kann, nämlich als Homomorphismus. Ein Homomorphismus ist eine Abbildung zwischen Algebren gleichen Typs, die die Operationen respektiert.

Der zentrale Satz lautet: Sei T(X) eine Termalgebra vom Typ (F,σ) über X. Dann gibt es für jede Algebra A vom selben Typ und jede Abbildung φ: X → A genau einen Homomorphismus φ̄: T(X) → A, der φ fortsetzt, also φ̄_|x = φ.

Die Abbildung φ heißt Belegung der Variablen mit Werten und wird gelegentlich mit „ass“ bezeichnet. Die Fortsetzung φ̄ heißt Auswertungshomomorphismus oder „eval“. Sie wird rekursiv definiert: φ̄((0,x)) := φ(x) und φ̄((1,f,t₁,…,tₙ)) := f_A(φ̄(t₁),…,φ̄(tₙ)). Dadurch wird der Vorgang des Ausrechnens eines Terms mathematisch erfasst.

Kategoriale Sicht

Die Termalgebra kann auch kategorial definiert werden. Betrachtet wird dabei die Kategorie, deren Objekte Algebren gleichen Typs sind und deren Morphismen Homomorphismen sind. Statt die Terme konkret zu „implementieren“, wird dann die universelle Eigenschaft zur Grundlage der Definition gemacht.

Bei Grundtermalgebren ist die Charakterisierung besonders einfach: Für jede Algebra A desselben Typs gibt es genau einen Homomorphismus von der Grundtermalgebra T nach A. Daher ist die Algebra der Grundterme ein Anfangsobjekt dieser Kategorie und wird auch initiale Termalgebra genannt.

Für freie Termalgebren wird die universelle Eigenschaft mithilfe des Vergissfunktors U: Alg → Set formuliert. Dieser überträgt Algebren auf ihre Grundmengen und Homomorphismen auf die zugrunde liegenden Funktionen. Eine kategoriale Definition macht die besondere Stellung der freien Termalgebra deutlich, verlangt aber Existenz- und Eindeutigkeitsbeweise. Dafür muss man zumindest im Beweis wieder eine konkrete Präsentation angeben.

Variablen und freie Konstruktion

Terme werden oft zunächst als syntaktische Konstruktionen verstanden: Variablen sind dann Bezeichner wie „a“, „b“, „c“, um die herum Funktionssymbole geschrieben werden. In diesem Sinn beschreibt der zentrale Satz die Auswertung oder Interpretation solcher syntaktischer Terme.

Für die freie Konstruktion ist die Variablenmenge aber mehr als eine Menge von Textvariablen. Sie steht als Platzhalter für die Grundmenge einer beliebigen anderen Struktur, um die herum die Termalgebra frei konstruiert wird. Die freie Termalgebra ist dabei besonders einfach, weil sie außer ihren Funktionen keine weiteren Gesetze mitbringt.

In der Mathematik gibt es freie Konstruktionen zu vielen Strukturen, etwa freies Monoid oder freie Gruppe. In der Informatik entsprechen ihnen parametrische Datentypen. Der Artikel nennt Haskell, wo freie Termalgebren direkt definiert werden können, und C++-Templates als Möglichkeit freier Konstruktion. Die Typparameter übernehmen dann die Rolle der Variablenmenge.

Einordnung und Anwendungen

Freie Termalgebren haben in der Kategorie der Algebren gleichen Typs eine besondere Stellung, weil jede Algebra desselben Typs von ihnen aus eindeutig erreichbar ist. Da sie keine zusätzliche Struktur besitzen, eignen sie sich als Ausgangspunkt, um andere Algebren zu gewinnen.

In der universellen Algebra untersucht man unter anderem, wie Algebren durch Gleichungen beschrieben werden können, wie es bei Gruppen oder Ringen geschieht. Das führt zu Gleichheitskalkülen und zur Quotiententermalgebra: einer Termalgebra unter der Kongruenz, die durch die Gleichungen erzeugt wird.

In der Informatik erscheint diese Methode als algebraische Spezifikation abstrakter Datentypen. Sind die definierenden Gleichungen direkt durch ein Termersetzungssystem ausführbar, liefert die Spezifikation zugleich eine Implementierung. In der mathematischen Logik wird die Grundtermalgebra in der Herbrand-Theorie als Herbrand-Struktur verwendet, um prädikatenlogische Formeln zu interpretieren.

Eine Besonderheit von Termalgebren ist, dass Gleichheit der Terme mit ihrer Identität zusammenfällt: Jeder Term ist nur mit sich selbst gleich und von allen anderen verschieden. Diese eindeutige Darstellung wird konstruktiv genutzt, etwa bei Erzeugungssystemen, induktiven Datentypen und struktureller Induktion.