Benutzer:Lowtec/p/Algebraische Spezifikation

Die algebraische Spezifikation ist ein Gegenstand der theoretischen Informatik. Sie verwendet Begriffe, Methoden und Ergebnisse der allgemeinen Algebra, um abstrakte Datentypen mittels formaler Spezifikationen zu beschreiben. Technisch können so definierte Datentypen ggfls. durch geeignete Termersetzungssysteme direkt ausführbar gemacht werden.

Einleitung

Fragestellung

In der Informatik treten eine Vielzahl von Datentypen wie Zahlen, Zeichenketten, Reihungen, endliche Abbildungen, Bäume usw. auf. Will man diese zum Gegenstand formaler (Korrektheits-)Beweise machen, dann stellt sich die Frage, welche Methoden man einsetzen kann, um sie hinreichend präziese zu beschreiben. Umgekehrt steht man im Rahmen einer formalen Fassung eines Datentypen vor dem Problem, gegebenenfalls mehr Details zu beschreiben, als gewünscht. Insbesondere soll eine formale Beschreibung möglichst neutral gegen einer Implementierung sein, von deren besonderen Details also abstrahiern. Allgemeiner hat eine geeignete Technik damit auch die Frage nach dem Verhältnis von Spezifikation und Implemenierung zufriedenstellend zu beantworten.

Grundgedanke

Zu allererst steht man bei der Herstellung eines Verfahrens, dass einen Datentyp abstrakt von jeglicher Implementierung und Darstellung beschreiben will, vor dem Problem, wie denn die Daten dann überhaupt noch darstellen soll, wenn man über deren Präsentation gar nicht mehr reden darf.

Der bei der algebraischen Spezifikation verfolgte Ansatz verwendet dazu zwei zentrale Mittel. Zunächst verbleiben für die Darstellung im Wesentlichen alleine die Namen der Operationen des Datentyps selbst als mögliche Grundlage. Da Operationen in diesem Zusammenhang grundsätzlich Funktionen sind, bieten sich Terme als hinreichend feinkörniges Ausdrucksmittel an.

Nun stehen Terme alleine allerdings nur für sich selbst, haben also zunächst keine besondere Bedeutung. Das zweite eingesetzte Mittel ist nun, die möglichen Werte eine Datentypen durch Gleichheit zwischen allen möglichen verschiedenen Darstellungen anzugeben. Damit kann ebenfalls formal präzisiert werden, welche Funktionen mit den Operationsnamen eigentlich genau bezeichnet sind.

Die Wirkung der Gleichheit als Mittel der Abstraktion lässt sich formal bereits durch Bildung von Klassen äquivalenter Gegenstände präzisieren. Legt man eine Menge $M$ von Präsentationen und eine Äquivalenzrelation $\sim$ zwischen ihnen zu Grunde, dann kann man alle zu $a\in M$ äquivalente Präsentationen zu einer Klasse zusammenfassen: $[a]::=\{x\in M\ |\ x\sim a\}$. Man kann dann von den Präsentationen, also der Mengen $M$ auf die Menge der so gebildeten Klassen $M/\sim \ ::=\{[a]\ |\ a\in M\}$ übergehen. Den Übergang bewerkstelligt eine für die Äquivalenz charakteristische kanonische Abbildung $nat::=\{a\mapsto [a]\ |a\in M\}$.

Man kann die Klassen in diesem Zusammenhang als Werte bezeichen. Legt man als Repräsentationen Ausdrücke zu Grunde, dann stellen beispielsweise die Ausdrücke '3', '+3', '2+1' alle den selben Wert drei dar. Eine Klasse wären dann alle Ausdrück, die drei ergeben, die kanonische Abbildung das Ausrechnen der Ausdrücke.

Offenbar hat dieses Beispiel noch das Problem, dass die Ausdrücke nicht alleine aus Funktionen bestehen, sondern zudem noch Zahlen direkt enthält. Um sich in der Darstellung nun ganz auf Terme zurückzuziehen, können etwa die beiden Funktionsnamen 'eins' und 'plus' vereinbart werden, die alleine für die Bildung eines Terms verwendet werden dürfen.

