Termalgebra

aus Wikipedia, der freien Enzyklopädie
(Weitergeleitet von Herbrand-Struktur)
Wechseln zu: Navigation, Suche

Eine Termalgebra ist eine algebraische Struktur, die aus einer Signatur frei generiert wird. Die Signatur gibt die Operationen der Algebra an mit deren Stelligkeiten – inklusive nullstellige Operationen, auch Konstanten genannt.

Zum Beispiel sind freie Halbgruppen isomorph zu Termalgebren, die aus einer Signatur generiert werden, die nur aus einer Binäroperation besteht (der Multiplikation-Operation der Halbgruppe) und einer Menge an Konstanten.

Termalgebren sind wichtig bei der Bestimmung der Bedeutung (Semantik) von abstrakten Datentypen (ADTs). Hierbei bietet die ADT-Deklaration einer Signatur für ein algebraische Struktur mit mehreren Typen. Die Termalgebra ist ein konkretes Modell der abstrakten Deklaration.

In der Logik, insbesondere in der logischen Programmierung, werden Termalgebren auch als Herbrand-Strukturen bezeichnet. Diese werden dort definiert als eine zu einer prädikatenlogischen Formelmenge F passende Struktur A=\left(U,I\right), so dass:

  • Das Universum ist das aus F generierte Herbrand-Universum, also  U=D\left(F\right).
  • Die Interpretationen I sind Herbrand-Interpretationen.

Bei einer Interpretation werden den Funktions- und Konstantensymbolen tatsächliche Funktionen und Konstanten zugeordnet. Bei der Herbrand-Interpretation weist man jedem Funktionsterm eine Interpretation durch sich selbst zu. Dies ist möglich, da das Herbrand-Universum genau aus der Menge aller möglichen Terme mit Funktions- und Konstantensymbolen besteht. Damit ist eine Herbrand-Struktur eine Terminterpretation.

Die Termalgebra zu einer Signatur ist das Initialobjekt in der Kategorie aller Strukturen dieser Signatur.

Beispiel[Bearbeiten]

Sei das Herbrand-Universum D\left(F\right) = \{ a, f(a), f(f(a)), ... \}. Dann lautet die Zuordnung zwischen Funktionssymbolen und Elementen aus dem Universum:

f^A(a) = f(a)
f^A(f(a)) = f(f(a))
f^A(f(f(a))) = f(f(f(a)))
...

Herbrand-Strukturen werden im Satz von Herbrand verwendet und sind nach Jacques Herbrand benannt.

Entscheidbarkeitsfragen[Bearbeiten]

Termalgebren sind entscheidbar unter der Eliminierung von Quantifizierern. Die Komplexität des Entscheidungsproblems gehört zur Klasse NONELEMENTARY.

Literatur[Bearbeiten]

  • Anatolii Ivanovic Mal'cev: "The Metamathematics of Algebraic Systems". North-Holland, 1971. (Studies in Logic and The Foundations of Mathematics, Volume 66)
  • H.-D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik, Spektrum Akademischer Verlag 1996, ISBN 3-8274-0130-5