Algebraische Spezifikation
Die algebraische Spezifikation ist eine Spezifikationsmethode. Bei der algebraischen Spezifikation versucht man, die Semantik von Operationen festzulegen:
• Zunächst ordnet eine Signatur mit der Funktion c den Operationsbezeichnern aus der Menge σ jeweils eine Charakteristik zu.
• Die Semantik der Operationen wird danach durch Gleichungen zwischen Termen erfasst.
Die Menge der möglichen Terme definiert man anhand der Operationsbezeichner, einer Menge X von Variablen und der Signatur. Dabei bezeichnet man die Operationsbezeichner, denen eine Charakteristik der Form s zugeordnet ist, als Konstanten. Die Menge der Konstanten K bildet zusammen mit der Menge X der Variablen die Menge der atomaren Terme. Jeder Variable ist ein Sortenbezeichner zugeordnet.
Für die Menge der Terme T(s, σ, c, X) gilt:
• k ∈ T(s, σ, c, X), falls k ∈ K und c(k) = s,
• x ∈ T(s, σ, c, X), falls x ∈ X die Sorte s zugeordnet ist,
• ∀ N ∈ σ mit c(N) = ((s1 ✕ s2 ✕ ... ✕ sk) → s) und ti ∈ T(si, σ, c, X) ist N(t1, t2, ..., tk) ∈ T(s, σ, c, X)
Terme können innerhalb einer Algebra A ausgewertet werden.
eval(k) = k, falls c(k) = s
eval(N(t1, t2, ..., tn)) = NA(eval(t1), eval(t2), ..., eval(tn))
NA ist die unter der Algebra A vorgegebene Operation zum Operationsbezeichner N.
Man spricht von einer Termalgebra, wenn die NA so gewählt werden, dass eval die identische Abbildung zwischen Termen ist.
Beispiel
Signatur
• emptyList: list
• cons: alpha ✕ list → list
• append: list ✕ list → list
• reverse: list → list
• isEmpty: list → bool
Gleichungen
• append(emptyList, X) = X
• append(cons(X, Y), Z) = cons(X, append(Y, Z))
• reverse(emptyList) = emptyList
• reverse(cons(X, Y)) = append(reverse(Y), cons(X, emptyList))
• isEmpty(emptyList) = true
• isEmpty(cons(X, Y)) = false
Eine Algebra A ist eine Spezifikationsalgebra, wenn für alle Grundinstanzen aller Gleichungen L = R gilt: eval(L) = eval(R).
Definiert man eine Gleichheitsrelation == so, dass für zwei Grundterme s und t die Aussage s == t genau dann gilt, wenn eval(s) = eval(t) in jeder Spezifikationsalgebra gilt, dann handelt es sich bei der Relation == um eine Kongruenzrelation.
Kongruenzrelationen sind Äquivalenzrelationen (reflexiv, symmetrisch, transitiv), die zusätzlich mit den Operationen verträglich sind, d.h.:
t1 == s1 & t2 == s2 & ... & tn == sn
impliziert
N(t1, t2, ..., tn) == N(s1, s2, ..., sn)
für alle Operationen N.
Die Algebra, deren Trägermenge die Menge aller Äquivalenzklassen zu == ist und bei der N([t1], [t2], ... , [tn]) = [N(t1, t2, ... , tn)] gilt, nennt man Quotiententermalgebra.
Man bezeichnet die Menge aller Spezifikationsalgebren zu einer gegebenen Spezifikation als deren mathematische Semantik (loose semantics). Die Menge aller zur Quotiententermalgebra isomorphen Algebren wird als initiale Semantik (initial semantics) bezeichnet.
Eine Spezifikationsalgebra kann in ein Logik-Progamm umgeformt werden, das unter günstigen Umständen ausführbar ist.
• Zunächst ordnet eine Signatur mit der Funktion c den Operationsbezeichnern aus der Menge σ jeweils eine Charakteristik zu.
• Die Semantik der Operationen wird danach durch Gleichungen zwischen Termen erfasst.
Die Menge der möglichen Terme definiert man anhand der Operationsbezeichner, einer Menge X von Variablen und der Signatur. Dabei bezeichnet man die Operationsbezeichner, denen eine Charakteristik der Form s zugeordnet ist, als Konstanten. Die Menge der Konstanten K bildet zusammen mit der Menge X der Variablen die Menge der atomaren Terme. Jeder Variable ist ein Sortenbezeichner zugeordnet.
Für die Menge der Terme T(s, σ, c, X) gilt:
• k ∈ T(s, σ, c, X), falls k ∈ K und c(k) = s,
• x ∈ T(s, σ, c, X), falls x ∈ X die Sorte s zugeordnet ist,
• ∀ N ∈ σ mit c(N) = ((s1 ✕ s2 ✕ ... ✕ sk) → s) und ti ∈ T(si, σ, c, X) ist N(t1, t2, ..., tk) ∈ T(s, σ, c, X)
Terme können innerhalb einer Algebra A ausgewertet werden.
eval(k) = k, falls c(k) = s
eval(N(t1, t2, ..., tn)) = NA(eval(t1), eval(t2), ..., eval(tn))
NA ist die unter der Algebra A vorgegebene Operation zum Operationsbezeichner N.
Man spricht von einer Termalgebra, wenn die NA so gewählt werden, dass eval die identische Abbildung zwischen Termen ist.
Beispiel
Signatur
• emptyList: list
• cons: alpha ✕ list → list
• append: list ✕ list → list
• reverse: list → list
• isEmpty: list → bool
Gleichungen
• append(emptyList, X) = X
• append(cons(X, Y), Z) = cons(X, append(Y, Z))
• reverse(emptyList) = emptyList
• reverse(cons(X, Y)) = append(reverse(Y), cons(X, emptyList))
• isEmpty(emptyList) = true
• isEmpty(cons(X, Y)) = false
Eine Algebra A ist eine Spezifikationsalgebra, wenn für alle Grundinstanzen aller Gleichungen L = R gilt: eval(L) = eval(R).
Definiert man eine Gleichheitsrelation == so, dass für zwei Grundterme s und t die Aussage s == t genau dann gilt, wenn eval(s) = eval(t) in jeder Spezifikationsalgebra gilt, dann handelt es sich bei der Relation == um eine Kongruenzrelation.
Kongruenzrelationen sind Äquivalenzrelationen (reflexiv, symmetrisch, transitiv), die zusätzlich mit den Operationen verträglich sind, d.h.:
t1 == s1 & t2 == s2 & ... & tn == sn
impliziert
N(t1, t2, ..., tn) == N(s1, s2, ..., sn)
für alle Operationen N.
Die Algebra, deren Trägermenge die Menge aller Äquivalenzklassen zu == ist und bei der N([t1], [t2], ... , [tn]) = [N(t1, t2, ... , tn)] gilt, nennt man Quotiententermalgebra.
Man bezeichnet die Menge aller Spezifikationsalgebren zu einer gegebenen Spezifikation als deren mathematische Semantik (loose semantics). Die Menge aller zur Quotiententermalgebra isomorphen Algebren wird als initiale Semantik (initial semantics) bezeichnet.
Eine Spezifikationsalgebra kann in ein Logik-Progamm umgeformt werden, das unter günstigen Umständen ausführbar ist.