Man erhielte dann für als Klasse für den Werte drei die beiden Terme 'plus(eins,plus(eins,eins))' und 'plus(plus(eins,eins),eins)'. Um die Terme nun zu ihren Klassen zusammenzufassen, ist eine geeignet Gleichheit anzugeben, wobei hier die Assoziativität von 'plus' bereits ausreicht, also:

plus(plus(A,B),C) = plus(A,plus(B,C))

Da Klassen nun aus vielen Elementen bestehen, sind sie in der Praxis ggfls. ein nur schwer handbares Darstellungsmittel. Durch Wahl eines Repräsentaten als Vertreter seiner jeweiligen Klasse, kann man sich jedoch wieder auf die Grundmenge selbst, die Terme also zur Darstellung zurückziehen. Dies führt auf den Begriff der kanonischen Normalform eines Terms.

Wendet man auf einen beliebigen Term die Assoziativitätsregel oben grundsätzlich von links nach rechts so lange an, wie dies möglich ist, dann erhält man in diesem Beispiel den Term in seiner kanonischen Form, hier etwa 'plus(eins,plus(eins,eins))' als Repräsentanten von drei. In dieser Form geht die Gleichheit in die Identität über, man kann also die Gleichheit zweier Terme testen, indem man sie kanonifiziert und die Normalformen unmittelbar vergleicht.

Die Gleichungen und damit auch die algebraische Spezifikations selbst können also u.U. als Termersetzungsregeln praktisch mit einem Termersetzungssystem zur Ausführung gebracht werden.

Leistung und Abgrenzung

Algebraische Spezifikationen sind ausdrucksstark genug, gängige Datentypen formal zufriedenstellend zu beschreiben. Welche Algebren, also Datentypen mit Hilfe von Gleichungen beschrieben werden können, hat Birkhoff näher untersucht. Aus Sicht der Informatik sind gleichungsdefinierte Algebren ausdrucksstark genug, so ist etwa der Lambda-Kalkül algebraisch definierbar. Die Herstellung von Normalformen stösst entsprechend auf Entscheidbarkeitsprobleme.

Um algebraische Spezifikationen trotzdem sowohl möglichst natürlich und zugleich direkt ausführbar zu machen, wurden Termersetzungssysteme in der Informatik intensiv untersucht und zahlreiche Programmiersprachen auf der Grundlage algebraischer Spezifikation entwickelt, darunter etwa die OBJ-Familie Goguens.

Zur Abgrenzung ist insbesondere hervorzuheben, dass Datentypen hier als Menge von Werten verstanden werden, also keine zustandsbehaftete Größe darstellen, etwa im Gegensatz zu Objekten im Sinne objektorientierter Programmierung. Historisch und z.T. noch landläufig wird der Terminus Datentyp auch für zustandsveränderliche Strukturen verwendet, Stapel, etwa. Da solche Beispiele auch in der Literatur zur algebraischen Spezifikation durchaus üblich ist, ist hier sorgfältig zu unterscheiden: Die algebraische Spezifikation ist sehr wohl in der Lage, den Inhalt eines Stapel als Wert zu beschreiben, auch durch eine Kette von Operation hindurch. Nicht beschrieben werden kann jedoch ein Stapel als zustandsveränderlich Größe. Dies müsste mit einer den Stapel als zustandsbehafteten Gegenstand präsentierenden (Programm-)Variablen geschehen, die den Inhalt des Stapels enthält und im Rahmen der Ausführung jeder Operation als Seiteneffekt aktualisiert wird.

Je nach dem, was im Vordergrund der formalen Modellierung steht, sind die Mittel entsprechend zu wählen. Möchte man Werte und deren Operationen beschreiben, kann algebraische Spezifikation geeignet sein, stehen Zustände im Vordergrund, dann sind ggfls. automatentheoretischen Möglichkeiten für eine Formalisierung besser geeignet.

Formale Beschreibung

Signaturen, Algebren

Signaturen beschreiben den Typ der spezifizierten Algebra in dem Sinne, in dem eine Signatur in der Programmierung zur Beschreibung der Schnittstelle eines Moduls verwendet wird.

In der universellen Algebra versteht man unter einer Signatur $\sigma :F\rightarrow \mathbb {N}$ eine endliche Abbildung von Funktionsnamen $F$ auf natürliche Zahlen. Die Signatur gibt dann einfach die Arität der Operation an. Ein Signatur in diesem Sinne ist für das einleitende Beispiel $\{eins\mapsto 0,plus\mapsto 2\}$, womit zum Ausdruck gebracht wird, dass man eine Algebra beschreibt, die zwei Operationen 'eins' und 'plus' hat, wobei letztere zwei Argumente und die erstere kein Argument benötigt, also eine Konstante ist.

Unter einer zu einer Signatur $\sigma$ passenden Algebra ${\mathcal {A}}$ wird dann ein Paar $(A,{\mathcal {F}})$ verstanden, wobei $A$ die Grundmenge und ${\mathcal {F}}$ eine Familie von Funktionen $(f_{A}|(f,n)\in F)$, die jedem Funktionsnamen $f$ der Signatur eine $\sigma (f)$-stellige Funktion $f_{A}$ über der Grundmenge der Algebra zuordnet.

Signaturen in algebraischen Spezifikationen

In algebraische Spezifikationen werden kompliziertere Signaturen verwendet, da man oft Operationen mit mehr als einem Datentyp beschreiben möchte. Entsprechend werden die Operationen durch die Signaturen getypt. Je nach Spezifikationmethode kann die Signatur noch beliebig komplizierter und die zugehörige Spezifikationssprache entsprechend ausdrucksstärker sein. Um die Darstellung hier nicht zu überfrachten, werden Signaturen wie die unten nur als Beispiele gebracht und nicht weiter präzisiert.

typ
 Nat
ops
 eins : Nat
 plus : Nat x Nat -> Nat

Terme, Termalgebra

Bei gegebener Signatur lassen sich bereits Terme angeben. Sind (induktiv) $t_{1},\ldots ,t_{n}$ Terme und ist $f$ ein n-stelliges Funktionssymbol der Signatur, so ist $f(t_{1},\ldots ,t_{n})$ ein Term. Sind dies die einzigen zugelassen Terme, dann spricht man auch von Grundtermen. 'plus(plus(eins,eins),eins)' war weiter oben ein Beispiel für einen Grundterm. Man bezeichnet die Menge der Grundterme zu einer Signatur $\sigma$ mit $T_{\sigma }$.

Legt man nun $T_{\sigma }$ als Grundmenge einer $\sigma$-Algebra $A$ zugrunde und definiert für jedes $(f\mapsto n)\in \sigma$ eine Funktion $f_{T_{\sigma }}(t_{1},\ldots ,t_{n})::=f(t_{1},\ldots ,t_{n})$, dann erhält man zusammen die initiale Termalgebra dieser Signatur.

Da auf den ersten Blick scheint der praktische Nutzen einer Termalgebra durchaus zweifelhaft erscheinen mag, direkt eine Anwendung. Einleitend war erwähnt worden, dass man den Wert eines Terms durch Ausrechnen ermitteln kann. Mit der Termalgebra an der Hand, kann dies nun präzisiert werden. Für jede Signatur $\sigma$ und jede $\sigma$-Algebra $A$ gibt es einen eindeutig bestimmten Auswertungs-Homomorphismus $eval:T_{\sigma }\rightarrow A$.

Sammlung

Begriffe

• Term-Algebra
• Gleichungsdefinierte Spezifikation
• Quotient-Term-Algebra, Faktoralgebra
• Lose (klassische), initiale, freie Semantik
• Normalformen
• Syntaktischer und Semantischer Folgerungsbegriff
• Spezifikation, Modell

Artikel

• Universelle Algebra
• Algebraische Struktur
• Abstrakter Datentyp
• Formale Semantik
• Termersetzungssystem
• Äquivalenzrelation
• Kongruenzrelation

Implementierungen

• Verweis auf entsprechende Systeme

Beispiel für Ausdruckskraft

S * x * y * z = (x * z) * (y * z)
K * x * y     = x