Universität Hamburg
Fachbereich Informatik

Diplomarbeit
Algebraische PetrinetzeB ODO M ÖLLER
<bmoeller@acm.org>
1. Oktober 1999

Erstbetreuer: Prof. R ÜDIGER VALK
Zweitbetreuer: Prof. C HRISTOPHER H ABELInhaltsverzeichnis
Einführung

5

1 Algebren
7
1.1 Terme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2 Σ-Algebren . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.3 Die Kategorie Alg(Σ) zu einer Signatur . . . . . . . . . . . . . 17
2 Algebraische Spezifikation durch Gleichungen21
2.1 SPEC -Algebren . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.2 Die Kategorie Alg(SPEC ) zu einer Gleichungsspezifikation . 32
3 Erweiterungen von Gleichungsspezifikationen

34

4 Endlichkeitsspezifikationen
38
4.1 SPECF -Algebren . . . . . . . . . . . . . . . . . . . . . . . . . . 38
4.2 Die Kategorie Alg(SPECF ) zu einer Endlichkeitsspezifikation 43
4.3 Erweiterungen von Endlichkeitsspezifikationen . . . . . . . . 45
5 Multimengen und gewichtete Mengen46

6 Gefärbte Netze
6.1 Struktur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.2 Verhalten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.3 Invarianten . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

52
52
54
57

7 Algebraische Netze

62

8 Lineare Invarianten
65
8.1 Algebraische Sicht . . . . . . . . . . . . . . . . . . . . . . . . . . 66
8.2 Bedeutung in den Interpretationen . . . . . . . . . . . . . . . . 72
Literatur

87

Index

91

Einführung
Die vorliegende Diplomarbeit befaßt sich mit algebraischen Methoden zur
Beschreibung und Untersuchung von gefärbten Petrinetzen. Im Gegensatz
zu den üblichen Definitionen für gefärbte Petrinetze werden hier Netze mit
unendlich vielen Stellen und Transitionen gestattet; unendliche Markierungen sind zulässig, auch mit unendlich vielen Marken pro Stelle; und
Schaltvorgänge dürfen unendliche Nebenläufigkeit aufweisen. Das entspricht den ursprünglichen Definitionen der Petrinetze, die keine Endlichkeitsforderungen enthalten – solche werden aber oft hinzugefügt, indem
z. B. alle Markierungen als Elemente eines freien Monoids angesehen werden. Bei gefärbten Petrinetzen ergeben sich Markierungen mit unendlich
vielen Marken auf einer Stelle in natürlicher Weise z. B. dann, wenn füreine Stelle mit einer unendlichen Farbmenge eine Kapazität durch eine
komplementäre Stelle realisiert werden soll [2].
In dieser Arbeit werden algebraische Petrinetze als Beschreibungen vonKlassen gefärbter Petrinetze verwendet. Da beim Umgang mit der Unendlichkeit nicht alle Eigenschaften wie von den endlichen Fällen her bekannt
bestehen bleiben, wird das bekannte Beschreibungsmittel der Gleichungsspezifikationen ergänzt zu Endlichkeitsspezifikationen.
In Abschnitt 1 wird der allgemeine Begriff der Σ-Algebra als Grundlage für die algebraische Spezifikation behandelt; Abschnitt 2 beschäftigt
sich mit Gleichungsspezifikationen. Die Inhalte dieser beiden Abschnitte
sind zum großen Teil an [24], [5], [4] und [35] orientiert. Um algebraische
Spezifikation aus einer weiteren Perspektive zu betrachten, werden in Abschnitt 3 Erweiterungen von Gleichungsspezifikationen betrachtet. Der dort
entwickelte Begriff der vorsichtigen Erweiterung bleibt in der vorliegenden
Arbeit ohne konkrete Anwendung auf Petrinetze, sollte jedoch dabei helfen, die Möglichkeiten und Grenzen der Spezifikation durch Gleichungenkennenzulernen. Abschnitt 4 stellt das neue Konzept der Endlichkeitsspezifikationen vor.
In Abschnitt 5 werden als Voraussetzung für gefärbte und algebraische
Petrinetze gewichtete Mengen und als ein Spezialfall davon Multimengen
behandelt. Dabei wird schwerpunktmäßig einer Problematik nachgegangen, die erst durch das Zulassen von Unendlichkeit eine Rolle spielt unddeshalb in der Petrinetz-Literatur sonst keine Erwähnung findet: Für den
Umgang mit gewichteten Mengen werden einige Verträglichkeitsbegriffe
eingeführt und untersucht.
Abschnitt 6 definiert den Begriff des gefärbten Petrinetzes und geht
auf das Verhalten von gefärbten Petrinetzen ein. Dabei wird der Begriff
der Invarianten in allgemeiner Form erörtert. Abschnitt 7 definiert, ausgehend vom Konzept der Endlichkeitsspezifikation, den Begriff des algebraischen Petrinetzes und zeigt den Zusammenhang mit gefärbten Netzen. Abschitt 8 schließlich illustriert anhand von linearen Invarianten algebraischer Petrinetze die Motivation, bei der algebraischen Spezifikation
von Petrinetzen anstatt von Gleichungsspezifikationen von Endlichkeitsspezifikationen auszugehen.
56

Einführung1 Algebren
Dieser Abschnitt schafft die Grundlage für die algebraische Spezifikation,indem einige der wichtigen Begriffe definiert und eine Reihe von später
verwendeten Resultaten bewiesen werden. Vom Begriff der Signatur ausgehend werden zunächst Terme und Substitutionen (Abschnitt 1.1), dann
Algebren und Homomorphismen (Abschnitt 1.2) behandelt; anschließend
wird gezeigt, wie die Algebren zu einer Signatur als Objekte einer Kategorie zueinander in Beziehung gestellt werden können (Abschnitt 1.3).
In späteren Abschnitten werden weitergehende Beschreibungsmöglichkeiten für Algebren vorgestellt, dadurch ergeben sich Spezialfälle von
Σ-Algebren: Spezifikation mittels formaler Gleichungen führt dann zu
SPEC -Algebren (Abschnitt 2), Spezifikation durch Endlichkeitsterme zu
SPECF -Algebren (Abschnitt 4).
Durchgängig werden folgende Vereinbarungen vorausgesetzt: Die Menge N = {0, 1, 2, . . .} der natürlichen Zahlen enthält die 0. Zu einer Menge S
S
ist die disjunkte Vereinigung S ∗ = n∈N S n mit S 0 = {λ} die Menge derWörter über dem Zeichenvorrat S. Für Mengen A, B ist Abb(A, B) die Menge aller Abbildungen A → B.

1.1

Terme

Terme sind nach gewissen Regeln aufgebaute endliche beschriftete Bäume.
Eine mögliche Konstruktion dafür wird im folgenden explizit dargestellt.
Bei dieser Konstruktion ist jeder Teilbaum ein Paar, dessen erste Komponente die Beschriftung der Wurzel des Teilbaums angibt. Die zweite Komponente enthält, falls der Baum keine weiteren Knoten besitzt (die Wurzel
also selbst ein Blatt ist), die leere Menge ∅; andernfalls enthält sie ein aus
den Unterbäumen der Wurzel gebildetes n-Tupel.
Definition 1.1. Eine Signatur ist ein Paar Σ = (S, Ω), wobei S eine Menge
ist und Ω = (Ωw,s )(w,s)∈S ∗ ×S eine Familie von paarweise disjunkten Mengen.
Die Elemente von S heißen Sorten. Die Elemente von Ωλ,s heißen Konstantensymbole der Sorte s. Die Elemente von Ωw,s mit w 6= λ heißen Operationssymbole der Sorte s, genauer mit Argumentsorten w und Wertsorte s.
Zur Vereinfachung der Schreibweise steht Ω gelegentlich auch für die
S
Menge (w,s)∈S ∗ ×S Ωw,s . Da die Mengen Ωw,s paarweise disjunkt sind, ist
für jedes ω ∈ Ω klar, aus welcher Menge Ωw,s es stammt. Deshalb hat man
wohldefinierte Abbildungen arg : Ω → S ∗ und sort : Ω → S, so daß ω ∈Ωarg(ω),sort(ω) für alle ω ∈ Ω gilt.
Definition 1.2. Ein Variablensystem zu einer Signatur Σ = (S, Ω) ist eine Familie X = (Xs )s∈S von paarweise disjunkten Mengen, für die
[

s∈S

Xs ∩

[

Ωw,s = ∅(w,s)∈S ∗ ×S

gilt. Die Elemente von Xs heißen Variablen der Sorte s.
7

8

1

AlgebrenBemerkung 1.3. Ist X = (Xs )s∈S ein Variablensystem zu Σ und Y =(Ys )s∈S eine Familie von Mengen mit ∀ s ∈ S : Ys ⊆ Xs , so ist auch Y ein
Variablensystem zu Σ.
Definition 1.4. Sei X = (Xs )s∈S ein Variablensystem zu einer Signatur(m)Σ = (S, Ω). Die Familien TΩ,s (X) s∈S werden für m ∈ N induktiv wie folgt
definiert: Für jedes s ∈ S sei(0)TΩ,s (X) := (Xs ∪ Ωλ,s ) × {∅} = (a, ∅) | a ∈ Xs ∪ Ωλ,s .
Für m ∈ N und s ∈ S sei
(m+1)

TΩ,s

(0)

(X) := TΩ,s (X) ∪Ωw,s ×

 Y

(m)



TΩ,si (X)

s1 . . . sn = w ∈ S ∗ \{λ}, n ≥ 1 .

1≤i≤n



Die Familie TΩ,s (X) s∈S wird definiert durch
TΩ,s (X) :=[(m)

TΩ,s (X)m∈N

für s ∈ S. TΩ,s (X) ist die Menge aller Terme der Sortes über dem Varia
blensystem X. Die Elemente von TΩ,s := TΩ,s (∅)s∈S heißen Grundterme
der Sorte s.
(m)

Bemerkung 1.5. Wie man leicht durch Induktion sieht, gilt TΩ,s (X) ⊆
(m+1)

TΩ,s

(X) für jedes s ∈ S und jedes m ∈ N.
(0)

Definition 1.6. Die Tiefe eines Terms T ∈ TΩ,s (X) ist 0, falls T ∈ TΩ,s (X)gilt; andernfalls ist sie das (nach der vorhergehenden Bemerkung eindeutig
(m)
(m−1)
bestimmte) m ∈ N\{0} mit T ∈ TΩ,s (X) \ TΩ,s (X).


Hat der Term ω, (T1 , . . ., Tn ) ∈ TΩ,s (X) die Tiefe m, so haben offensichtlich die Terme T1 , . . ., Tn sämtlich Tiefen < m.
Die Terme ω, (T1 , . . ., Tn ) ∈ TΩ,s (X) (wobei Ti ∈ TΩ,si (X) für jedes i mit
1 ≤ i ≤ n, s1 . . . sn = arg(ω)) schreibt man suggestiver in der Formω(T1 , . . ., Tn );hierbei ist ω wohlgemerkt lediglich ein Operationssymbol und keine Abbildung. Für Terme (a, ∅) ∈ TΩ,s (X) (wobei also a ∈ Xs ∪ Ωλ,s ist) schreibt man
einfach a; gelegentlich schreiben wir auch term(a), um hervorzuheben, daßnicht das Element von Xs ∪ Ωλ,s gemeint ist, sondern der entsprechende(0)Term der Tiefe 0. (Um Xs ∪ Ωλ,s mit TΩ,s identifizieren zu können, wären noch zusätzliche Voraussetzungen zum Verhindern gewisser Anomalien nötig.)Wir benutzen folgende Kurzschreibweisen:TΩ (X) :=[TΩ,s (X),[TΩ,s .

s∈S

TΩ :=

s∈S

1 Algebren

9S

Die Mengenvereinigung s∈S TΩ,s (X) (und damit als Sonderfall auchs∈S TΩ,s ) ist disjunkt; dies folgt aus den Disjunktheitsvoraussetzungenin den Definitionen 1.1 und 1.2. Man kann also jedem Term bei Kenntnis
des zugrundeliegenden Variablensystems »ansehen«, von welcher Sorte er
ist; das heißt, wir haben eine wohldefinierte Abbildung sortX : TΩ (X) → S
mit T ∈ TΩ,sortX (T ) (X) für jedes T ∈ TΩ (X).
S

Definition 1.7. Die Menge U(T ) der Unterterme eines belieben Terms T ∈TΩ,s (X) wird wie folgt rekursiv definiert:• Hat T die Tiefe 0, so ist U(T ) = {T }.
• Hat T eine Tiefe > 0, also eine Darstellung ω(T1 , . . ., Tn ) (ω ∈ Ωw,s ,w = s1 . . . sn ∈ S ∗ \{λ}, Ti ∈ TΩ,si für i ∈ {1, . . ., n), so ist U(T ) ={T } ∪ U(T1 ) ∪ . . . ∪ U(Tn ).
Ein Unterterm T 0 von T heißt echter Unterterm, wenn T 0 6= T ist.
Bemerkung 1.8. Sind X = (Xs )s∈S und Y = (Ys )s∈S Variablensysteme
mit ∀ s ∈ S : Xs ⊆ Ys , so gilt TΩ (X) ⊆ TΩ (Y ), und sortY stimmt auf TΩ (X)
mit sortX überein.
Definition 1.9. Sei T ∈ TΩ (X) ein Term übereinem Variablensystem X =(Xs )s∈S . Dann bezeichnet var(T ) = vars (T ) s∈S das minimale Variablensystem des Terms T , d. h. dasjenige Variablensystem mit ∀ s ∈ S : vars (T ) ⊆Xs und T ∈ TΩ var(T ) , das nur diejenigen Variablen enthält, die tatsächlich in T vorkommen.
var(T ) ist offensichtlich in jedem Fall endlich, d. h. es gibt nur endlich
viele s ∈ S mit vars (T ) 6= ∅ und jede Menge vars (T ) ist endlich.
Definition 1.10. Eine Substitution über einem Variablensystem X =(Xs )s∈S ist eine Familie σ = (σs )s∈S von Abbildungen σs : Xs → TΩ,s (Y ),wobei Y = (Ys )s∈S ein weiteres Variablensystem ist.
In einem solchen Fall benutzt man auch die abkürzende Schreibweise
σ : X → TΩ (Y ). Für σs (x) kann man abkürzend σ(x) schreiben, denn die
Sorte s ist durch x eindeutig festgelegt.
Definition 1.11. Zu einer Substitution σ : X → TΩ (Y ) definiert man rekursiv eine Familie σ = (σ s )s∈S von Abbildungen σ s : TΩ,s (X) → TΩ,s (Y )durch
σ s term(x) := σs (x)für x ∈ Xs ,
σ s term(ω) := term(ω)
für ω ∈ Ωλ,s sowie

σ s ω(T1 , . . ., Tn ) := ω σ s1 (T1 ), . . ., σ sn (Tn )für ω ∈ Ωw,s mit w = s1 . . . sn ∈ S n (n ∈ N\{0}) und Ti ∈ TΩ,si (X). Die soerhaltene Familie σ bezeichnen wir als Substitutionsauswertung.

10

1

Algebren

Wegen der Eindeutigkeit der Sorten kann man die Familie von Abbildungen σ = (σ s )s∈S auch zu einer Abbildung σ : TΩ (X) → TΩ (Y ) zusammenfassen.
Definition 1.12. X = (Xs )s∈S und Y = (Ys )s∈S seien Variablensysteme mit∀ s ∈ S : Xs ⊆ Ys ; Z = (Zs )s∈S sei ein weiteres Variablensystem und σ : Y →TΩ (Z) eine Substitution. Dann ist die Einschränkung (Restriktion) von
σ auf X definiert als σ|X := (σs |Xs )s∈S .
Bemerkung 1.13. In der Situation von Definition 1.12 gilt offensichtlichσ|X (T ) = σ(T ) für alle T ∈ TΩ (X).

1 Algebren

1.2

11

Σ-Algebren

Definition 1.14. Sei Σ = (S, Ω) eine Signatur. Eine Σ-Algebra (kurz
Algebra, wenn der Zusammenhang eindeutig ist) ist ein Tupel A =(As )s∈S , (fω )ω∈Ω mit folgenden Eigenschaften:(i) Für jedes s ∈ S ist As eine Menge.
(ii) Für jedes ω ∈ Ω mit arg(ω) = λ ist fω ∈ Asort(ω) .
(iii) Für jedes ω ∈ Ω, für das arg(ω) = s1 . . . sn ∈ S n mit n ∈ N\{0} ist, istQfω eine Abbildung 1≤i≤n Asi → Asort(ω) .
Für s ∈ S heißt As Trägermenge (carrier set) von s. Die Elemente fω mitω ∈ Ω und arg(ω) = λ heißen Konstanten. Die Abbildungen fω mit ω ∈ Ω
und arg(ω) 6= λ heißen Operationen.
Erwähnenswerte Sonderfälle für Σ-Algebren zu einer beliebig gegebenen Signatur enthält die folgende Definition:
Definition 1.15. Sei Σ = (S, Ω) eine Signatur.
(i) Die triviale Σ-Algebra FinΣ (kurz »triviale Algebra«) wird definiertalsFinΣ := (Fins )s∈S , (fω )ω∈Ω
mit einelementigen Trägermengen Fins := {•} für jedes s. Dabei gilt
zwingend fω = • für jedes ω ∈ Ωλ,s (s ∈ S), und die fω ∈ Ωw,s mit
w ∈ S ∗ \{λ}, s ∈ S müssen konstante Abbildungen auf das Element• ∈ Fins sein.
(ii) Sei X = (Xs )s∈S ein Variablensystem. Bei der TermalgebraTΣ (X) :=TΩ,s (X) s∈S , (fω )ω∈Ωüber X werden die Terme als ihre eigenen Werte herangezogen: Das
heißt, für alle s ∈ S wird festgelegt∀ ω ∈ Ωλ,s : fω := term(ω),
und für alle w = s1 . . . sn ∈ S ∗ \{λ}, s ∈ S und ω ∈ Ωw,sfω :YTΩ,si (X) → TΩ,s (X),1≤i≤nfω (T1 , . . ., Tn ) := ω(T1 , . . ., Tn ).
(iii) Als Sonderfall davon ist
TΣ := (TΩ,s )s∈S , (fω )ω∈Ω



die Termalgebra über dem leeren Variablensystem.

121

AlgebrenIn der Literatur wird oft nicht genau getrennt zwischen den Termmengen »als solchen« einerseits und den Termalgebren andererseits. Den hierjeweils verwendeten Bezeichnungen liegt der Gedanke zugrunde, daß bei
den Familien TΩ (X) von Termmengen (siehe Definition 1.4) die Operationen aus Ω als »Bausteine« im Vordergrund stehen, während bei Termalgebren TΣ (X) deren Eigenschaft, ein Modell von Σ zu sein, hervorsteht.
Aus kategorientheoretischen Gründen wird die triviale Σ-Algebra auch
als finale Σ-Algebra und die Termalgebra über dem leeren Variablensystem auch als initiale Σ-Algebra bezeichnet; siehe Bemerkungen 1.34
und 1.35 im nachfolgenden Abschnitt 1.3.
Bemerkung 1.16. Trägermengen müssen nicht notwendig Elemente enthalten: Falls TΩ,s = ∅ gilt, ist auch As = ∅ möglich; ein Beispiel dafür ist
die Termalgebra über dem leeren Variablensystem in Definition 1.15 (iii).
Gilt jedoch TΩ,s 6= ∅, so muß zwangsläufig As 6= ∅ sein.
Definition 1.17. Sei A eine Σ-Algebra und X = (Xs )s∈S ein Variablensystem. Eine Belegung von X in der Σ-Algebra A ist eine Familie α = (αs )s∈S
von Abbildungen αs : Xs → As .
Man schreibt auch kürzer α(x) für αs (x) (mit x ∈ Xs ), da die Sorte s
durch x eindeutig festgelegt ist. Demgemäß verwendet man die abkürzende Schreibweise α : X → A.
Definition 1.18. Für eine Belegung α : X → A wird die Familie α =(αs )s∈S von Abbildungen αs : TΩ,s (X) → As rekursiv definiert durchαs term(x) := αs (x)für x ∈ Xs ,


αs term(ω) := fω
für ω ∈ Ωλ,s sowie

αs ω(T1 , . . ., Tn ) := fω αs1 (T1 ), . . ., αsn (Tn )für ω ∈ Ωw,s mit w = s1 . . . sn ∈ S n (n ∈ N\{0}) und Ti ∈ TΩ,si (X) für
1 ≤ i ≤ n. Eine solche Familie α heißt Auswertung (evaluation).
Hier schreibt man auch abkürzend α(T ) für αs (T ) (mit T ∈ TΩ,s (X)),
denn die Sorte s ist durch T eindeutig festgelegt. Entsprechend verwendet
man die Schreibweise α : TΩ (X) → A.
Definition 1.19. Für den Spezialfall des leeren Variablensystems (∅)s∈S
setzt man eval := (evals )s∈S , evals := αs : TΩ,s → As mit der hierfür einzig
möglichen Belegung α : (∅)s∈S → A.
Analog zum allgemeinen Fall schreibt man eval : TΩ → A.
Ähnlich wie in Definition 1.12 für Substitutionen kann man auch fürBelegungen die Einschränkung auf geeignete andere Variablensysteme definieren:

1 Algebren

13

Definition 1.20. X = (Xs )s∈S und Y = (Ys )s∈S seien Variablensysteme mit∀ s ∈ S : Xs ⊆ Ys , und α : Y → A sei eine Belegung. Dann ist die Einschränkung (Restriktion) von α auf X definiert als α|X := (αs |Xs )s∈S .
Bemerkung 1.21. In der Situation von Definition 1.20 gilt offensichtlichα|X (T ) = α(T ) für alle T ∈ TΩ (X).
Definition 1.22. Wie in Definition 1.18 sei Σ = (S, Ω) eine Signatur, A =(As )s∈S , (fω )ω∈Ω eine Σ-Algebra und X = (Xs )s∈S ein Variablensystemzu Σ. Nun sei B die Menge aller Belegungen von X in A:

B := α = (αs )s∈S ∀ s ∈ S : αs ∈ Abb(Xs , As )Außerdem sei se ∈ S eine beliebige Sorte. Die Abbildung
wird definiert durch

interpretA : TΩ,es (X) → Abb(B, Aes )interpretA (T ) := α 7→ α(T ) .
Ist speziell X ein Variablensystem, das nur eine einzige Variable einer Sorte
s1 ∈ S enthält – Xs1 = {x} und Xs = ∅ für alle s ∈ S\{s1 } –, so kann man
die Menge B mit der Trägermenge As1 identifizieren; damit hat man danninterpretA : TΩ,es (X) → Abb(As1 , Aes ).

Ist X das leere Variablensystem (∅)s∈S , so enthält die Menge B der Belegungen nur ein einziges Element ((αs )s∈S , wobei die αs Abbildungen mit
leerer Definitionsmenge sind). In diesem Fall kann man Abb(B, Aes ) mit Aes
identifizieren und erhält somit AbbildungeninterpretA : TΩ,es → Aes .

Definition 1.23. Sei Σ eine Signatur und A eine Σ-Algebra. A heißt
Σ-generiert oder einfach generiert, wenn die Abbildungen interpretA : TΩ,es→ Aes für alle se ∈ S surjektiv sind. Diese Eigenschaft wird auch mit »nojunk« beschrieben [24]: Die Algebra hat keine anderen Elemente als die, diedurch Grundterme beschrieben werden können.
Definition 1.24. Sei Σ = (S, Ω) eine Signatur; A = (As )s∈S , (fω )ω∈Ω und
B = (Bs )s∈S , (gω )ω∈Ω seien Σ-Algebren. Eine Familie ϕ = (ϕs )s∈S von Abbildungen ϕs : As → Bs ist ein Homomorphismus von A nach B, wennfolgende Verträglichkeitsbedingungen erfüllt sind:(i) Für alle s ∈ S und jedes Konstantensymbol ω ∈ Ωλ,s gilt
ϕs (fω ) = gω .
(ii) Für alle w = s1 . . . sn ∈ S ∗ \{λ}, s ∈ S und jedes Operationssymbolω ∈ Ωw,s gilt

∀ a1 ∈ A1 , . . ., an ∈ An : ϕs fω (a1 , . . ., an ) = gω ϕs1 (a1 ), . . ., ϕsn (an ) .

141

Algebren

Abkürzend benutzt man auch die Notation ϕ : A → B.
Definition 1.25. Die Komposition von Homomorphismen ϕ : A → B,
ψ : B → C (wobei A, B und C Σ-Algebren seien) ist der durch ψ ◦ ϕ :=(ψs ◦ ϕs )s∈S definierte Homomorphismus A → C.
Bemerkung 1.26. Daß mit ϕ und ψ in der Tat auch ψ ◦ ϕ ein Homomorphismus ist, sieht man leicht anhand der Definition 1.24.
Bemerkung 1.27. Mit dem jetzt eingeführten Begriff des Homomorphismus stellt sich nachträglich heraus, daß Substitutionsauswertungen (Definition 1.11)
σ : TΩ (X) → TΩ (Y )als spezielle Homomorphismen
σ : TΣ (X) → TΣ (Y )zwischen den entsprechenden Termalgebren angesehen werden können.
Analog ist zu sehen, daß Auswertungen (Definition 1.18)
α : TΩ (X) → A
auch als Homomorphismen
α : TΣ (X) → A
aufgefaßt werden können.
Satz 1.28. Jeder Homomorphismus ϕ = (ϕs )s∈S : TΣ (X) → A von der
Termalgebra übereinem Variablensystem X in eine Σ-Algebra A =(As )s∈S , (fω )ω∈Ω wird als Auswertung durch die Belegung α = (αs )s∈S : X→ A induziert, welche durchαs (x) := ϕs term(x)für alle s ∈ S, x ∈ Xs gegeben ist.

Beweis. Seien s ∈ S und T ∈ TΩ,s (X) beliebig gegeben. Zu zeigen ist
αs (T ) = ϕs (T ). Der Beweis erfolgt durch Induktion über die Tiefe von T(Definition 1.6), die jeweils zu zeigende Behauptung folgt unmittelbar aus
den betreffenden Definitionen:
Falls T die Tiefe 0 hat, ist entweder T = term(x) mit x ∈ Xs oder T =term(ω) mit ω ∈ Ωλ,s . Im ersten Fall ist αs (T ) = αs (x) = ϕs (T ) nach Definition 1.18 und der Definition von αs , im zweiten Fall ist αs (T ) = fω = ϕs (T )nach Definition 1.18 und Definitionen 1.24 und 1.15 (ii).
Ist die Tiefe von T größer als 0, so ist T = ω(T1 , . . ., Tn ) mit ω ∈ Ωw,s , w =s1 . . . sn ∈ S ∗ \{λ}, wobei die Terme Ti ∈ TΣ,si (X) sämtlich eine geringere
Tiefe haben als T . Nach Definition 1.18 istαs ω(T1 , . . ., Tn ) = fω αs1 (T1 ), . . ., αsn (Tn ) ,1 Algebren

15

und nach Definitionen 1.24 und 1.15 (ii) ist

ϕs ω(T1 , . . ., Tn ) = fω ϕs1 (T1 ), . . ., ϕsn (Tn ) .
Wegen αsi (Ti ) = ϕsi (Ti ) für i ∈ {1, . . ., n} (laut Induktionsvoraussetzung)folgt die Behauptung.
Definition 1.29. Sei Σ = (S, Ω) eine Signatur und A = (As )s∈S , (fω )ω∈Ω
eine Σ-Algebra. Eine Kongruenz auf A ist eine Familie ≡ = (≡s )s∈S vonÄquivalenzrelationen ≡s auf As , die für alle w = s1 . . . sn ∈ S ∗ \{λ}, s ∈ S
und jedes ω ∈ Ωw,s folgende Verträglichkeitsbedingung erfüllt:e1 ∈ As1 , . . ., an , aen ∈ Asn : a1 ≡s1 a
e1 ∧ . . . ∧ an ≡sn aen∀ a1 , ae1 , . . ., aen ) .
⇒ fω (a1 , . . ., an ) ≡s fω (aDefinition 1.30. Sei Σ = (S, Ω) eine Signatur, A = (As )s∈S , (fω )ω∈Ω eineΣ-Algebra und ≡ = (≡s )s∈S eine Kongruenz auf A. Der Quotient von A
nach ≡ ist definiert als
A  :=
≡





As 
e
≡s s∈S , (fω )ω∈Ω ,

wobei folgendes gilt: As ≡ ist im gewöhnlichen Sinne der Quotient dersMenge As nach der Äquivalenzrelation ≡s (die Äquivalenzklasse von a ∈ As
wird im folgenden als [a]s notiert); für alle s ∈ S, ω ∈ Ωλ,s ist feω = [fω ]s ; undfür alle w = s1 . . . sn ∈ S ∗ \{λ}, s ∈ S, ω ∈ Ωw,s ist
feω :

Y 

1≤i≤n

As i 
As 
≡si →
≡s


gegeben durch∀ a1 ∈ As1 , . . . , an ∈ Asn : feω [a1 ]s1 , . . ., [an ]sn = fω (a1 , . . ., an ) s(die Wohldefiniertheit folgt aus der Verträglichkeitsbedingung für Kongruenzen, Definition 1.29).
Offenbar ist auch A ≡ eine Σ-Algebra.


Bemerkung1.31. In der Situation von Definition 1.30 bestehe die Familie[ . ] = [ . ]s s∈S aus den kanonischen Abbildungen[ . ]s : As → As ≡ ,

sd. h. jedes Element von As werde durch [ . ]s auf seine Äquivalenzklasse
abgebildet. Dann liegt ein Homomorphismus[ . ]: A → A ≡

von Σ-Algebren vor, wie man unmittelbar an den Definitionen erkennt.

16

1



AlgebrenSatz 1.32. A = (As )s∈S , (fω )ω∈Ω und B = (Bs )s∈S , (gω )ω∈Ω seine
Σ-Algebren, ϕ = (ϕs )s∈S ein Homomorphismus A → B und ≡= (≡s )s∈S
eine Kongruenz auf A. Es gelte000∀ s ∈ S : ∀ a, a ∈ As : a ≡s a ⇒ ϕs (a) = ϕs (a ) .










A =
As   , (fe )
und
[
.
]
=
[
.
]
seien gemäß Definitiωω∈Ωs≡≡s s∈Ss∈S
on 1.30 bzw. Bemerkung 1.31 definiert. Unter diesen Gegebenheiten existiert
genau ein Homomorphismus

ϕe = (ϕes )s∈S : A ≡ → B

mit

ϕ = ϕe ◦ [ . ].

Beweis. Für jedes s ∈ S ist die Abbildung ϕes : As ≡ → Bs durch die Forsederung ϕs = ϕs ◦ [ . ]s eindeutig festgelegt; sind nämlich [a], [a0 ] ∈ As ≡sbeliebig vorgegeben (a, a0 ∈ As ), so ist im Fall [a] = [a0 ] laut Voraussetzungauch ϕ(a) = ϕ(a0 ).
Zu zeigen bleibt, daß es sich bei der so definierten Familie ϕe tatsächlichum einen Homomorphismus handelt. Dies folgt direkt aus den Definitionen
unter Benutzung der Voraussetzung, daß ϕ ein Homomorphismus A → B
ist: Ist ω ∈ Ωλ,s (s ∈ S) ein beliebiges Konstantensymbol, so giltϕes (feω ) = ϕes [fω ]s = ϕs (fω ) = gω ;ist ω ∈ Ωw,s (w = s1 . . .sn ∈ S ∗ \{λ}, s ∈ S) ein beliebiges Operationssymbol,

so gilt für alle [a1 ] ∈ As1 ≡ , . . ., [an ] ∈ Asn ≡s1

ϕes feω [a1 ]s1 , . . ., [an ]sn

sn



 



= ϕes fω (a1 , . . ., an ) s
= ϕs fω (a1 , . . ., an )= gω ϕs1 (a1 ), . . ., ϕsn (an )






= gω ϕes1 [a1 ] , . . ., ϕesn [an ] .

1 Algebren

1.3

17

Die Kategorie Alg(Σ) zu einer Signatur

Kategorien stellen wir durch »hom-Mengen« dar [22], d. h. eine Kategorie C
besteht aus folgendem:(i) Einer Menge von Objekten (auch die Objektmenge wird mit C bezeichnet, z. B. »a ∈ C«)1 ;(ii) einer Abbildung, die jedem Paar (a, b) von Objekten eine Mengehom(a, b) zuordnet; deren Elemente heißen Morphismen von a in b,f

und man schreibt f ∈ hom(a, b) oft als Pfeil: f : a → b oder a −→ b (dieMorphismen sind in vielen der betrachteten Fälle, aber nicht notwendig, Abbildungen von a in b);(iii) zu jedem Tripel (a, b, c) von Objekten einer Abbildung(g, f ) 7→ g ◦a,b,c f : hom(b, c) × hom(a, b) → hom(a, c)(Komposition), so daß das Assoziativgesetz
h ◦a,c,d (g ◦a,b,c f ) = (h ◦b,c,d g) ◦a,b,d f
gilt; da meist klar ist, welche Komposition gemeint ist, wird einfachg ◦ f geschrieben für g ◦a,b,c f , und das Assoziativgesetz macht Klammerung verzichtbar (»h ◦ g ◦ f «);(iv) zu jedem Objekt b einem Element 1b ∈ hom(b, b), der Identität von b,
so daß für alle f ∈ hom(a, b), g ∈ hom(b, c) (mit Objekten a, c) gilt
1b ◦ f = fundg ◦ 1b = g.

Auf die sonst oft geforderte Disjunktheitsbedingung hom(a, b) 6= hom(a0 , b0 )für (a, b) 6= (a0 , b0 ) verzichten wir (sie läßt sich durch geeignetes Beschriften der Elemente der hom(a, b) erfüllen, d. h. durch Ersetzen von hom(a, b)
durch {a} × hom(a, b) × {b}).
Für hom(a, b) schreibt man auch homC (a, b), um den Bezug zur jeweiligen Kategorie klarzustellen; eine andere gebräuchliche Schreibweise ist
C(a, b). (Hätten wir die Disjunktheitsbedingung für hom-Mengen gefordert,so wäre für f ∈ hom(a, b) auch die Kurzschreibweise »f in C« möglich,dadann Objekte dom(f ) und cod(f ) mit f ∈ hom dom(f ), cod(f ) eindeutig
bestimmt wären.)Ein Morphismus f ∈ hom(a, b) heißt Isomorphismus, wenn es einenMorphismus g ∈ hom(b, a) gibt mit g ◦ f = 1a und f ◦ g = 1b . Man nennt
dann die Objekte a und b zueinander isomorph. (g, das Inverse von f , isteindeutig bestimmt: Denn ist auch g 0 ∈ hom(b, a) ein Inverses, d. h. g 0 ◦ f =1a und f ◦ g 0 = 1b , so folgt g 0 = g 0 ◦ 1b = g 0 ◦ f ◦ g = 1a ◦ g = g.)
Um beim Umgang mit Kategorien mengentheoretische Probleme zu
vermeiden (wie das Russelsche Paradoxon »{x | x 6∈ x}«), geht man von1
Vielfach wird allgemeiner eine Klasse von Objekten zugelassen; wir folgen [22] underlauben lediglich Mengen.

18

1

Algebreneinem Universum aus, d. h. von einer für die jeweiligen Zwecke genügend
großen Menge U , die folgende Abschlußeigenschaften erfüllt [22]:(i) x ∈ u ∈ U impliziert x ∈ U .
(ii) u ∈ U ∧ v ∈ U impliziert {u, v} ∈ U , (u, v) ∈ U und u × v ∈ U .
(iii) x ∈ U impliziert P(x) ∈ U (P(x) ist die Potenzmenge von x, d h. die
S
Menge {a | a ⊆ x}) und x ∈ U .
(iv) ω ∈ U , wobei ω = {0, 1, 2, . . .} die Menge aller endlichen Ordinalzahlen bezeichnet.
(v) Ist f : a → b mit a ∈ U und b ⊆ U eine surjektive Abbildung, so giltauch b ∈ U .
Wenn, wie in der folgenden Definition, eine Menge aller Σ-Algebren heranzuziehen wäre, so ist dabei implizit stets ein geeignetes Universum vorausgesetzt; nur Σ-Algebren aus diesem Universum sind zu betrachten.
Definition 1.33. Sei Σ = (S, Ω) eine Signatur. Die von den Σ-Algebren mit
ihren Homomorphismen (und der üblichen Komposition für Homomorphismen) gebildete Kategorie bezeichnen wir mit Alg(Σ).
Damit liegt in der Tat eine Kategorie vor: Da die Homomorphismen Familien von Abbildungen sind und die Komposition von Homomorphismen
komponentenweise durch die Komposition von Abbildungen definiert ist,
ist das Assoziativgesetz erfüllt; und zu jeder Σ-Algebra A ist die Familie
idA := (idAs )s∈S von konstanten Abbildungen offensichtlich ein Homomorphismus mit den für die Identität von A geforderten Eigenschaften.
Ein Objekt a einer Kategorie C heißt initial, wenn es für jedes Objekt bder Kategorie genau einen Morphismus von a in b gibt:∀ b ∈ C : # hom(a, b) = 1.
Ein Objekt b heißt final, wenn es für jedes Objekt a genau einen Morphismus von a in b gibt:∀ a ∈ C : # hom(a, b) = 1.
Eine Kategorie hat nicht notwendig initiale Objekte und hat nicht notwendig finale Objekte. Für den Fall der Existenz initialer oder finaler Objekte sieht man leicht: Alle initialen Objekte einer Kategorie sind zueinander isomorph, und alle finalen Objekte sind zueinander isomorph. Dies ist
eine unmittelbare Konsequenz der universellen Eigenschaft der initialen
bzw. finalen Objekte: Sind a1 und a2 beide initial, so gibt es eindeutig bestimmte Morphismen f : a1 → a2 und g : a2 → a1 ; da wegen der Initialität
von a1 auch der Morphismus a1 → a1 eindeutig bestimmt ist, gilt g◦f = 1a1 ;entsprechend gilt auch f ◦ g = 1a2 ; also sind f und g Isomorphismen. (Analog für finale Objekte.)
Aus der Eindeutigkeit der Inversen (S. 17) folgt, daß jedes Objekt, welches zu einem initialen oder finalen Objekt isomorph ist, selbst initial

1 Algebren

19bzw. final ist: Sei etwa a1 initial und a2 isomorph zu a1 mit Isomorphisfgmen a1 −→ a2 −→ a1 ; dann gilt für jedes Objekt b und das dazu eindeutig
bestimmte h1 ∈ hom(a1 , b) zwangsläufig hom(a2 , b) = {h1 ◦ g} (denn daßh1 ◦ g ∈ hom(a2 , b) ist, ist unmittelbar klar; und für h2 ∈ hom(a2 , b) gilth2 = h2 ◦ f ◦ g = h1 ◦ g, weil h2 ◦ f = h1 ist wegen # hom(a1 , b) = 1).
| {z }
1a2

Bemerkung 1.34. In Alg(Σ) ist TΣ , die Termalgebra über dem leeren Variablensystem (siehe (iii) in Definition 1.15), initial.
Beweis. Alle Auswertungen sind Homomorphismen (Bemerkung 1.27);
umgekehrt ist auch jeder Homomorphismus von einer Termalgebra in eine
beliebige Σ-Algebra die Auswertung einer Belegung (siehe Satz 1.28). Da
das leere Variablensystem
offensichtlich genau eine Belegung in A hat,folgt # hom(TΣ , A) = 1. Somit ist TΣ initial in Alg(Σ).
Bemerkung 1.35. In Alg(Σ) ist FinΣ , die triviale Σ-Algebra (siehe (i) in
Definition 1.15), final.
Beweis. Zu jeder Σ-Algebra A ist die Familie (fins )s∈S von Abbildungenfins : As → {•} = Fins eindeutig bestimmt. Sie ist offensichtlich ein Homomorphismus A → FinΣ ; also gilt # hom(A, FinΣ ) = 1, und demnach ist
FinΣ final in Alg(Σ).
C sei wieder eine beliebige Kategorie, und C ⊆ C sei eine beliebige
Teilmenge. Dann heißt a ∈ C bzw. b ∈ C initial in C bzw. final in C, wenn

∀ b ∈ C : # hom(a, b) = 1
bzw.
∀ a ∈ C : # hom(a, b) = 1
gilt. Der Begriff der Initialität läßt sich wie folgt verallgemeinern:
Definition 1.36. Sei Σ = (S, Ω) eine Signatur und X = (Xs )s∈S ein Variablensystem zu Σ. C sei eine Teilmenge
der Menge der Objekte von Alg(Σ).
Eine Algebra F = (Fs )s∈S , (ϕω )ω∈Ω ∈ C heißt in C frei über X, wenn es
eine Familie u = (us )s∈S von Abbildungen us: Xs → Fs gibt, so daß zu einer
vorgegebenen Algebra A = (As )s∈S , (fω )ω∈Ω ∈ C und einer vorgegeben Familie h = (hs )s∈S von Abbildungen hs : Xs → As stets genau ein Homomorphismus h = (hs ) : F → A existiert mit ∀ s ∈ S : ∀ x ∈ Xs : hs (x) = hs u(x) .
F ist in C frei über dem leeren Variablensystem (∅)s∈S genau dann,wenn F in C initial ist; für das leere Variablensystem spielen nämlich die
Abbildungen us , hs (s ∈ S) wegen leerer Definitionsbereiche Xs keine Rolleund es bleibt lediglich die Forderung der Existenz genau eines Homomorphismus F → A. Bemerkung 1.34 ist damit ein Sonderfall der folgenden
Bemerkung:
Bemerkung 1.37. Die Algebra TΣ (X) (siehe (ii) in Definition 1.15) ist freiüber X in Alg(Σ).

201AlgebrenBeweis. Die Abbildungen us : Xs → TΩ,s (X) seien für alle s ∈ S durch∀ x ∈ Xs : us (x) := term(x) definiert. Sind nun eine Algebra A und Abbildungen hs : Xs → As (s ∈ S) gegeben, so findet man einen Homomorphismus h : TΣ (X) → A als Auswertung (Definition 1.18) der Belegungh = (hs )s∈S , und nach Satz 1.28 ist h in der Tat auch der einzige solche
Homomorphismus mit h term(x) = hs (x) für alle s ∈ S, s ∈ Xs .

2 Algebraische Spezifikation durch GleichungenEine Signatur Σ = (S, Ω) erlaubt alleine kaum Aussagen darüber, welche Zusammenhänge in Σ-Algebren zwischen den durch Terme beschriebenen Elementen bestehen: Insbesondere kann man auf Gleichheit der
Werte zweier Terme unter beliebigen Belegungen der vorkommenden Variablen nur dann schließen, wenn die Terme selbst gleich sind; das zeigt
das Beispiel der Termalgebra. Um eine Möglichkeit zu erhalten, weitergehende Untersuchungen auf der Ebene der Terme ohne Festlegung einer bestimmten Algebra durchzuführen, kann man gewisse Forderungen an die
gewünschten Algebren in Form von formalen Gleichungen festlegen; diesführt zum Konzept der Gleichungsspezifikation. In Abschnitt 2.1 werden
Gleichungsspezifikationen und SPEC -Algebren definiert, ein Regelsystem
zum formalen Ableiten neuer formaler Gleichungen aus vorgegebenen wird
vorgestellt, und dessen Korrektheit und Vollständigkeit wird nachgewiesen. Abschnitt 2.2 schließt an Abschnitt 1.3 an und behandelt die Kategorie
der SPEC -Algebren zu einer vorgegebenen Gleichungsspezifikation.

2.1

SPEC -Algebren

Definition 2.1. Sei Σ = (S, Ω) eine Signatur. Eine formale Gleichung(der Sorte s) bezüglich Σ ist ein Tupel (X, L, R), wobei X ein Variablensystem zu Σ ist und L, R Terme ∈ TΩ (X) sind mit sortX (L) = sortX (R) (= s).
Definition 2.2. Sei g = (X, L, R) eine formale Gleichung. Wir verwenden
folgende Bezeichnungen für ihre Komponenten: X wird als das Variablensystem von g bezeichnet, L ist die linke Seite von g, R ist die rechte Seite
von g.
Definition 2.3. Eine Gleichungsspezifikation ist ein Tupel SPEC =(S, Ω, Ξ, G), wobei (S, Ω) eine Signatur, Ξ = (Ξs )s∈S ein Variablensystem zu(S, Ω) und G eine Menge von formalen Gleichungen bezüglich (S, Ω) ist, so
daß für alle g ∈ G das Variablensystem X = (Xs )s∈S von g die Forderung∀ s ∈ S : Xs ⊆ Ξs erfüllt.
Gleichungsspezifikationen werden in der Literatur oft auch als »algebraische Spezifikationen« bezeichnet. Entgegen der üblichen Darstellung schreiben wir schon in jeder Gleichungsspezifikation ein Variablensystem fest, das dann für sämtliche Terme als Basis genommen wird – dadurch werden Mehrdeutigkeiten hinsichtlich der Sortenzugehörigkeit der
Variablen von vornherein vermieden.
Definition 2.4. Sei Σ = (S, Ω) eine Signatur und A = (As )s∈S , (fω )ω∈Ω
eine Σ-Algebra. Eine formale Gleichung (X, L, R) ist gültig in A, wenn fürjede Belegung α = (αs )s∈S , αs : Xs → As , die Gleichung α(L) = α(R) erfüllt
ist.
Eine formale Gleichung hat man sich also als Ausdruck »L = R« vorzustellen, der für jede im Variablensystem X vorkommende Variable allquan21

22

2

Algebraische Spezifikation durch Gleichungentifiziert ist. (Die Angabe des Variablensystems X ist dabei nicht entbehrlich: Ist nämlich As = ∅ für eine Sorte s, so ist jede Gleichung (X, L, R) mit
Xs 6= ∅ zwangsläufig gültig in A, während eine ansonsten unveränderte
Gleichung (Y, L, R) mit Ys = ∅ nicht gültig zu sein braucht.)
Definition 2.5. Sei Σ = (S, Ω) eine Signatur und SPEC = (S, Ω, Ξ, G) eine Gleichungsspezifikation. Eine Σ-Algebra A heißt ein Modell von SPEC(auch: eine SPEC -Algebra), wenn jede formale Gleichung g ∈ G in A gültig
ist.
Die Definitionen der Begriffe Homomorphismus, Kongruenz und Quotient bleiben für die Betrachtung von SPEC -Algebren unverändert wie im
Fall der Σ-Algebren.
Der Gültigkeitsbegriff ergibt Möglichkeiten, aus bekannten Gleichungen weitere abzuleiten, die durch die bereits bekannten Gleichungen gerechtfertigt werden. Die spätere Definition 2.11 gibt Ableitungsregeln hierfür an; die Sätze 2.12 und 2.18 zeigen die Korrektheit sowie – unter bestimmten Voraussetzungen über das Variablensystem Ξ – die Vollständigkeit dieser Regeln. Auf diesem Weg wird schließlich die Existenz initialer
SPEC -Algebren nachgewiesen (Bemerkung 2.25).
Die Menge aller formaler Gleichungen, die zu gegebenen S, Ω und Ξ(wie in Definition 2.3) überhaupt denkbar sind, kann man wie folgt definieren:
Definition 2.6.
nGS,Ω,Ξ := (X, L, R) X = (Xs )s∈S

mit





∀ s ∈ S : Xs ⊆ Ξs ,o

∃ s ∈ S : L, R ∈ TΩ,s (X)Damit gilt für eine Gleichungsspezifikation (S, Ω, Ξ, G) in jedem Fall
G ⊆ GS,Ω,Ξ . Weil die zu betrachtende Gleichungsspezifikation hier als fest
vorgegeben angesehen wird, können wir auch als kürzere Notation G :=GS,Ω,Ξ setzen.
Daß Ξ = (Ξs )s∈S fest vorgegeben ist und die Ξs paarweise disjunkt sind,ermöglicht eine weitere Vereinfachung der Schreibweise: Variablensysteme X = (Xs )s∈S mit Xs ⊆ Ξs für s ∈ S kann man statt als Familien auchS
als Teilmengen von s∈S Ξs auffassen. Zu einer Familie (Xs )s∈S gehört die
SS
Menge X := s∈S Xs ; umgekehrt ist die zu X ⊆ s∈S Ξs gehörende Familie(Xs )s∈S gegeben durch Xs := X ∩ Ξs . Im folgenden sind Schreibweisen wie»X ⊆ Y «, »X ∪ Y «, »x ∈ X« oder »X = {x1 , . . ., xn }« in diesem Sinne zu
verstehen.
Außerdem kann man bei X ⊆ Ξ überall, wo die Abbildung sortX verwendet wird, statt ihrer gemäß Bemerkung 1.8 auch sortΞ verwenden; daΞ feststeht, schreiben wir für sortΞ einfach sort.
Definition 2.7. Sei M eine Menge. Eine Schlußregel R auf M »mit nPrä
missen« ist eine Teilmenge von M n × M (n ∈ N). Für (aν )1≤ν≤n , a ∈ Rschreibt man
a1 , . . ., an(R).
a2 Algebraische Spezifikation durch Gleichungen23

Die aν (1 ≤ ν ≤ n) bezeichnet man dabei als Prämissen, a heißt Folgerung.
Definition 2.8. Sei R = (Ri )i∈I eine Familie von Schlußregeln auf einer
Menge M , und die Familie (ni )i∈I von natürlichen Zahlen gebe die jeweiligen Prämissenanzahlen an (das heißt Ri ⊆ M ni × M für i ∈ I). Weiter seia ∈ M . Ein formaler Beweis für a (auch: eine Ableitung von a) aus den
Axiomen A ⊆ M mit dem Regelsystem R ist eine endliche Folge
a1 , . . ., ak(mit k ∈ N\{0}), so daß ak = a gilt und für jedes j ∈ {1, . . ., k} eine derfolgenden Bedingungen erfüllt ist:(i) aj ∈ A(ii) Es existiert ein i ∈ I und eine Familie (jν )1≤ν≤ni von natürlichen Zahlen mit 1 ≤ jν < j, so daß
aj1 , . . ., ajni
(Ri )
aj
gilt.
k wird als Länge des Beweises bezeichnet. Wenn es einen Beweis für a aus A
mit R gibt, heißt a beweisbar (auch: ableitbar). Dafür schreibt man kurz
A `R a.
Definition 2.9. Sei R ein Regelsystem auf M . Für beliebige TeilmengenA ⊆ M setzt manclR (A) := {a ∈ M | A `R a}
und nennt clR (A) den Abschluß (closure) von A.
Bemerkung 2.10. clR : P(M ) → P(M ) ist damit in der Tat ein Abschlußoperator (auch: Hüllenoperator), das heißt, clR hat folgende Eigenschaften(wie man leicht nachprüft):(i) Extensionalität: Für A ⊆ M gilt A ⊆ clR (A).
(ii) Monotonie: Für A, B ⊆ M mit A ⊆ B gilt clR (A) ⊆ clR (B).
(iii) Idempotenz: Für A ⊆ M gilt clR clR (A) = clR (A).
Auf diese Eigenschaften, namentlich auf (iii), wird in folgenden Beweisen
zurückgegriffen, ohne dies jeweils explizit kenntlichzumachen.
Definition 2.11. Die Schlußregeln
Rrefl ⊆ G 0 × G,
Rsymm ⊆ G 1 × G,
Rtrans ⊆ G 2 × G,
Rsubst1 ⊆ G 1 × G,
Rsubst2 ⊆ G 1 × G

24

2

Algebraische Spezifikation durch Gleichungenauf der Menge G = GS,Ω,Ξ der formalen Gleichungen enthalten jeweils genau
diejenigen Elemente, die sich durch die im folgenden angegebenen Darstellungen ergeben.
• Reflexivität: Es gilt
(X, T, T )(Rrefl )für alle Variablensysteme X ⊆ Ξ und alle T ∈ TΩ (X).
• Symmetrie: Es gilt
(X, T1 , T2 )(X, T2 , T1 )(Rsymm )für alle Variablensysteme X ⊆ Ξ und alle T1 , T2 ∈ TΩ (X) mit
sort(T1 ) = sort(T2 ).
• Transitivität: Es gilt
(X, T1 , T2 ), (X, T2 , T3 )(X, T1 , T3 )(Rtrans )für alle Variablensysteme X ⊆ Ξ und alle T1 , T2 , T3 ∈ TΩ (X) mit
sort(T1 ) = sort(T2 ) = sort(T3 ).
• Einfache Substitution: Es gilt
(X, T1 , T2 )Y, σ(T1 ), σ(T2 )(Rsubst1 )für alle Variablensysteme X, Y ⊆ Ξ, alle T1 , T2 ∈ TΩ (X) mit sort(T1 ) =sort(T2 ) und alle Substitutionen σ : X → TΩ (Y ) (siehe Definition 1.10
und Definition 1.11).
• Doppelte Substitution: Es gilt
(Y, T1 , T2 )
X ∪ Y, σ1 (T ), σ2 (T )(Rsubst2 )für alle Variablensysteme X, Y ⊆ Ξ, alle T ∈ TΩ (X), T1 , T2 ∈ TΩ (Y )mit sort(T1 ) = sort(T2 ) und Substitutionen σ1 , σ2 : X → TΩ (X ∪ Y )(siehe Definition 1.10 und Definition 1.11), die für jedes x ∈ X die
Bedingungσ1 (x) = σ2 (x)∨σ1 (x) = T1 ∧ σ2 (x) = T2

erfüllen.
R := (Ri )i∈{refl,symm,trans,subst1 ,subst2 } sei das aus diesen Schlußregeln bestehende Regelsystem. Da diese Definition von den zugrundeliegenden Mengen
S und Ω sowie vom Variablensystem Ξ abhängt, schreiben wir für R auchgenauer RS,Ω,Ξ .

2 Algebraische Spezifikation durch Gleichungen

25

Satz 2.12. Das in Definition 2.11 angegebene Regelsystem R = RS,Ω,Ξ ist
korrekt (sound): Ist SPEC = (S, Ω, Ξ, G) eine Gleichungsspezifikation, g ∈clR (G) und A eine beliebige SPEC -Algebra, so ist g gültig in A.
Beweis. Es reicht zu zeigen, daß für jedes Ri (i ∈ {refl, symm, trans, subst1 ,subst2 }) für beliebige in A gültige formale Gleichungen g1 , . . ., gn ∈ G (wobei
n die Prämissenanzahl von Ri sei) und für g ∈ G mit
g1 , . . ., gn
g

(Ri )

auch die formale Gleichung g in A gültig sein muß; denn durch Induktionüber die Längen (Definition 2.8) der Beweise von beliebigen g ∈ clR (G)folgt daraus die Behauptung des Satzes.
Es seien also i, g1 , . . ., gn und g gegeben. Im einzelnen seien die Benennungen so wie im jeweiligen Fall der Definition 2.11. Weiter sei α eine beliebige Belegung des Variablensystems von g. Zu zeigen ist, daß die Auswertung α für die linke Seite von g den gleichen Wert ergibt wie für die
rechte Seite von g.
• i = refl: α(T ) = α(T ) ist klar.
• i = symm: Nach der Voraussetzung über die Gültigkeit der formalen
Gleichung (X, T1 , T2 ) in A, die das gleiche Variablensystem hat wie(X, T2 , T1 ), ist in der Tat α(T2 ) = α(T1 ).
• i = trans: Weil (X, T1 , T2 ) und (X, T2 , T3 ) in A gültig sind, ist α(T1 ) =α(T2 ) = α(T3 ).
• i = subst1 : Die zu betrachtende Situation (gemäß Definition 2.11) ist(X, T1 , T2 )Y, σ(T1 ), σ(T2 )(Rsubst1 )mit einer beliebig vorgegebenen Substitution σ : X → TΩ (Y ). Durch
ϕ := (ϕs )s∈S := (αs ◦ σ s )s∈S definiert man (nach Bemerkung 1.26
und Bemerkung 1.27) einen Homomorphismus ϕ : TΣ (X) → A. Gemäß Satz 1.28 ist ϕ die Auswertung der Belegung α ◦ σ := (αs ◦ σs )s∈S
von X in A. Laut Voraussetzung ist (X, T1 , T2 ) gültig
in A; alsoistϕs (T1 ) = ϕs (T2 ) für s = sort(T1 ), das heißt αs σ s (T1 ) = αs σ s (T2 ) .
• i = subst2 : Nach Definition 2.11 sind Situationen(Y, T1 , T2 )
X ∪ Y, σ1 (T ), σ2 (T )(Rsubst2 )zu betrachten, wobei die Substitutionen σ1 , σ2 : X → TΩ (X ∪ Y ) für
alle x ∈ X die Bedingung
σ1 (x) = σ2 (x)∨σ1 (x) = T1 ∧ σ2 (x) = T2



(2.1)

26

2

Algebraische Spezifikation durch Gleichungenerfüllen. Wir zeigen durch Induktion über die Tiefe (Definition 1.6)
von T , daß für alle T ∈ TΩ (X)α σ1 (T ) = α σ2 (T )

(2.2)

ist.
Hat T die Tiefe 0, so sind drei Fälle zu unterscheiden:– Ist T = term(ω) mit einem ω ∈ Ωλ,sort(T ) , so ist σ1 (T ) = σ2 (T ),und also gilt (2.2).
– Ist T = term(x) mit einem x ∈ Xsort(T ) und gilt σ1 (x) = σ2 (x), so
gilt offensichtlich auch (2.2).
– Wegen (2.1) bleibt sonst nur der Fall T = term(x) mit einemx ∈ Xsort(t) , für das σ1 (x) = T1 und σ2 (x) = T2 ist. Wegen dervorausgesetzten Gültigkeit der formalen Gleichung (Y, T1 , T2 ) in
A ist α|Y (T1 ) = α|Y (T2 ). Für j ∈ {1, 2} ist

α σj (T ) = α σj (x) = α(Tj ) = α|Y (Tj )laut Bemerkung 1.21. Also gilt (2.2).
Hat T eine Tiefe > 0, so hat es die Form T = ω(T1 , . . ., Tn ), und dabei gilt die Behauptung laut Induktionsvoraussetzung für die Terme
T1 , . . ., Tn wegen deren geringerer Tiefe; das heißt, es ist α σ1 (Tj ) =α σ2 (Tj ) für 1 ≤ j ≤ n. Nach Definition 1.11 und Definition 1.18 folgt
daraus
α σ1 ω(T1 , . . ., Tn ) = α σ2 ω(T1 , . . ., Tn ) ,also (2.2).
Damit sind alle Möglichkeiten für i untersucht.
Definition 2.13. Sei Ξ = (Ξs )s∈S ein Variablensystem zu einer Signatur(Σ, Ω). Ξ heißt gesättigt, wenn für jedes s0 ∈ S und jedes w = s1 . . . sn ∈S ∗ \{λ}, für das ein s ∈ S existiert mit Ωw,s 6= ∅, die Menge Ξs mindestens# i ∈ {1, . . ., n} | si = s0Elemente hat.
Definition 2.14. SPEC = (S, Ω, Ξ, G) sei eine Gleichungsspezifikation mit
einem (bezüglich (S, Ω)) gesättigten Ξ, und es sei X ⊆ Ξ ein Variablensystem. Dann wird die Familie
T (X)

≡GΣ

T (X)

Σ
von zweistelligen Relationen ≡G,s

T (X)

Σ
T1 ≡G,sfür T1 , T2 ∈ TΩ,s (X).

T2

T (X) Σ
= ≡G,s:⇔s∈S

auf TΩ,s (X) definiert durch(X, T1 , T2 ) ∈ clR (G)2 Algebraische Spezifikation durch Gleichungen

27
T (X)

Satz 2.15. Die in Definition 2.14 festgelegte Familie ≡GΣist eine Kongruenz (Definition 1.29) auf der Σ-Algebra TΣ (X) (Definition 1.15).
T (X)Σ
Beweis. Daß die Relationen ≡G,sÄquivalenzrelationen sind, sieht man
direkt an den Regeln Rrefl , Rsymm und Rtrans aus Definition 2.11.
Indem wir außerdem die Regel Rsubst2 heranziehen, zeigen wir, daßTΣ (X)≡Gin der Tat eine Kongruenz ist: Dafür sei ω ∈ Ωw,s (w = s1 . . . sn ∈∗S \{λ}, s ∈ S) beliebig gegeben, und für j ∈ {1, . . ., n} seien Tj , Tej ∈TΣ (X) eTΩ,sj (X) Terme mit Tj ≡G,sTj (das heißt (X, Tj , Tej ) ∈ clR (G)). Zu zeigen
j

T (X)

Σ
ist, daß daraus ω(T1 , . . ., Tn ) ≡G,sω(Te1 , . . ., Ten ), also anders geschriebenX, ω(T1 , . . ., Tn ), ω(Te1 , . . ., Ten ) ∈ clR (G)(2.3)

folgt. Dafür werden wir im folgenden nachweisen, daß

X, ω(T1 , . . ., Tn ), ω(Te1 , T2 . . ., Tn ) ∈ clR (G)..
.
X, ω(Te1 , . . ., Tek−1 , Tk , . . ., Tn ), ω(Te1 , . . ., Tek , Tk+1 , . . ., Tn ) ∈ clR (G)..
.
X, ω(Te1 , . . ., Ten−1 , Tn ), ω(Te1 , . . ., Ten ) ∈ clR (G)gilt – also, zusammengefaßt notiert: Für jedes k ∈ {1, . . ., n} ist
X, ω(Lk1 , . . ., Lkn ), ω(R1k , . . ., Rnk ) ∈ clR (G)


(2.4)

mit
• Lkj := Rjk := Tej für j < k,• Lkj := Rjk := Tj für j > k,
• Lkk := Tk und Rkk := Tek .

Aus diesen n formalen Gleichungen erhält man durch n − 1 Anwendungender Regel Rtrans , daß in der Tat (2.3) gilt.
Zu zeigen bleibt noch (2.4). Dafür seien y1 ∈ Ξs1 , . . . , yn ∈ Ξsn paarweiseverschiedene Variablen – daß hierfür in Ξ von jeder Sorte genügend Variablen vorhanden sind, wird durch Definition 2.13 gewährleistet – und Y ⊆ Ξ
das aus diesen Variablen gebildete Variablensystem: Y := {y1 , . . ., yn }. Wirsetzen T := ω(y1 , . . ., yn ). Nun seien Substitutionen σ1 , σ2 : Y → TΩ (X) festgelegt durch σ1 (yj ) := Lkj , σ2 (yj ) := Rjk für j ∈ {1, . . ., n}. Für j 6= k gilt
damit σ1 (yj ) = σ2 (yj ), und es ist σ1 (yk ) = Tk sowie σ2 (yk ) = Tek . Wegen
der Voraussetzung (X, Tk , Tek ) ∈ clR (G) darf also die Regel Rsubst2 wie folgt
angewendet werden:(X, Tk , Tk )kX ∪ Y, ω(L1 , . . ., Lkn ), ω(R1k , . . ., Rnk )
e

|

{z

=σ1 (T )} |{z=σ2 (T )}(Rsubst2 )28

2Algebraische Spezifikation durch GleichungenUm von dieser Folgerung zu (2.4) zu gelangen, sei σ : X ∪ Y → TΩ (X) eine
Substitution mit σ(x) := term(x) für x ∈ X. Für y ∈ Y mit y 6∈ X kann σ(y)beliebig aus TΩ,sort(y) (X) gewählt werden (die Bedingung TΩ,sort(y) (X) 6= ∅,so daß ein σ der gewünschten Art tatsächlich existiert, ist erfüllt; denn esgilt Tj ∈ TΩ,sort(y) (X) für das j mit yj = y). Terme aus TΩ (X) werden durch
σ nicht verändert, also folgt jetzt
X ∪ Y, ω(Lk1 , . . ., Lkn ), ω(R1k , . . ., Rnk )X, ω(Lk1 , . . ., Lkn ), ω(R1k , . . ., Rnk )(Rsubst1 ),und somit gilt (2.4).
Definition 2.16. In der Situation von Definition 2.14 setzt man weiter
TSPEC (X) := TΣ (X)

.

T (X)

≡GΣ

(siehe Definition 1.30); für jedes s ∈ S setzt man dabei
TSPEC ,s (X) := TΩ,s (X).

T (X) .

Σ≡G,sSatz 2.17. TSPEC (X) ist eine SPEC -Algebra.
Beweis. Klar ist wegen der Definition als Quotient aus einer Σ-Algebra undeiner Kongruenz darauf, daß TSPEC (X) eine Σ-Algebra ist. Zu zeigen ist,
daß alle formalen Gleichungen aus G in TSPEC (X) gültig sind. Dafür sei
eine beliebige Gleichung (Y, L, R) ∈ G vorgegeben mit einem Variablensystem Y = (Ys )s∈S ; und α = (αs )s∈S , αs : Ys → TSPEC ,s (X), sei eine beliebige
Belegung von Y in TSPEC (X). Zu zeigen ist jetzt, daß α(L) = α(R) ist.
Zunächst sei zu α eine Substitution σ = (σs )s∈S : Y → TΩ (X) so gewählt, daß∀ y ∈ Y : σ(y) sort(y) = α(y)ist; hierbei bezeichnet σ(y) sort(y) entsprechend Definition 1.30 die Äquivalenzklasse von σ(y) ∈ TΩ,sort(y) (X) bezüglich der Äquivalenzrelation
T (X)Σ≡G,sort(y). Nun stellen wir fest, daß der Homomorphismus

α : TΣ (Y ) → TSPEC (X)
die Komposition [ . ] ◦ σ der Homomorphismen
σ : TΣ (Y ) → TΣ (X)und[ . ] : TΣ (X) → TSPEC (X)T (X)ist, wobei [ . ] = ([ . ]s )s∈S gemäß Bemerkung 1.31 von der Kongruenz ≡GΣinduziert
wird. Das heißt, für jedes T ∈ TΩ,s (Y ), s ∈ S beliebig, gilt α(T ) =σ(T ) s . Dies sieht man mit Induktion über die Tiefe (Definition 1.6) von T
an den Definitionen von α und σ (Definition 1.18 und 1.11).

2 Algebraische Spezifikation durch Gleichungen29



Wegen (Y, L, R) ∈ G ergibt sich G `R X, σ(L), σ(R) laut Definition 2.8
mit der Schlußregel Rsubst1 aus Definition 2.11. Also ist gemäß DefinitiTΣ (X)
on 2.14 σ(L) ≡G,sort(L)
σ(R), d. h. σ(L) s = σ(R) s (mit s := sort(L) =sort(R)). Wegen α(L) = σ(L) s und α(R) = σ(R) s folgt hieraus die Behauptung.
Satz 2.18. Das in Definition 2.11 angegebene Regelsystem R ist vollständig (complete) für Gleichungsspezifikationen SPEC = (S, Ω, Ξ, G), bei denen das Variablensystem Ξ gesättigt (Definition 2.13) ist: Ist g ∈ GS,Ω,Ξ eineformale Gleichung, die in jeder SPEC -Algebra gültig ist, so ist g ∈ clR (G).
Beweis. Sei g = (X, T1 , T2 ), s = sort(T1 ) (= sort(T2 )). Wir betrachten die
SPEC -Algebra TSPEC (X). Der Satz ist bewiesen, wenn man gezeigt hat,
daß im Fall g 6∈ clR (G) die formale Gleichung g nicht in TSPEC (X) gültig
ist.

Für die Belegung α : X → TSPEC (X) mit α(x) = term(x) sort(x) für allex ∈ X ergibt sich α(T1 ) = [T1 ]s und α(T2 ) = [T2 ]s (wie man mit DefiniTΣ (X)tion 1.30 leicht sieht). Aus der Annahme g 6∈ clR (G) folgt T1 6≡G,sT2 ,das heißt [T1 ]s 6= [T2 ]s . Somit ist α(T1 ) 6= α(T2 ), und also ist (X, T1 , T2 ) nicht
gültig in TSPEC (X).
Beispiel 2.19. Wir zeigen eine Gleichungsspezifikation, die den Begriff
der kommutativen Gruppe ausdrückt. Für formale Gleichungen (X, L, R)
schreiben wir dabei suggestiver X : L = R. Bei Termen verwenden wir
für zweistellige Operationssymbole eine Infixschreibweise, d. h. T1 + T2
steht für +(T1 , T2 ). Klammern werden gesetzt, soweit dies zur Eindeutigkeit der Baumdarstellung
der Terme nötig ist; z. B. steht T1 + (T2 + T3 ) für+ T1 , +(T2 , T3 ) .
Sei Σ := (S, Ω) mit S := {s1 }, Ωλ,s1 := {0}, Ωs1 ,s1 := {−}, Ωs1 s1 ,s1 := {+}und mit Ωw,s1 := ∅ für alle w ∈ S ∗ \ {λ, s1 , s1 s1 }. Weiter sei Ξ := (Ξs )s∈S mit
der einzigen Komponente Ξs1 := {x, y, z}, und es seinG := {x} :x + 0 = x,{x} :x + (−x) = 0,{x, y} :x + y = y + x,

{x, y, z} :(x + y) + z = x + (y + z) .

o

Schließlich sei SPEC := (S, Ω, Ξ, G).

Eine Σ-Algebra A := (As )s∈S , (fω )ω∈Ω ist genau dann ein Modell dieser Gleichungsspezifikation SPEC , wenn die Menge As1 mit der Operation f+ : A × A → A die Struktur einer kommutativen Gruppe hat, wobei
f0 ∈ As1 das Nullelement dieser Gruppe ist und f− : As1 → As1 jedem Element von As1 sein Inverses zuordnet.
Als einfaches Beispiel für einen formalen
Beweis zeigen wir die Schritteeiner Herleitung von {x} : (−x) + x = 0 :

{x, y}, x + y, y + x{x}, (−x) + x, x + (−x)(Rsubst1 )30

2

Algebraische Spezifikation durch Gleichungen{x}, (−x) + x, x + (−x) , {x}, x + (−x), 0{x}, (−x) + x, 0(Rtrans )Beispiel 2.20. Auf Basis von Beispiel 2.19 geben wir nun eine Gleichungsspezifikation an, deren Modelle aus zwei kommutativen Gruppen bestehen
und einen Gruppenhomomorphismus von der ersten in die zweite dieser
Gruppen enthalten.
Es sei Σ := (S, Ω) mit S := {s1 , s2 },Ωλ,s1 := {01 },Ωλ,s2 := {02 },Ωs1 ,s1 := {−1 },Ωs2 ,s2 := {−2 },Ωs1 s1 ,s1 := {+1 },Ωs2 s2 ,s2 := {+2 },Ωs1 ,s2 := {ϕ}und mit Ωw,s := ∅ für alle anderen (w, s). Nun sei Ξ := (Ξs )s∈S mit
Ξs1 := {x1 , y1 , z1 } und Ξs2 := {x2 , y2 , z2 }, und die Menge G der formalen
Gleichungen sei definiert durch
G := {x1 } :nx1 +1 01 = x1 ,{x2 } :

x2 +2 02 = x2 ,{x1 } :

x1 +1 (−x1 ) = 01 ,{x2 } :

x2 +2 (−x2 ) = 02 ,{x1 , y1 } :x1 +1 y1 = y1 +1 x1 ,{x2 , y2 } :x2 +2 y2 = y2 +2 x2 ,{x1 , y1 , z1 } :(x1 +1 y1 ) +1 z1 = x1 +1 (y1 +1 z1 ),{x2 , y2 , z2 } :(x2 +2 y2 ) +2 z2 = x2 +2 (y2 +2 z2 ),o{x1 , y1 } :ϕ(x1 +1 y1 ) = ϕ(x1 ) +2 ϕ(y1 ) .

Beispiele für Modelle
von SPEC := (S, Ω, Ξ, G) sind die Σ-Algebren A :=(As )s∈S , (fω )ω∈Ω mit
As1 := Z n Z


1

und

As2 := Z n Z ,2wobei n1 , n2 ∈ Z ganze Zahlen sind mit n2 | n1 (hierbei ist auch n1 = 0
zugelassen – für diesen Fall sei ∀ n2 ∈ Z : n2 | 0 und Z 0 Z = Z vereinbart), und jeweils den natürlichen Additionen f+1 , f+2 , den natürlichen
Nullelementen f01 , f02 und den natürlichen Inversenabbildungen f−1 , f−2
und beliebigen Gruppenhomomorphismen
fϕ : Z n Z → As2 := Z n Z ,


1



2

z. B. der natürlichen Projektion
fϕ : x + n1 Z 7→ x + n2 Z
oder der konstanten Abbildung
fϕ : x + n1 Z 7→ 0 + n2 Z.

2 Algebraische Spezifikation durch Gleichungen

31

Beispiel 2.21. Wir ergänzen das vorangegangene Beispiel 2.20 noch um
ein zusätzliches Konstantensymbol 11 für die erste Sorte sowie um eineformale Gleichung für die zweite Sorte, die besagt, daß alle Elemente derzweiten Gruppe eine Gleichung der Form a+a = 0 erfüllen sollen, d. h. jedes
Element außer dem Nullelement muß die Ordnung 2 haben.
Hier sei SPEC := (S, Ω, Ξ, G) mit S := {s1 , s2 },Ωλ,s1 := {01 , 11 },Ωλ,s2 := {02 },Ωs1 ,s1 := {−1 },Ωs2 ,s2 := {−2 },Ωs1 s1 ,s1 := {+1 },Ωs2 s2 ,s2 := {+2 },Ωs1 ,s2 := {ϕ},Ωw,s := ∅ für alle anderen (w, s), Ξ := (Ξs )s∈S mit Ξs1 := {x1 , y1 , z1 } undΞs2 := {x2 , y2 , z2 },G := {x1 } :nx1 +1 01 = x1 ,{x2 } :

x2 +2 02 = x2 ,{x1 } :

x1 +1 (−x1 ) = 01 ,{x2 } :

x2 +2 (−x2 ) = 02 ,{x1 , y1 } :x1 +1 y1 = y1 +1 x1 ,{x2 , y2 } :x2 +2 y2 = y2 +2 x2 ,{x1 , y1 , z1 } :(x1 +1 y1 ) +1 z1 = x1 +1 (y1 +1 z1 ),{x2 , y2 , z2 } :(x2 +2 y2 ) +2 z2 = x2 +2 (y2 +2 z2 ),{x1 , y1 } :{x2 } :

ϕ(x1 +1 y1 ) = ϕ(x1 ) +2 ϕ(y1 ),ox2 +2 x2 = 02 .

Von den in Beispiel 2.20 angegebenen Modellen bleiben diejenigen mit n2 =
1 oder n2 = 2 bestehen. Die hinzugekommene Konstante f11 ∈ Z n Z kann1
in jedem Fall beliebig gewählt werden, da sie in keine der Gleichungeneingeht.

32

2

2.2

Algebraische Spezifikation durch Gleichungen

Die Kategorie Alg(SPEC ) zu einer Gleichungsspezifikation

Eine Unterkategorie einer Kategorie C ist eine Kategorie C0 , die folgende
Voraussetzungen erfüllt:• Die Menge der Objekte von C0 ist eine Teilmenge der Menge der Objekte von C;• für a, b ∈ C0 ist homC0 (a, b) ⊆ homC (a, b);• für a, b, c ∈ C0 , f ∈ homC0 (a, b), g ∈ homC0 (b, c) ist g ◦ f in der Kategorie
C0 das gleiche wie in C.
Gilt hierbei homC0 (a, b) = homC (a, b) für alle a, b ∈ C0 , so heißt C0 eine volle
Unterkategorie von C.
Definition 2.22. Sei SPEC = (S, Ω, Ξ, G) eine Gleichungsspezifikation und
Σ = (S, Ω) die zugrundeliegende Signatur. Mit Alg(SPEC ) bezeichnen wir
die volle Unterkategorie von Alg(Σ) (Definition 1.33) mit denjenigen Objekten von Alg(Σ), die Modelle von SPEC sind.
Bemerkung 2.23. Für jede Gleichungsspezifikation
SPEC = (S, Ω, Ξ, G)haben SPEC und SPEC cl := S, Ω, Ξ, clRS,Ω,Ξ (G) die gleichen Modelle, also
Alg(SPEC ) = Alg(SPEC cl ).
Diese Aussage ist eine Neuformulierung der Feststellung, daß das Regelsystem RS,Ω,Ξ korrekt ist (Satz 2.12).
Bemerkung 2.24. Seien SPEC = (S, Ω, Ξ, G) und SPEC 0 = (S, Ω, Ξ0 , G)
Gleichungsspezifikationen mit Ξ = (Ξs )s∈S , Ξ0 = (Ξ0s )s∈S , ∀ s ∈ S : Ξs ⊆ Ξ0s .
Dann haben SPEC und SPEC 0 die gleichen Modelle:
Alg(SPEC ) = Alg(SPEC 0 )In Alg(SPEC ) gibt es initiale und finale Algebren:
Bemerkung 2.25. Sei SPEC = (S, Ω, Ξ, G) eine Gleichungsspezifikation.
Es kann o. B. d. A. angenommen werden, daß das Variablensystem Ξ gesättigt ist; denn es existiert offensichtlich in jedem Fall ein Variablensystem Ξ0 , das sowohl die Voraussetzungender Bemerkung 2.24 erfüllt, so
daß Alg (S, Ω, Ξ, G) = Alg (S, Ω, Ξ0 , G) ist, als auch den Anforderungendes Sättigungsbegriffs (Definition 2.13) genügt. Die somit gemäß Definition 2.16 gegebene Algebra TSPEC := TSPEC (∅) (wobei ∅ das leere Variablensystem (∅)s∈S bezeichnet) ist eine initiale SPEC -Algebra; für den Beweis
wird auf die nachfolgende, allgemeinere Bemerkung 2.26 verwiesen.
Die finale Σ-Algebra FinΣ (S. 12) ist offensichtlich auch in Alg(SPEC )final.
Bemerkung 2.26. X ⊆ Ξ sei ein Variablensysten (Ξ sei dabei wiedero. B. d. A. gesättigt). Dann ist TSPEC (X) in Alg(SPEC ) frei über X (Definition 1.36).

2 Algebraische Spezifikation durch Gleichungen33

Beweis. [ . ] = [ . ]s s∈S sei die Familie der kanonischen Abbildungen (BeT (X)merkung 1.31) zur Kongruenz ≡GΣ(Definition 2.14) auf der Σ-AlgebraTΣ (X). Die Familie u = (us)s∈S von Abbildungen us : Xs → TSPEC ,s (X)sei definiert durch us (x) := term(x) s für alle x ∈ Xs . Eine SPEC -Alge
bra A = (As )s∈S , (fω )ω∈Ω und eine Familie h = (hs )s∈S von Abbildungen
hs : Xs → As seien beliebig vorgegeben.
TΣ (X) ist frei über X in Alg(Σ) (Bemerkung 1.37); demzufolge gibt esgenau einen Homomorphismus ϕ = (ϕs )s∈S : TΣ (X) → A mit ϕs term(x) =hs (x) für alle s ∈ S, x ∈ Xs . Da A eine SPEC -Algebra ist, gilt
h

T (X)

0
Σ
∀ s ∈ S : ∀ T, T ∈ TΩ,s (X) : T ≡G,si

T 0 ⇒ ϕs (T ) = ϕs (T 0 ) ;also läßt sich Satz 1.32 anwenden: Demnach gibt es genau einen Homomorphismus
ϕe = (ϕes )s∈S : TΣ (X).

T (X) = TSPEC (X) → A≡GΣ

mit ϕ = ϕe ◦ [ . ].
Ein Homomorphismus h : TSPEC (X) → A erfüllt genau dann die Bedingung ∀ s ∈ S : ∀ x ∈ Xs : hs (x) = hs term(x) s ,
also




∀ s ∈ S : ∀ x ∈ Xs : hs (x) = hs ◦ [ . ]s term(x) ,wenn h ◦ [ . ] = ϕ ist; dies folgt aus der bereits erwähnten Eindeutigkeit
von ϕ. Somit erfüllt h := ϕe das gemäß Definition 1.36 Verlangte und ist
eindeutig bestimmt.

3

Erweiterungen von Gleichungsspezifikationen

Wir haben gesehen, wie mittels des Regelsystems für formale Gleichungen(Definition 2.11) zu einer Gleichungsspezifikation SPEC Eigenschaften gefunden werden können, die sämtlichen SPEC -Algebren gemein sind: Nach
Satz 2.18 über die Vollständigkeit des Regelsystems läßt sich jede formale
Gleichung ableiten, die in allen SPEC -Algebren gültig ist. Es kann jedochweitere auf alle SPEC -Algebren zutreffende Eigenschaften von Interesse
geben, die hierdurch nicht erfaßt sind – denn manche Eigenschaft läßt sichgar nicht erst als formale Gleichung aus GS,Ω,Ξ ausdrücken.
Beispiel 3.1. Die folgende Gleichungsspezifikation beschreibt Halbgruppen mit neutralem Element: Sei SPEC 0 = (S0 , Ω0 , Ξ0 , G0 ) mit S0 := {s0 },Ω0 = (Ωw,s )(w,s)∈S0∗ ×S0 , Ωλ,s0 := {1}, Ωs0 s0 ,s0 := {·} und Ωw,s0 := ∅ für w ∈S0∗ \ {λ, s0 s0 }, Ξ0 := (Ξs )s∈S mit der einzigen Komponente Ξs0 := {x, y, z}und
G0 := {x} :nx · 1 = x,{x} :1 · x = x,{x, y, z} :(x · y) · z = x · (y · z)o(wobei die formalen Gleichungen wie in Beispiel 2.19 erläutert notiertsind). Anders als bei Gruppen muß in Halbgruppen mit neutralem Element
nicht jedes Element Inverse haben. Deshalb läßt sich die bekannte Tatsache, daß – die jeweilige Existenz vorausgesetzt – ein Linksinverses und ein
Rechtsinverses eines Elements zwangsläufig gleich sind, nicht durch eine formale Gleichung ausdrücken; der Vollständigkeitssatz hilft hier nicht
weiter.
Eine Möglichkeit, derartige weitergehende Tatsachen auszudrücken
und formal zu beweisen, ergibt sich durch die Zuhilfenahme geeigneter
Erweiterungen der ursprünglichen Spezifikation.
Definition 3.2. Seien Σ0 = (S0 , Ω0 ) und Σ1 = (S1 , Ω1 ) (Ωi = (Ωiw,s )(w,s)∈Si∗ ×Si
für i ∈ {0, 1}) Signaturen mit S0 ⊆ S1 und Ω0 ⊆ Ω1 (d. h. für w ∈ S0∗ unds ∈ S0 gelte stets Ω0w,s ⊆ Ω1w,s ). Dann wird Σ0 als Subsignatur von Σ1bezeichnet, und Σ1 heißt Erweiterung der Signatur Σ0 .
Definition 3.3. SPEC 0 = (S0 , Ω0 , Ξ0 , G0 ) und SPEC 1 = (S1 , Ω1 , Ξ1 , G1 ) seien Gleichungsspezifikationen mit S0 ⊆ S1 , Ω0 ⊆ Ω1 , Ξ0 ⊆ Ξ1 und G0 ⊆ G1
(insbesondere sei also (S0 , Ω0 ) eine Subsignatur von (S1 , Ω1 )). Dann wird
SPEC 0 als Subspezifikation von SPEC 1 und SPEC 1 als Erweiterung
der Gleichungsspezifikation SPEC 0 bezeichnet.
Definition 3.4. Es seien Signaturen Σ0 = (S0 , Ω0 ) und Σ1 = (S1 , Ω1 ) gegeben; Σ1 sei einer Erweiterung von Σ0 . Nun sei A1 = (As )s∈S1 , (fω )ω∈Ω1 eine
Σ1 -Algebra. Die durch(A1 )Σ0 := (As )s∈S0 , (fω )ω∈Ω034



3 Erweiterungen von Gleichungsspezifikationen

35

definierte Σ0 -Algebra heißt Einschränkung von A1 auf Σ0 .
Speziell seien Σ0 und Σ1 die Signaturen aus Gleichungsspezifikationen
SPEC 0 = (S0 , Ω0 , Ξ0 , G0 ) und SPEC 1 = (S1 , Ω1 , Ξ1 , G1 ), SPEC 1 eine Erweiterung von SPEC 0 und A1 eine SPEC 1 -Algebra. Unter diesen Voraussetzungen ist (A1 )Σ0 notwendig eine SPEC 0 -Algebra (die Gültigkeit aller zu
betrachtenden formalen Gleichungen folgt aus der Voraussetzung G0 ⊆ G1 );man schreibt dann für (A1 )Σ0 auch (A1 )SPEC 0 und bezeichnet es als Einschränkung von A1 auf SPEC 0 .
Von Interesse sind für uns solche Erweiterungen SPEC 1 einer vorgegebenen Gleichungsspezifikation SPEC 0 , deren Modelle durch Einschränkung auf SPEC 0 genau alle Modelle von SPEC 0 ergeben: Damit haben
nämlich alle aus SPEC 1 gefolgerten formalen Gleichungen eine Bedeutung
für jede SPEC 0 -Algebra.
»Konservative Erweiterungen« im Sinne von [5], Def. 6.12 (S. 152), erfüllen unsere Anforderung nicht: An solche wird lediglich gefordert, daß der
Homomorphismus
TSPEC 0 → (TSPEC 1 )SPEC 0
von der initialen SPEC 0 -Algebra in die Einschränkung der initialen
SPEC 1 -Algebra auf SPEC 0 bijektiv sein soll. Damit bleiben diejenigen Elemente der Trägermengen der Algebren außen vor, die nicht durch einen
Grundterm beschrieben werden können:
Beispiel 3.5. SPEC 0 := (S, Ω, Ξ, G0 ) und SPEC 1 := (S, Ω, Ξ, G1 ) seien die
Gleichungsspezifikationen mit S := {s}, Ω := (Ωw,s )(w,s)∈S ∗ ×S , Ωλ,s := {1},Ωw,s :=∅ für w ∈ S ∗ \{λ}, G0 := ∅ und G1 := {x, y : x = y}. Dann ist
TΩ,s = term(1) , und somit sind TSPEC 0 ,s und TSPEC 1 ,s (Definition 2.16)
beide einelementig; da es keine weitere Sorte gibt, ist der Homomorphismus TSPEC 0 → (TSPEC 1 )SPEC 0 bijektiv. Es liegt also eine konservative Erweiterung vor. Jedoch gibt es SPEC 0 -Algebren, in denen die Trägermenge
von s mehrere Elemente enthält; diese können keine Einschränkungen vonSPEC 1 -Algebren sein, denn in SPEC 1 -Algebren hat die Trägermenge von sinfolge der Gleichung »x = y« stets nur ein Element.
(Nur, wenn man lediglich generierte Algebren (Definition 1.23) in Betracht zieht, leistet die Definition der konservativen Erweiterungen dashier von uns Gewünschte.)
Wir benutzen folgende Definition:
Definition 3.6. Die Gleichungsspezifikation SPEC 1 = (S1 , Ω1 , Ξ1 , G1 ) sei
eine Erweiterung der Gleichungsspezifikation SPEC 0 = (S0 , Ω0 , Ξ0 , G0 )(Ωi = (Ωiw,s )(w,s)∈§∗i ×Si für i ∈ {0, 1}). Wir nennen SPEC 1 eine vorsichtige
Erweiterung von SPEC 0 , wenn die folgenden Anforderungen erfüllt sind:(i) Neue Sorten haben keine Konstantensymbole: Für alle s ∈ S1 \ S0 istΩ1λ,s = ∅.
(ii) Neue Operationssymbole gibt es nur, soweit eine der Argumentsorten
neu ist: Für w ∈ S0∗ , s ∈ S1 gilt Ω1w,s = Ω0w,s bei s ∈ S0 und Ω1w,s = ∅ beis ∈ S 1 \ S0 .

36

3Erweiterungen von Gleichungsspezifikationen(iii) Neue Gleichungen enthalten neue Operationssymbole: Für g ∈ G1 \ G0kommt in der linken oder in der rechten Seite von g ein Operationssymbol aus einem Ω1w,s mit w ∈ S1∗ \ S0∗ , s ∈ S1 vor.
Ist SPEC 1 eine vorsichtige Erweiterung von SPEC 0 , so läßt sich zu einer beliebig vorgegebenen SPEC 0 -Algebra A0 stets eine SPEC 1 -Algebra A1
finden, deren Einschränkung auf SPEC 0 gerade A0 ist: Es gibt nämlich immer die Möglichkeit, für sämtliche Trägermengen von Sorten aus S1 \ S0
die leere Menge zu wählen (und alle Trägermengen der übrigen Sorten aus
A0 zu übernehmen, wie Definition 3.4 es in jedem Fall erzwingt); die hinzugekommenen Operationssymbole spielen dann keine Rolle, so daß auchdie hinzugekommenen formalen Gleichungen unbeachtlich bleiben. ÜberSPEC 1 -Algebren, die nicht in dieser Weise trivial sind, kann man dagegenmit aus SPEC 1 gefolgerten formalen Gleichungen gegebenenfalls zusätzliche Erkenntnisse über A0 erlangen.
Beispiel 3.7. Wir erweitern die Gleichungsspezifikation SPEC 0 aus
Beispiel 3.1 zur Gleichungsspezifikation SPEC 1 := (S1 , Ω1 , Ξ1 , G1 ) mit
S1 := {s0 , s1 }, Ω1 := (Ωw,s )(w,s)∈S1∗ ×S1 mit der neuen KomponenteΩs1 ,s0 := {ϕ, ϕL , ϕR } (die übrigen Komponenten von Ω bleiben, soweit
sie nicht schon in Beispiel 3.1 festgelegt wurden, leer), Ξ1 := (Ξs )s∈S mit
Ξs1 := {x1 } (Ξs0 wie in Beispiel 3.1),nϕL (x1 ) · ϕ(x1 ) = 1,{x1 } :

ϕ(x1 ) · ϕR (x1 ) = 1 .

G1 := G0 ∪ {x1 } :oNun lassen sich mit dem Regelsystem für formale Gleichungen leicht folgende Kongruenzen (siehe Definition 2.14) zeigen:TΣ ({x1 })ϕL (x1 ) ≡G11,s0

ϕL (x1 ) · 1TΣ ({x1 })≡G11,s0ϕL (x1 ) · ϕ(x1 ) · ϕR (x1 )TΣ ({x1 })≡G11,s0ϕL (x1 ) · ϕ(x1 ) · ϕR (x1 )TΣ ({x1 })≡G11,s0TΣ ({x1 })≡G11,s0

1 · ϕR (x1 )ϕR (x1 )

Es ist also {x1 }, ϕL (x1 ), ϕR (x1 ) ∈ clRS1 ,Ω1 ,Ξ1 (G1 ).
In Modellen A = (As )s∈S , (fω )ω∈Ω von SPEC 1 ist As0 , da eine vorsichtige Erweiterung der Gleichungsspezifikation SPEC 0 vorliegt, genau wie
in Beispiel 3.1 eine Halbgruppe mit der Multiplikation f· und dem neutralen Element f1 ; die neue Trägermenge As1 kann beliebig festgelegt werden,
und die Operationen fϕ , fϕL , fϕR : As1 → As0 müssen dazu so gewählt werden, daß∀ a1 ∈ As1 : f· fϕL (a1 ), fϕ (a1 ) = f1 = f· fϕ (a1 ), fϕR (a1 )3 Erweiterungen von Gleichungsspezifikationen

37

gilt. Die oben hergeleitete formale Gleichung besagt (laut Satz 2.12 überdie Korrektheit des Regelsystems für formale Gleichungen), daß unter diesen Gegebenheiten∀ a1 ∈ As1 : fϕL (a1 ) = fϕR (a1 )ist. Entfernt man sich nun von der Ebene der formalen Gleichungen undbeschränkt sich auf einelementige Mengen As1 = {a1 }, so kann man diese
Schlußfolgerungen mit a := fϕ (a1 ), aL := fϕL (a1 ), aR := fϕR (a1 ) auch lesenals∀ a, aL , aR ∈ As0 : f· (aL , a) = f1 = f· (a, aR ) ⇒ aL = aR ;die Erweiterung des ursprünglichen Gleichungssystems um die neue Sorte s1 und die Operationssymbole ϕ, ϕL , ϕR ∈ Ωs1 ,s0 entspricht also grob einem solchen Allquantor.

4

Endlichkeitsspezifikationen

Im Hinblick auf unser Vorhaben, algebraisch beschriebene Petrinetze mitmöglicherweise unendlich nebenläufigen Schaltvorgängen zu untersuchen,sind Gleichungsspezifikationen noch nicht ausreichend, wie ein späteres
Beispiel illustrieren wird. Zur angemessenen Behandlung benötigen wir
zusätzliche Beschreibungsmittel, um die Unendlichkeit in den Griff bekommen zu können. Hierzu führt Abschnitt 4.1 dieser Arbeit den Begriff
des Endlichkeitsterms ein; eine Gleichungsspezifikation mit hinzugefügten Endlichkeitstermen bezeichnen wir als Endlichkeitsspezifikation, ihre
Modelle als SPECF -Algebren. Ein Regelsystem wird angegeben, das das
formale Ableiten weiterer Endlichkeitsterme ermöglicht. Wie schon für
Σ-Algebren und SPEC -Algebren wird dann in Abschnitt 4.2 auf die Kategorie der SPECF -Algebren eingegangen. Abschnitt 4.3 zeigt, wie die Konzepte für Erweiterungen von Gleichungsspezifikationen aus Abschnitt 3 auf
Endlichkeitsspezifikationen übertragen werden können.

4.1

SPECF -Algebren

Definition 4.1. Sei Σ = (S, Ω) eine Signatur, Ξ ein Variablensystem zu Σ
und A eine Σ-Algebra. Für s ∈ S, T ∈ Ts,Ω (Ξ) bezeichne Bvar(T ),A die Menge aller Belegungen des minimalen Variablensystems zu T (Definition 1.9)
in A. T heißt ein Endlichkeitsterm für A, wenn für alle a ∈ As die Mengeα ∈ Bvar(T ),A | α(T ) = a

endlich ist.
Definition 4.2. Eine Endlichkeitsspezifikation ist ein Tupel SPECF =(S, Ω, Ξ, G, T fin ), wobei (S, Ω, Ξ, G) eine Gleichungsspezifikation (Definition 2.3) ist und T fin = (Tsfin )s∈S eine Familie von Mengen Tsfin ⊆ TΩ,s (Ξ).
Definition 4.3. Sei SPECF = (S, Ω, Ξ, G, T fin ) eine Endlichkeitsspezifikation. A sei ein Modell (Definition 2.5) der Gleichungsspezifikation (S, Ω, Ξ, G).
A wird als Modell von SPECF (auch: SPECF -Algebra) bezeichnet, wennfür alle s ∈ S jedes T ∈ Tsfin ein Endlichkeitsterm für A ist.
Offensichtlich gilt folgendes:
Bemerkung 4.4. Sei SPEC = (S, Ω, Ξ, G) eine Gleichungsspezifikation.
Die Endlichkeitsspezifikation
SPECF SPEC := S, Ω, Ξ, G, (∅)s∈S

mit leeren Mengen von Endlichkeitstermen hat die Eigenschaft, daß jedes
Modell von SPEC (Definition 2.5) auch ein Modell von SPECF SPEC (Definition 4.3) ist.
Zu einer vorliegenden Endlichkeitsspezifikation SPECF lassen sich gegebenenfalls weitere Terme finden, die Endlichkeitsterme für sämtliche38

4 Endlichkeitsspezifikationen

39

SPECF -Algebren sind. Zum Finden solcher zusätzlicher Endlichkeitsterme
verwenden wir das folgende Regelsystem. Speziell (vgl. Bemerkung 4.4)
kann man auch auch ausgehend von einer Gleichungsspezifikation SPEC
Terme finden, die für jede SPEC -Algebra Endlichkeitsterme sind.
Definition 4.5. Zu SPEC = (S, Ω, Ξ, G) wird das Regelsystem Rfin
SPEC , kurz
fin
fin
fin
R , definiert als R := (Ri )i∈N∪{G} , wobei die Schlußregeln
iRifin ⊆ TΩ (Ξ) × TΩ (Ξ)
fin
RG
⊆

0

TΩ (Ξ)(i ∈ N),× TΩ (Ξ)

genau die im folgenden angegebenen Elemente enthalten:• Es giltt(R0fin )für alle s ∈ S, t ∈ Ωλ,s ∪ Ξs .
• Sei T ∈ TΩ (Ξ) mit var(T) = {x1 , . . ., xn } (n ∈ N\{0}beliebig) und seienT1 ∈ TΩ,sort(x1 ) var(T ) , . . . , Tn ∈ TΩ,sort(xn ) var(T ) Terme mit:(i) T ist Unterterm (Definition 1.7) jedes Tk (1 ≤ k ≤ n);(ii) außerhalb der Vorkommnisse von T kommen in den Tk keineVaeriablen vor (d. h. ist x ∈ Ξsort(T ) , so gibt es Tk ∈ TΩ {x} mit
Tk = σ(Tek ) für σ : {x} → TΩ var(T ) , σ(x) := T );(iii) gemäß dem Regelsystem für formale Gleichungen
aus Definiti
on 2.11 ist var(T ), x1 , T1 , . . ., var(T ), xn , Tn ∈ clRS,Ω,Ξ (G).
Dann gilt
T

fin
(RG
).

• Für T ∈ TΩ (Ξ) mit var(T ) = {x1 , . . ., xi } (i ∈ N\{0}) giltT, σ(x1 ), . . ., σ(xi )σ(T )(Rifin )für alle Substitutionen σ : var(T ) → TΩ (Ξ).
fin mag es zunächst seltsam erscheinen, daß die VorBei der Regel RG
aussetzungen var(T ), xk , Tk ∈ clRS,Ω,Ξ (G) nicht formal als Prämissen gehandhabt werden, z. B. indem das Regelsystem mit Schlußregeln auf dem
Coprodukt (d. h. einer »disjunkten Vereinigung«) der Mengen TΩ (Ξ) und
GS,Ω,Ξ anstelle von Schlußregeln nur auf TΩ (Ξ) definiert wird. Da jedoch
die Folgerungen ausschließlich Terme sind und keine neuen formalen Gleichungen abgeleitet werden können, ist die gewählte Darstellung die natürlichere.

Satz 4.6. SPEC = (S, Ω, Ξ, G) sei eine beliebige Gleichungsspezifikation.
Das Regelsystem Rfin = Rfin
SPEC für Endlichkeitsterme ist korrekt: Ist
SPECF = (S, Ω, Ξ, G, T fin ) eine auf SPEC aufbauende
Endlichkeitsspezifinfikation, T ∈ clRfin (T ) und A = (As )s∈S , (fω )ω∈Ω eine beliebige SPECF Algebra, so ist T ein Endlichkeitsterm für A.

40

4

Endlichkeitsspezifikationen

Beweis. Sei i ∈ N ∪ G beliebig gegeben; wir betrachten die Schlußregel Ri .
Bei i ∈ {0, G} hat Ri keine Prämissen; für diese Fälle zeigen wir, daß jede Folgerung (Definition 2.7) von Ri ein Endlichkeitsterm für A sein muß.
Bei i ∈ N\{0} betrachten wir eine Situation gemäß der Darstellung beim
entsprechenden Fall der Definition 4.5 und zeigen, daß unter der Voraussetzung, daß T , σ(x1 ), . . . , σ(xn ) sämtlich Endlichkeitsterme für A sind,auch σ(T ) ein Endlichkeitsterm sein muß. Sind alle Fälle von i untersucht,
so folgt durch Induktion über die Länge von formalen Beweisen (Definition 2.8) für jedes T ∈ clRfin (T fin ), daß es ein Endlichkeitsterm für A ist.
Zunächst betrachten wir den Fall i = 0. Die Folgerungen von R0 sind
Terme, die lediglich aus einem Konstantensymbol oder einer Variablen bestehen: T = term(t), t ∈ Ωλ,s ∪ Ξs . Bei t ∈ Ωλ,s ist var(T ) = ∅, und damit
hat Bvar(T ),A , die Menge der Belegungen des minimalen Variablensystem
von T in A, nur ein einziges Element. Bei t ∈ Ξs ist var(T ) = {t} einelementig, und man kann Bvar(T ),A mit der Trägermenge As identifizieren: Fürjedes a ∈ As gibt es dann genau ein Element α ∈ Bvar(T ),A mit α(T ) = a. In
beiden Fällen ist für jedes a ∈ As die Mengeα ∈ Bvar(T ),A | α(T ) = a

endlich und T also laut Definition ein Endlichkeitsterm für A.
Im Fall i = G erfüllt die Folgerung T ∈ TΩ (Ξ) die Bedingung, daß zu{x1 , . . ., xn } ∈ var(T ) Terme Tk ∈ TΩ,sort(xk ) var(T ) (k ∈ {1, . . ., n}) existie
ren, die sämtlich T zum Unterterm haben und für die var(T ), xk , Tk ∈clRS,Ω,Ξ (G) gilt – in jeder Belegung α ∈ Bvar(T ),A ist alsoα(xk ) = α(Tk )laut Satz 2.12 über die Korrektheit von RS,Ω,Ξ – und die sich als
Tk = σ(Tek )schreiben lassen mit
σ : {x} → TΩ var(T )σ(x) = T
und Tek ∈ TΩ {x} . Wir zeigen für diese Situation, daß es zu einem vorgegebenen a ∈ Asort(T ) nur ein einziges α ∈ Bvar(T ),A geben kann mit α(T ) = a(womit T also ein Endlichkeitsterm für A ist); anders gesagt, durch α(T )sind die α(xk ) (k ∈ {1, . . ., n}) sämtlich eindeutig bestimmt. Dies aber ist
nach den Voraussetzungen klar, denn es istα(xk ) = α(Tk ) = (α ◦ σ)(Tek ),und da α ◦ σ als Homomorphismus TΣ {x} → A angesehen werden kann(Bemerkungen 1.27 und 1.26), ist es gemäß Satz 1.28 die Auswertung einer
Belegung {x} → A und somit in der Tat durch (α ◦ σ)(x) = α(T ) eindeutig
festgelegt.

4 Endlichkeitsspezifikationen

41

Schließlich untersuchen wir den Fall i ∈ N\{0}. Sei a ∈ Asort(T ) =Asort(σ(T )) vorgegeben. Damit für eine Belegung α : var σ(T ) → A
die Gleichung α σ(T ) = a erfüllt sein kann, muß für die Belegung
β : {x1 , . . ., xi } → A mit β(xk ) := (α ◦ σ)(xk ) (k ∈ {1, . . ., i}) die Gleichungβ(T ) = a erfüllt sein. Es gibt aber nur endlich viele solche Belegungen βlaut der Voraussetzung, daß T ein Endlichkeitsterm für A ist, und zu jederderartigen Belegung
β gibt es für jedes k nur endlich viele Belegungenαk : var α(xk ) → A mit α σ(xk ) = β(xk ), denn auch σ(xk ) ist laut Voraussetzung ein Endlichkeitsterm für A; also gibt es wegenvar α(T ) =[var α(xk )k∈{1,...,i}auch nur endlich viele α, deren sämtliche Einschränkungen αk :=α|var(α(xk )) derartige Gleichungen erfüllen. Damit kann es zum gegebe
nen a insgesamt nur endlich viele Belegungen α geben mit α σ(T ) = a.
Somit ist σ(T ) tatsächlich ein Endlichkeitsterm für A.
Eine offene Frage ist, ob für das Regelsystem Rfin auch ein Vollständigkeitssatz gilt, d. h. ob jeder Endlichkeitsterm sämtlicher SPECF -Algebren
darin einen formalen Beweis besitzt. Ebenfalls offen ist die Frage, ob möglicherweise eine Endlichkeitsspezifikation für alle ihre Modelle die Gültigkeit von formalen Gleichungen erzwingen kann, die nicht in allen Modellen
der zugrundeliegenden Gleichungsspezifikation gültig sind.
Beispiel 4.7. Wir betrachten SPEC SPECF (gemäß Bemerkung 4.4) für die
Gleichungsspezifikation SPEC aus Beispiel 2.21. Wir wollen
x1 +1 11 ∈ clRfin

SPEC(∅)s∈Sfin : Es ist var(x + 1 ) = {x }, undnachweisen. Das geschieht mit Regel RG1  1 1
1
für den Term T1 := (x1 +1 11 ) +1 (−1 11 ) gilt {x1 }, x1 , T1 ∈ clRS,Ω,Ξ (G), wie
man leicht nachweist; außerdem ist x1 +1 11 ein Unterterm von T1 und in
T1 kommen sonst keine Variablen vor. Somit hat man

x1 +1 11

fin
(RG
).

Beispiel 4.8. Wir ergänzen die Gleichungsspezifikation SPEC = (S, Ω, Ξ,G) aus Beispiel 2.21 zu einer Endlichkeitsspezifikation
SPECF := (S, Ω,

fin
fin
fin
Ξ, G, T ) mit T:= (Ts )s∈S , Ts1 := ∅, Ts2 := ϕ(x1 ) . Modelle von
SPECF sind definitionsgemäß diejenigen Modelle A = (As )s∈S , (fω )ω∈Ω
von SPEC , bei denen der Homomorphismus fϕ : As1 → As2 zu jedem Element von As2 nur endlich viele Urbilder besitzt – aus Beispiel 2.21 bleiben
diejenigen Modelle übrig, bei denen n1 6= 0 gilt (so daß also die Menge
As1 = Z n Z endlich ist).
1
Wir wollen mit dem Regelsystem aus Definition 4.5 nachweisen, daßfür beliebige Variablen y ∈ Ξs1 die Terme ϕ(y) und ϕ(y +1 11 ) Endlichkeitsterme für jede SPECF -Algebra sind. Für ϕ(y) ergibt sich das durch die424Endlichkeitsspezifikationen

Substitution σ : {x1 } → TΩ (Ξ) mit σ(x1 ) := y wie folgt aus ϕ(x1 ) ∈ Ts1 :y(R0fin )ϕ(x1 ), yϕ(y)(R1fin )(denn σ ϕ(x1 ) = ϕ(y)). Für ϕ(y +1 11 ) zeigt man zunächst analog zu Beispiel 4.7
fin
(RG
)
y +1 11und dann mit σ(x1 ) := y +1 11
ϕ(x1 ), y +1 11
ϕ(y +1 11 )(R1fin ).

4 Endlichkeitsspezifikationen

4.2

43

Die Kategorie Alg(SPECF ) zu einer Endlichkeitsspezifikation

Definition 4.9. Sei SPECF = (S, Ω, Ξ, G, T fin ) eine Endlichkeitsspezifikation und SPEC = (S, Ω, Ξ, G) die zugrundeliegende Gleichungsspezifikation.
Alg(SPECF ) ist die volle Unterkategorie von Alg(SPEC ) (Definition 2.22)
mit denjenigen Objekten, die Modelle von SPECF sind.
In Alg(SPECF ) gibt es zwar finale Algebren (die triviale Σ-Algebra
FinΣ ist auch eine SPECF -Algebra), jedoch – anders als in Alg(Σ) undAlg(SPEC ) – im allgemeinen keine initialen Algebren, wie das folgende
Beispiel zeigt.
Beispiel 4.10. Sei SPECF := (S, Ω, Ξ, G, T fin ) mit S := {s1 , s2 , s3 }, Ω :=(Ωw,s )(w,s)∈S ∗ ×S ,
Ωλ,s1 := {01 , 11 },Ωλ,s2 := {02 },Ωs1 ,s1 := {−1 },Ωs2 ,s2 := {−2 },Ωs1 s1 ,s1 := {+1 },Ωs2 s2 ,s2 := {+2 },Ωs1 ,s2 := {ϕ1 },Ωs2 ,s3 := {ϕ2 },Ωw,s := ∅ für alle anderen (w, s), Ξ := (Ξs )s∈S , Ξ1 := {x1 , y1 , z1 }, Ξ2 :={x2 , y2 , z2 }, Ξ3 := {x3 , y3 },G := {x1 } :nx1 +1 01 = x1 ,{x2 } :

x2 +2 02 = x2 ,{x1 } :

x1 +1 (−x1 ) = 01 ,{x2 } :

x2 +2 (−x2 ) = 02 ,{x1 , y1 } :x1 +1 y1 = y1 +1 x1 ,{x2 , y2 } :x2 +2 y2 = y2 +2 x2 ,{x1 , y1 , z1 } :(x1 +1 y1 ) +1 z1 = x1 +1 (y1 +1 z1 ),{x2 , y2 , z2 } :(x2 +2 y2 ) +2 z2 = x2 +2 (y2 +2 z2 ),{x1 , y1 } :ϕ1 (x1 +1 y1 ) = ϕ1 (x1 ) +2 ϕ1 (y1 ),{x3 , y3 } :x3 = y3 ,o

T fin := (Tsfin )s∈S , Tsfin:= ∅, Tsfin:= ∅, Tsfin:= ϕ2 (x2 ) .
1
2
3Modelle der zugrundeliegenden Gleichungsspezifikation
SP EC :=
(S, Ω, Ξ, G) sind Algebren A = (As )s∈S , (Ωw,s )(w,s)∈S ∗ ×S mit kommutativen Gruppen A1 und A2 (wobei f+i die Addition, f0i das neutrale Element, f−i die Invertierungsabbildung von Ai ist) und einer einelementigen
Menge A3 ; dabei ist f11 ein beliebiges Element von A1 , fϕ1 ein Gruppenhomomorphismus von A1 in A2 und fϕ2 die konstante Abbildung von A2 auf
das einzige Element von A3 .
In Modellen von SPECF muß außerdem ϕ2 (x2 ) ein Endlichkeitstermsein, d. h. A2 darf nur endlich viele Elemente haben. Beispiele für SPECF 44

4Endlichkeitsspezifikationen

Algebren erhält man mit den Gruppen
A1 := Z und

A2 := Z n Z ,n ∈ Z\{0}, und der natürlichen Projektion
fϕ1 : Z → Z n Z .
Gäbe es eine initiale SPECF -Algebra, so müßte die Trägermenge von s1
darin unendlich sein, denn die Grundterme
T1 := 11 , T2 := 11 +1 11 ,
T3 := (11 +1 11 ) +1 11 , T4 := (11 +1 11 ) +1 11 +1 11 , . . . beschreiben in den
oben genannten Beispielen für SPECF -Algebren paarweise verschiedene
Elemente. Die Trägermenge von s2 dagegen ist in jeder SPECF -Algebra
endlich; also müßte
es ein k ∈ N\{0} geben, für das in der initialen Al
gebra evals2 ϕ1 (Tk ) = evals2 (02 ) wäre. Das aber ist nicht damit vereinbar,
daß evals2 ϕ1 (Tk ) 6= evals2 (02 ) gilt in der oben angegebenen Beispielalgebra mit A2 = Z n Z , n = k+1: Im Widerspruch zur Definition der Initialität
könnte es keinen Homomorphismus von der initialen in die Beispielalgebra geben. Somit existiert zur gegebenen Endlichkeitsspezifikation SPECF
keine initiale SPECF -Algebra.

4 Endlichkeitsspezifikationen

4.3

45

Erweiterungen von Endlichkeitsspezifikationen

Das in Abschnitt 3 über Erweiterungen von Gleichungsspezifikationen Gesagte läßt sich im wesentlichen unverändert auf Endlichkeitsspezifikationen übertragen:Definition 4.11. SPECF 0 = (S0 , Ω0 , Ξ0 , G0 , T0fin ) und SPECF 1 = (S1 , Ω1 ,
Ξ1 , G1 , T1fin ) seien Endlichkeitsspezifikationen; dabei sei SPEC 0 := (S0 , Ω0 ,
Ξ0 , G0 ) eine Subspezifikation von SPEC 1 := (S1 , Ω1 , Ξ1 , G1 ) (Definition 3.3)
und T0fin ⊆ T1fin . Dann heißt SPECF 0 Subspezifikation von SPECF 1 undumgekehrt SPECF 1 Erweiterung von SPECF 0 .
Definition 4.12. In der Situation von Definition 4.11 sei A1 eine SPECF 1 Algebra. (A1 )SPEC 0 (Definition 3.4) ist dann notwendig eine SPECF 0 -Algebra; man schreibt für (A1 )SPEC 0 auch (A1 )SPECF 0 und spricht von der Einschränkung von A1 auf SPECF 0 .
Definition 4.13. In der Situation von Definition 4.11 ist SPECF 1 einevorsichtige Erweiterung von SPECF 0 , wenn SPEC 1 eine vorsichtige Erweiterung von SPEC 0 (Definition 3.6) ist und jeder Endlichkeitsterm aus
T1fin \ T0fin mindestens eine Variable einer Sorte aus S1 \ S0 enthält.
Diese Definition für vorsichtige Erweiterungen von Endlichkeitsspezifikationen stellt sicher, daß die Konstruktion von Seite 36 weiterhin anwendbar ist: Zu jeder SPECF 0 -Algebra A0 läßt sich somit eine SPECF 1 Algebra A1 finden mit (A1 )SPECF 0 = A0 .

5Multimengen und gewichtete Mengen

Die Definition der gefärbten Petrinetze beruht wesentlich auf dem Konzept
der Multimenge. Eine Multimenge M über einer Menge A kann man sichvorstellen als eine Sammlung von Elementen a ∈ A, die anders als bei »gewöhnlichen« Mengen auch eine Vielfachheit M (a) ∈ N haben. Allgemeiner
ist der Begriff der gewichteten Menge, bei der die Gewichtungen auch negativ sein dürfen. Da wir Petrinetze mit unendlichen Markierungen undunendlich nebenläufigen Schaltvorgängen zulassen wollen, benötigen wirüber die bei Multimengen und gewichteten Mengen üblichen Begriffe hinaus eine Reihe von neuen Definitionen: Wir behandeln die Addierbarkeit
einer Familie von gewichteten Mengen, die Auswertungsverträglichkeit einer gewichteten Menge mit einer Abbildung oder mit einer gewichteten
Menge von Abbildungen sowie die Verträglichkeit zweier gewichteter Mengen miteinander bezüglich einer zweistelligen Abbildung.
Definition 5.1. Für eine Menge A ist
M± (A) := Abb(A, Z)
die Menge aller gewichteten Mengen über A und
M(A) := Abb(A, N) ⊆ M± (A)die Menge aller nichtnegativ gewichteten Mengen oder Multimengenüber A. Für M ⊆ M± (A), a ∈ A wird die Zahl M (a) als Gewichtung von ain M bezeichnet.
Definition 5.2. Zu M ∈ M± (A) definiert man den Träger (support) von
M als supp(M ) := {a ∈ A | M (a) 6= 0} ⊆ A.
Definition 5.3. Eine gewichtete Menge M ∈ M± (A) heißt leer, wennsupp(M ) = ∅ ist.
Definition 5.4. Eine gewichtete Menge M ∈ M± (A) heißt endlich,wenn supp(M ) eine endliche Menge ist; andernfalls heißt M unendlich. M±
fin (A) ist die Menge aller endlichen gewichteten Mengen über A,
Mfin (A) = M±fin (A) ∩ M(A) die Menge aller endlichen Multimengen über A.
Definition 5.5. Sei M ∈ M± (A). a ∈ A ist ein Element von M , wenn
M (a) 6= 0 ist. Ist M (a) = n, so heißt a ein n-faches Element von M . Fürendliches M heißtX#(M ) :=M (a)a∈A

die Elementanzahl von M .
Bemerkung 5.6. Eine endliche gewichtete Menge M ∈ M±
fin (A) mit#(M ) = 0 ist nicht notwendig leer im Sinne von Definition 5.3. Ist jedoch
M ∈ Mfin (A) eine endliche Multimenge, so hat die Summe in Definition 5.5
keine negativen Summanden, und es gilt #(M ) = 0 genau dann, wenn M
leer ist.
46

5 Multimengen und gewichtete Mengen47

Wie allgemein für Abbildungen nach Z, sind für M, N ∈ M± (A), z ∈ Z
gewichtete Mengen M + N , M − N und z · M definiert durch(M + N )(a) := M (a) + N (a),(M − N )(a) := M (a) − N (a)und(z · M )(a) := z · M (a)für a ∈ A. Mit diesen Definitionen ist M± (A) ein Z-Modul (und damit
eine abelsche Gruppe bezüglich +). M±
fin (A) ist ein Untermodul (und ei±
ne Untergruppe) von M (A), denn für M, N ∈ M±
fin (A) und z ∈ Z ist±
M + N ∈ M±
(A)
und
z
·
M
∈
M
(A).
fin
fin
Ferner hat man auf M± (A) die Ordnungsrelation ≤ mit
M ≤N

:⇔

∀ a ∈ A : M (a) ≤ N (a).

Analog ist auf M± (A) die Ordnungsrelation ≥ definiert.
∅A bezeichnet die leere Multimenge über A:∅A (a) := 0
für alle a ∈ A. Ist x ∈ A, so schreiben wir {|x|} für die einelementige Multimenge über A, die durch{|x|}(x) := 1,{|x|}(a) := 0 für a ∈ A\{x}definiert ist. Für x1 , . . ., xk ∈ A (mit k ∈ N\{0}) wird die Multimenge{|x1 , . . ., xk }| definiert durch{|x1 , . . ., xk }| := {|x1}| + · · · + {|xk }| .
Für Ae ⊆ A ist χAe die durchee) := 1 für ae ∈ A,χAe(aχAe(a) := 0 für a ∈ A\Aedefinierte Multimenge über A. ({|x|} ist also das gleiche wie χ{x} .)Definition 5.7. Sei A eine Menge und (Mi )i∈I eine Familie von gewichteten
Mengen Mi ∈ M± (A). Die Familie (Mi )i∈I heißt addierbar, wenn für jedesa ∈ A nur endlich viele i ∈ I mit Mi (a) 6= 0 existieren. Dann ist die SummeP
der Familie (Mi )i∈I definiert als die gewichtete Menge i∈I Mi ∈ M± (A)
mit


X
i∈I

für a ∈ A.

Mi (a) :=Xi∈I

Mi (a)

48

5

Multimengen und gewichtete Mengen

Bemerkung 5.8. Sind (Mi )i∈I und (Ni )i∈I addierbare Familien von gewichteten Mengen Mi , Ni ∈ M± (A), so ist auch die Familie (Mi + Ni )i∈I
addierbar, und es gilt
X

(Mi + Ni ) =

i∈I

X

Mi +

i∈I

X

Ni .

i∈I

Beweis. Wie man leicht sieht, sind für jedes a ∈ A die gemäß Definition 5.7
zu überprüfenden Bedingungen erfüllt.
Definition 5.9. Seien A, B Mengen und f : A → B eine Abbildung. Eine gewichtete Menge M ∈ M± (A) heißt auswertungsverträglich mit f , wenn
für jedes b ∈ B die Mengea ∈ supp(M ) | f (a) = b

endlich ist. M±
f (A) bezeichne die Menge aller gewichteten Mengen über A,
die mit f auswertungsverträglich sind. Für M ∈ M±
f (A) definiert man die±
gewichtete Menge f (M ) ∈ M (B) durchf (M ) (b) :=X

M (a).

a∈Af (a)=bf bezeichnet damit außer der ursprünglichen Abbildung A → B auch±eine Abbildung M±
f (A) → M (B).
±
Bemerkung 5.10. Es ist offensichtlich M±
fin (A) ⊆ Mf (A) für beliebige±
Abbildungen f : A → B, und für M ∈ M±
fin (A) ist f (M ) ∈ Mfin (B).

Definition 5.11. Seien A, B Mengen und F ∈ M± Abb(A, B) . Eine gewichtete Menge M ∈ M± (A) heißt auswertungsverträglich mit F , wenn
für jedes b ∈ B die Menge(f, a) ∈ supp(F ) × supp(M ) | f (a) = b

endlich ist. M±
F (A) bezeichne die Menge aller gewichteten Mengen über A,
die mit F auswertungsverträglich sind. Für M ∈ M±
F (A) definiert man die±
gewichtete Menge F (M ) ∈ M (B) durch
F (M ) :=X

F (f ) · M (a).

(f,a)∈supp(F )×supp(A)f (a)=b

Mit dieser Definition induziert die gewichtete Menge F eine ebenfalls±
mit F bezeichnete Abbildung M±
F (A) → M (B).
Bemerkung 5.12. Ist eine Multimenge M ∈ M(A) auswertungsverträglich mit einer Multimenge F ∈ M Abb(A, B) , so ist auch F (M ) eine Multimenge (die Vielfachheiten der Elemente von F (M ) können nicht negativ
werden).

5 Multimengen und gewichtete Mengen

49

Durch F := {|f }| findet man Definition 5.9 in Definition 5.11 als Spe±±zialfall wieder; denn es ist M±
f (A) = M{|f}| (A), und für M ∈ Mf (A) ist
f (M ) = {|f }| (M ).
Bemerkung 5.13. Sei F ∈ M±
fin Abb(A, B) eine endliche gewichtete Menge und M ∈ M± (A) eine gewichtete Menge. Ist für jedes f ∈ supp(F ) die
gewichtete Menge M auswertungsverträglich mit f im Sinne der Definition 5.9, so ist M auswertungsverträglich mit F .
Beweis. Die Menge(f, a) ∈ supp(F ) × supp(M ) f (a) = b
[

=





{f } × a ∈ supp(M ) f (a) = b

f ∈supp(F )

ist als Vereinigung endlich vieler endlicher Mengen selbst endlich.
Definition 5.14. A1 , A2 und B seien Mengen, ϕ : A1 × A2 → B eine Abbildung. Gewichtete Mengen M1 ∈ M± (A1 ), M2 ∈ M± (A2 ) heißen miteinander
verträglich bezüglich ϕ, wenn für jedes b ∈ B die Menge(a1 , a2 ) ∈ supp(M1 ) × supp(M2 ) ϕ(a1 , a2 ) = b

endlich ist; dann schreibt man ϕ(A1 , A2 ) für die gewichtete Menge ∈M± (B), die durchϕ(M1 , M2 ) (b) :=X

M1 (a1 ) · M2 (a2 )(a1 ,a2 )∈A1 ×A2
ϕ(a1 ,a2 )=b

definiert ist.
Damit ist für b ∈ B
ϕ(M1 , M2 ) (b) =X

M1 (a1 ) · M2 (a2 ),(a1 ,a2 )∈supp(A1 )×supp(A2 )ϕ(a1 ,a2 )=b

wobei in diese Darstellung gerade diejenigen Summanden aus der Definition aufgenommen wurden, die von 0 verschieden sind. Hieran sieht man,daß die Verträglichkeit gemäß Definition 5.14 nötig ist, um das Definierenvon ϕ(M1 , M2 ) wie gewünscht möglich zu machen: Anschaulich gesprochen
werden in ϕ(M1 , M2 ) alle Elemente ϕ(a1 , a2 ) versammelt, die durch Anwendung von ϕ auf Paare aus Elementen a1 von M1 und a2 von M2 entstehen,wobei jedes solche Bildelement entsprechend den Vielfachheiten in M1 undin M2 berücksichtigt wird.
Bemerkung 5.15. Ist eine Multimenge M1 ∈ M(A1 ) verträglich mit einer
Multimenge M2 ∈ M(A2 ) bezüglich einer Abbildung ϕ : A1 × A2 → B, so
ist auch ϕ(M1 , M2 ) eine Multimenge (die Vielfachheiten der Elemente vonϕ(M1 , M2 ) können nicht negativ werden).

50

5Multimengen und gewichtete Mengen

Bemerkung 5.16. Die Situation von Definition 5.11 kann als Sonderfall
derjenigen in Definition 5.14 angesehen werden. Mit A1 := Abb(A, B),
A2 := A und ϕ(f, a) := f (a) für f ∈ Abb(A, B), a ∈ A ergibt sich in Definition 5.14 das gleiche wie in Definition 5.11, nämlich:• M ∈ M± (A) ist auswertungsverträglich mit F ∈ M± Abb(A, B) genau dann, wenn F und M miteinander verträglich bezüglich ϕ sind;• ist das der Fall, so gilt F (M ) = ϕ(F, M ).
Notiert man eine Abbildung A1 × A2 → B in Infixschreibweise, so kannman noch folgende Notation einführen:
Definition 5.17. A1 , A2 und B seien Mengen und• : A1 × A2 → B,
(a1 , a2 ) 7→ a1 • a2eine Abbildung. Ist M1 ∈ M± (A1 ) gegeben, so bezeichneM±M1 • (A2 )die Menge aller derjeniger gewichteter Mengen M2 ∈ M± (A2 ), für die M1
und M2 miteinander verträglich bezüglich • sind. Analog bezeichne für gegebenes M2 ∈ M± (A2 )M±•M2 (A1 )die Menge der gewichteten Mengen M1 ∈ M± (A1 ), für die M1 und M2 miteinander verträglich bezüglich • sind.
In Ergänzung zu Bemerkung 5.16 besteht auch hier ein enger Zusammenhang mit Definition 5.11: Definiert man • : Abb(A, B) × A → B durch±f • a := f (a), so ist M±
F (A) = MF • (A).
Bemerkung 5.18. Sei • : A × B → C eine Abbildung. Die auf der Menge(M, N ) ∈ M± (A) × M± (B) M ∈ M±
•N (A)= (M, N ) ∈ M± (A) × M± (B) N ∈ M±
M • (B)

definierte Abbildung (M, N ) 7→ M • N ist in beiden Parametern Z-linear:Das heißt, bei festem N ∈ M± (B) ist M±•N (A) ein Z-Modul und M 7→ M •N
ein Z-Modulhomomorphismus (es gilt nämlich(M1 + M2 ) • N = M1 • N + M2 • N
sowie(z · M ) • N = z · (M • N )±für M1 , M2 , M ∈ M±
•N (A) und z ∈ Z), und analog ist bei festem M ∈ M (A)±MM • (B) ein Z-Modul und N 7→ M • N ein Z-Modulhomomorphismus (dennM • (N1 + N2 ) = M • N1 + M • N2und
M • (z · N ) = z · (M • N )für N1 , N2 , N ∈ M±
M • (B) und z ∈ Z).

5 Multimengen und gewichtete Mengen

51

Damit gilt für Familien (Mi )i∈I , (Nj )j∈J mit endlichen Indexmengen I
und J
X



Mi • N =i∈I

XMi • N ,



X

M•

i∈I

X

Nj



=

j∈J

X

M • Nj

j∈J

und
X
i∈I

Mi •

Nj



j∈J

=

XX

Mi • N j ;i∈I j∈Jdas beweist man durch Induktion über die Anzahl der Elemente von I
bzw. J.
Bemerkung 5.19. Seien A1 , A2 und B Mengen, • : A1 × A2 → B eine±
Abbildung und M1 ∈ M±
fin (A1 ), M2 ∈ Mfin (A2 ) endliche gewichtete Mengen. Dann sind M1 und M2 miteinander verträglich bezüglich •, es gilt
M1 • M2 ∈ M ±fin (B), und es ist #(M1 • M2 ) = #(M1 ) · #(M2 ).
Nach Bemerkung 5.16 ist folgendes ein Spezialfall von Bemerkung 5.18:
Bemerkung 5.20. Die auf der Mengeno(F, M ) ∈ M± Abb(A, B) × M± (A) M ∈ M±
F (A)

definierte Abbildung (F, M ) 7→ F (M ) ist in beiden Parametern Z-linear.
Analog zu Bemerkung 5.19 gilt:
Bemerkung 5.21. Sind M ∈ M± (A) und F ∈ M± Abb(A, B) beide endlich, so ist M auswertungsverträglich
mit F . Dann ist auch F (M ) endlich,und es ist # F (M ) = #(F ) · #(M ).
Für Auswertungsverträglichkeit (und also auch allgemeiner für die Verträglichkeit wie in Bemerkung 5.19) reicht es dagegen im allgemeinennicht aus, wenn nur eine dieser gewichteten Mengen endlich ist:
Beispiel 5.22. finA sei die konstante Abbildung, die alle Elemente derMenge A auf das einzige Element der Menge {1} abbildet:
finA := (a 7→ •) : A → {•}Mit der endlichen gewichteten Menge {|finA}| auswertungsverträglich sindnach Definition 5.11 offensichtlich genau diejenigen gewichteten Mengenüber A, die selbst endlich sind – es gilt also (mit den Schreibweisen aus
Definitionen 5.4, 5.9 und 5.11)±±
M±
fin (A) = MfinA (A) = M{|finA}| (A).

Speziell mit F := {|f }| ergibt sich aus Bemerkung 5.20 folgendes:
Bemerkung 5.23. Die auf der Menge M±
f (A) definierte Abbildung M 7→
f (M ) ist Z-linear.

6

Gefärbte Netze

Als ein gefärbtes Netz bezeichnen wir eine Strukturbeschreibung, die Mengen von Stellen und Transitionen, zu jeder Stelle eine Farbmenge, zu jeder
Transition eine Menge von Schaltmodi sowie zu jedem geordneten Paaraus einer Stelle und einer Transition oder umgekehrt eine Multimenge
von Kanten vorgibt (Abschnitt 6.1). In einer solchen Beschreibung nicht
enthalten sind dagegen Anfangsmarkierungen sowie die Schaltregeln, dievorgeben, welche der bei einem gefärbten Netz denkbaren Schritte konkret erlaubt werden sollen. Diese beiden Konzepte werden bei der Definition des Verhaltens eines gefärbten Netzes eingeführt (Abschnitt 6.2).
Wir verzichten entgegen den üblichen Definitionen so weit wie möglich auf
Endlichkeitsforderungen: Nicht nur die Farbmengen und die Mengen der
Schaltmodi dürfen unendlich sein, sondern auch die Mengen der Stellen
und Transitionen sowie die Kanten-Multimengen; wir lassen unendlicheMarkierungen zu und Schaltvorgänge mit unendlicher Nebenläufigkeit (esdürfen also nicht nur endlich viele Transitionen in endlich vielen Schaltmodi zur Zeit schalten). Dabei spielen die im vorangegangenen Abschnitt 5 behandelten Verträglichkeitsbegriffe für den Umgang mit gewichteten Mengen eine wichtige Rolle.

6.1

Struktur

Definition 6.1. Ein gefärbtes Netz ist ein Tupel

CN = P, T, (Cp )p∈P , (Dt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P) ,wobei folgendes gilt:(i) P und T sind disjunkte Mengen. Die Elemente von P heißen Stellen(places) von CN , die Elemente von T heißen Transitionen von CN .
(ii) Für jedes p ∈ P ist Cp eine Menge, die Farbmenge der Stelle p. Die
Elemente von Cp heißen Farben (colours).
(iii) Für jedes t ∈ T ist Dt eine Menge, die Menge der Schaltmodi derTransition t.
(iv) Für jedes p ∈ P und jedes t ∈ T gilt Fp,t , Ft,p ∈ M Abb(Dt , Cp ) . Die
Elemente der Multimengen Fp,t und Ft,p heißen Kanten (arcs) von pnach t bzw. von t nach p.
Der Buchstabe »F « bei Fp,t und Ft,p steht dafür, daß diese Multimengen
einen gewissen Fluß (flow) symbolisieren.
In anderen Definitionen wird die Bezeichnung »Kante« für Elementevon (P × T) ∪ (T × P) verwendet, zu denen dann eine Kantenbeschriftung(entsprechend unseren Fp,t und Ft,p ) Näheres aussagt. – Eine Verallgemeinerung der hier gegebenen
Definition ergäbe sich, wenn
Fp,t und Ft,p statt
aus M Abb(Dt , Cp ) aus der Menge Abb Dt , M(Cp ) gewählt werden dürften (»flexible Kanten«, [18]).
52

6 Gefärbte Netze

53

In graphischen Darstellungen werden Stellen als Kreise (allgemeiner:
Ellipsen) und Transitionen als Quadrate (Rechtecke) wiedergegeben. Pfeile können für »Mehrfachkanten« stehen (d. h. für eine Multimenge Fp,t oderFt,p , die dann als Pfeilbeschriftung angegeben wird) oder auch für einzelne
Kanten (z. B. kann, wenn Fp,t oder Ft,p die Form {|x|} hat, ein mit x beschrifteter Pfeil verwendet werden).
Beispiel 6.2. Sei G = Z n Z mit einem n ∈ Z\{0} (G = Z im Fall n = 0).
Das durchCN := CN G := P, T, (Cp )p∈P , (Dt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P)

mit
P := {p}, T := {t1 , t2 },Cp := Dt1 := Dt2 := G,
Fp,t1 := ∅Abb(G,G) ,

Ft1 ,p := (x 7→ x), (x 7→ x + 1)Fp,t2 := (x 7→ x), (x 7→ x + 1)



∈ M Abb(G, G) ,

∈ M Abb(G, G) ,Ft2 ,p := ∅Abb(G,G)
definierte gefärbte Netz kann wie folgt dargestellt werden:p#t1{|(x7→x),(x7→x+1)|}

t2{|(x7→x),(x7→x+1)|}

-

G

-

"!

G

G

54

6.2

6

Gefärbte Netze

Verhalten

Definition 6.3. Eine Markierung
eines gefärbten Netzes CN = P, T,
(Cp )P , (Dt )T , (Fx,y )(P×T)∪(T×P) ist eine Familie m = (mp )p∈P von Multimengen mp ∈ M(Cp ). Die Menge aller Markierungen von CN wird mit MCN
bezeichnet.
Die Elemente der Multimengen mp bezeichnet man als Marken undsagt, daß diese Marken auf der Stelle p liegen.
Zur Beschreibung des möglichen Verhaltens eines gefärbten Netzes CN
dienen uns Transitionsysteme (MCN , E, Trans E ) (d. h. Tupel bestehend
aus der Zustandsmenge MCN , einer Ereignismenge E und einer Zustandsübergangsrelation Trans E ⊆ MCN × E × MCN [28]) mit der Eigenschaft, daß aus (m, e, m0 ) ∈ Trans E ∧ (m, e, m00 ) ∈ Trans E folgt, daß m0 = m00
ist: Falls eine vom Ereignis e bewirkte Nachfolgemarkierung m0 von mexistiert, so ist diese eindeutig bestimmt.
(Es ist zu beachten, daß der Begriff »Transition« in zwei verschiedenen
Bedeutungen auftritt. Als Wortbestandteil von »Transitionssystem« steht
er für den Übergang zwischen zwei Zuständen; eine Transition im Sinne
der Definition 6.1 dagegen ist ein Element t ∈ T.)
Die Definition der Zustandsübergangsrelation Trans E erhalten wir ausgehend von der Menge T der Transitionen, der Familie (Dt )t∈T der Schaltmodi und der Familie (Fx,y )(x,y)∈(P×T)∪(T×P) der Kantenmultimengen. Die
Grundidee ist, daß eine Transition t ∈ T in einem Schaltmodus d ∈ Dt
aus jeder Stelle p ∈ P nach Maßgabe von (Fp,t )({|d|}) gewisse Elemente derMultimenge mp verbraucht und anschließend in jede Stelle nach Maßgabe
von (Ft,p )({|d|}) neue Elemente hinzufügt (wobei die Auswertungsverträglichkeit von {|d|} mit den Fp,t und Ft,p gefordert werden muß, damit die Multimengen (Fp,t )({|d|}), (Ft,p )({|d|}) ∈ M(Cp ) definiert sind): t »schaltet« imModus d. Unsere Definition der Zustandsübergangsrelation Trans E wird
darüberhinaus möglich machen, mehrere (nicht notwendig endlich viele)
Schaltvorgänge gleichzeitig zuzulassen.
Für die Ereignismenge E werden wir keine genau Festlegung treffen,
sondern eine Menge ECN angeben, für die dann E ⊆ ECN beliebig gewählt
werden kann (bestimmte Sonderfälle für diese Wahl von E werden später
in diesem Abschnitt vorgestellt). Solche Teilmengen E nennen wir Schaltregeln, denn sie geben an, welche Schritte erlaubt sind und welche nicht.
(In der Literatur ist eine andere Bedeutung des Wortes »Schaltregel« im
Gebrauch, die sich auf das Betrachten von Folgen von Ereignissen bezieht;
z. B. »faire Schaltregel«, siehe [16].)
Definition 6.4. Ein Prä-Schritt
eines gefärbten Netzes CN = P, T,
(Cp )P , (Dt )T , (Fx,y )(P×T)∪(T×P) ist eine Familie e = (et )t∈T von Multimengen et ∈ M(Dt ), so daß für jedes t ∈ T und jedes p ∈ P die Multimenge et
mit den Multimengen Fp,t und Ft,p auswertungsverträglich (Definition 5.11)
ist.


Damit sind also für alle t ∈ T, p ∈ P durch Fp,t , Ft,p ∈ M Abb(Dt , Cp )und et ∈ M(Dt ) Multimengen Fp,t (et ), Ft,p (et ) ∈ M(Cp ) gegeben.

6 Gefärbte Netze

55

Definition 6.5. Ein Prä-Schritt e =(et )t∈T eines gefärbten Netzes CN =
P, T, (Cp )P , (Dt )T , (Fx,y )(P×T)∪(T×P)
ist ein Schritt, wenn fürjedes p ∈ Psowohl die Familie Fp,t (et ) t∈T als auch die Familie Ft,p (et ) t∈T addierbar(Definition 5.7) ist. Die Menge aller Schritte von CN heißt ECN .
Bemerkung 6.6. Sei e(et )t∈T ∈ ECN ein beliebiger Schritt von CN undte ∈ T. Dann ist auch e0 := (e0t )t∈T mit ee0t := eet und e0t := ∅Dt für alle t ∈ T\teein Schritt, also e0 ∈ ECN .
Sei m = (mp )p∈P eine Markierung und e = (et )t∈T ein Schritt eines
gefärbten Netzes CN . Der Schritt e heißt aktiviert in der Markierung m,wenn für alle p ∈ PX
mp ≥Fp,t (et )t∈Tgilt. Dann ist die durch e bewirkte Nachfolgemarkierung m0 von m gegeben
als m0 := (m0p )p∈P mit
m0p := mp −X

Fp,t (et ) +t∈TXFt,p (et ).

t∈T

Die Aktivierungsbedingung impliziert, daß die gewichteten Mengen m0p ∈M± (Cp ) nichtnegativ sind, also Multimengen: m0p ∈ M(Cp ).
Sei eine Schaltregel E ⊆ ECN gegeben. Um wie gewünscht ein Transitionssystem (MCN , E, Trans E ) zu erhalten, definieren wir Trans E ⊆ MCN ×
E × MCN entsprechend den gerade vorgestellten Konzepten wie folgt:
Definition 6.7. Für m, m0 ∈ MCN und e ∈ E mit m = (mp )p∈P , m0 =(m0p )p∈P , e = (et )t∈T gilt
(m, e, m0 ) ∈ Trans E :⇐⇒ ∀ p ∈ P :

h

mp ≥

X

Fp,t (et )t∈T∧ m0p = mp −X

Fp,t (et ) +

t∈T

X

i

Ft,p (et ) .

t∈Te

Für (m, e, m0 ) ∈ Trans E schreibt man auch m −→E m0 .
Geht es in erster Linie nur um die Zustände und ihre Übergänge, abernicht darum, durch welche Ereignisse diese verursacht werden, so kannman statt Trans E die Relation →E ⊆ MCN × MCN verwenden, die wie folgt
definiert ist:
Definition 6.8. Für m, m0 ∈ MCN gilt
m →E m0:⇔e0→E m .
∃e ∈ E: m −(MCN , →E ) ist ein gerichteter Graph mit der Knotenmenge MCN und
der Kantenmenge →E . Der reflexive und transitive Abschluß von →E wird∗mit −→E bezeichnet:

56

6

Definition 6.9. Es ist

∗

[

−
→E :=

Gefärbte Netze

→E n

n∈N

(mit →E

0 = {(m, m) | m ∈ MCN }).

Definition 6.10. Für eine Markierung m ∈ MCN heißt m0 ∈ MCN von m∗aus erreichbar, wenn m −→E m0 gilt. Die Menge aller von m aus erreichbaren Markierungen bezeichnet man mit [miE , es wird also definiert∗[miE := {m0 ∈ MCN | m −→E m0 }.
Für M ⊆ MCN setzt man[[M iE :=

[miE .

m∈M

Neben der Möglichkeit, alle Schritte des gefärbten Netzes als Ereignisse zuzulassen (E = ECN ), sind die folgenden beiden Möglichkeiten für die
Festlegung von E erwähnenswert:
l-fin (siehe nachfolgende Definition 6.11), die Menge aller lokal• E = ECN
endlich agierenden Schritte (von jedem Schritt sind an jeder Stelle nur endlich viele Marken betroffen).
fin (siehe nachfolgende Definition 6.11), die Menge aller end• E = ECN
lich agierenden Schritte (bei jedem Schritt sind nur endlich viele
Stellen und an jeder Stelle nur endlich viele Marken betroffen).
l-fin , E fin ⊆ E
Definition 6.11. ECN
CN sind gegeben durch:
CN



l-fin
:= (et )t∈T ∈ ECN
ECN∀ p ∈ P:hX

Fp,t (et ) und

t∈T

fin
ECN
:=



l-fin
(et )t∈T ∈ ECN

n

p∈P

X

i

Ft,p (et ) sind endlicht∈TX

Fp,t (et ) 6= ∅Cp ∨t∈T

X

Ft,p (et ) 6= ∅Cp

o

t∈T



ist endlich

l-fin = E fin .
Wenn P eine endliche Menge ist, gilt zwangsläufig ECN
CN
fin ist oft die einzige Schaltregel, die für gefärbte Netze überhaupt beECN
trachtet wird; oder es werden daraus sogar nur Elementarschritte zugelassen, d. h. Schritte (et )t∈T , bei denen genau ein te ∈ T existiert mit #(eet ) = 1,
wobei alle anderen et leer sind.

6 Gefärbte Netze

6.3

57

Invarianten

Für die durch eine Schaltregel E ⊆ ECN festgelegte Relation →E kannman Fragen der Erreichbarkeit betrachten und gewisse invariante Eigenschaften anzugeben versuchen. Ein Tupel (CN , m0 ) aus einem gefärbten
Netz CN und einer Markierung m0 ∈ MCN (der Anfangsmarkierung)bezeichnet man als gefärbtes Netzsystem. Oft will man für ein gefärbtes Netz CN nicht beliebige Markierungen aus MCN zulassen, sondern es
wird eine Menge M0 ⊆ MCN von erlaubten Anfangsmarkierungenvorgegeben. Das Tupel (CN , M0 ) bestimmt dann die Menge (CN , m0 ) | m0 ∈ M0
von gefärbten Netzsystemen (»die (CN , M0 )-Netzsysteme«). Unter diesen
Gegebenheiten kann man den Begriff der Invarianten sehr allgemein wie
folgt formalisieren:
Definition 6.12. Sei CN ein gefärbtes Netz, M0 ⊆ MCN und E ⊆ ECN .
Eine Invariante der (CN , M0 )-Netzsysteme bezüglich E ist ein Tupel(I, I, Mind ) aus einer Menge I, einer Abbildung I : MCN → I und einer
Menge Mind ⊆ MCN , so daß folgende Bedingungen erfüllt sind:(i) M0 ⊆ Mind(ii) Ist m ∈ Mind und m0 ∈ MCN mit m →E m0 , so gilt m0 ∈ Mind undI(m) = I(m0 ).
Hat man eine Invariante (I, I, Mind ) gemäß dieser Definition, so wird auchdie Abbildung I als Invariante bezeichnet; Mind ist ihr Induktionsbereich.
Aus den Bedingungen der Definition 6.12 folgt: [M0 iE ⊆ Mind (alle erreichbaren Zustände sind demnach in Mind enthalten), und I ist für jedesm ∈ Mind (insbesondere also für jedes m ∈ M0 ) auf der Menge [miE konstant; das heißt ∀ m0 ∈ [miE : I(m0 ) = I(m). Damit können Invarianten
Aussagen über Nichterreichbarkeit von Zuständen machen:
Bemerkung 6.13. Sei (I, I, Mind ) eine Invariante eines gefärbten Netzes
CN bezüglich einer Schaltregel E ⊆ ECN . Seien m1 , m2 ∈ MCN . Es gelte
I(m1 ) 6= I(m2 ). Dann existiert kein m ∈ Mind mit m1 ∈ [miE ∧ m2 ∈ [miE .
Insbesondere gilt, falls m1 ∈ Mind ist, m2 6∈ [m1 iE und entsprechend, falls
m2 ∈ Mind ist, m1 6∈ [m2 iE .
Beweis. Sei m ∈ Mind mit m1 ∈ [miE und m2 ∈ [miE . Nach Definition von[miE gibt es n1 , n2 ∈ N mit m1 →E n1 m und m2 →E n2 m. Durch Induktionüber n1 bzw. n2 folgt I(m1 ) = I(m) = I(m2 ) im Widerspruch zu I(m1 ) 6=I(m2 ).
Bemerkung 6.14. Sei CN ein gefärbtes Netz, M0 ⊆ MCN und seien
E1 , E2 ⊆ ECN Schaltregeln mit E2 ⊆ E1 . Ist ein Tupel (I, I, Mind ) eine
Invariante bezüglich E1 , so ist es auch eine Invariante bezüglich E2 .
Beweis. Nur die Bedingung (ii) der Definition 6.12 muß überprüft werden.
Da sie für E1 erfüllt ist, ist sie das auch für E2 ; denn mit m →E2 m0 gilt
stets auch m →E1 m0 .

58

6

Gefärbte Netze

In der Literatur (so zum Beispiel [17]) versteht man unter Invarianteneines Transitionssystems häufig Prädikate auf der Menge der Zustände(in diesem Fall also Abbildungen p : MCN → {wahr, falsch}), die gewisse Eigenschaften erfüllen. Genauer unterscheidet man zwischen »Invarianten«
schlechthin und »induktiven Invarianten« – bei ersteren kommt es nur auf
erreichbare Zustände an, bei letzteren dagegen auf alle Zustände:• Von einer »Invarianten« verlangt man lediglich, daß das Prädikat injedem erreichbaren Zustand wahr ist (∀ m ∈ [M0 iE : p(m) = wahr). In
anderer Literatur (siehe etwa [9]) werden derartige Prädikate auchals »always-true« bezeichnet.
Mit Invarianten im Sinne der Definition 6.12 steht dieses Konzept
wie folgt in Beziehung: Ein Prädikat p ist genau dann eine Invariante(»always-true«), wenn das Tupel{wahr, falsch}, p, [M0 iEeine Invariante gemäß Definition 6.12 ist und∀ m0 ∈ M0 : p(m0 ) = wahr
gilt.
• Bei einer induktiven Invarianten (in [9] einfach als »invariant« bezeichnet) wird gefordert, daß sie in den Anfangszuständen wahr ist(∀ m0 ∈ M0 : p(m0 ) = wahr) und bei beliebigen Zustandsübergängen
m →E m0 (m, m0 ∈ MCN ) im Fall p(m) = wahr auch p(m0 ) = wahr
gilt. (Jede induktive Invariante ist damit auch eine Invariante; die
Umkehrung gilt aber nicht, weil nur bei den induktiven Invarianten
auch die nicht erreichbaren Zustände eine Rolle spielen.)
Ein Prädikat p ist genau dann eine induktive Invariante, wenn{wahr, falsch}, p, p−1 (wahr)eine Invariante nach Definition 6.12 ist. (Die Forderung an induktive
Invarianten, daß ∀ m0 ∈ M0 : p(m0 ) = wahr gelten soll, ist von Definition 6.12 ausgehend deshalb erfüllt, weil die dortige Bedingung (i)dann besagt, daß M0 ⊆ p−1 (wahr) ist.)
Ein gegenüber Definition 6.12 etwas anderer Ansatz für die Klärung
des Begriffs »Invariante« sieht wie folgt aus:
Definition 6.15. Sei CN ein gefärbtes Netz, M0 ⊆ MCN und E ⊆ ECN . Als
Invariante der (CN , M0 )-Netzsysteme bezüglich E bezeichnet man auchein Tupel (∼, Mind ) aus einer Äquivalenzrelation ∼ ⊆ MCN ×MCN und einer
Menge Mind ⊆ MCN , das folgende Bedingungen erfüllt:(i) M0 ⊆ Mind(ii) Ist m ∈ Mind und m0 ∈ MCN mit m →E m0 , so gilt m0 ∈ Mind undm ∼ m0 .

6 Gefärbte Netze

59

Hat man eine Invariante (∼, Mind ) gemäß dieser Definition, so wird auchdie Äquivalenzrelation ∼ als Invariante bezeichnet; Mind ist ihr Induktionsbereich.
Wie diese beiden Auffassungen von Invarianten zueinander in Beziehung stehen, zeigen die folgenden Bemerkungen:
Bemerkung 6.16. Sei CN ein gefärbtes Netz, M0 ⊆ MCN und E ⊆ ECN .
Sei (I, I, Mind ) eine Invariante gemäß Definition 6.12. Nun wird die Relation ∼I ⊆ MCN × MCN definiert durchm ∼I m0:⇔

I(m) = I(m0 )für m, m0 ∈ MCN . Dann ist ∼I eine Äquivalenzrelation, und (∼I , Mind ) ist
eine Invariante gemäß Definition 6.15.
Bemerkung 6.17. Sei CN ein gefärbtes Netz, M0 ⊆ MCN und E ⊆ ECN .
Sei (∼, Mind ) eine Invariante gemäß Definition 6.15. Nun sei
I∼ := MCN ∼

die Menge der Äquivalenzklassen, und die AbbildungI∼ : MCN → I∼
sei definiert durch die Forderungm ∈ I∼ (m)für alle m ∈ MCN , das heißtI∼ (m) = {m0 ∈ MCN | m ∼ m0 }.
Dann ist (I∼ , I∼ , Mind ) ist eine Invariante gemäß Definition 6.12.
Bemerkung 6.18. Ausgehend von einer Invarianten (∼, Mind ) gemäß Definition 6.15 ergibt sich mit den Definitionen aus Bemerkung 6.17 eine AbbildungI∼ : MCN → I∼
und hieraus mit der Definition aus Bemerkung 6.16 eine Äquivalenzrelation∼I∼ ⊆ MCN × MCN .
Wie man leicht sieht, gilt dabei ∼I∼ = ∼, das heißt, man erhält wieder die
ursprüngliche Äquivalenzrelation zurück. In einem gewissen Sinne sinddie beiden Definitionen von Invarianten also gleichwertig, der wesentliche
Unterschied liegt nur im Vorhandensein der Menge I in Definition 6.12.
Bei der Interpretation der später in Abschnitt 8 definierten linearen Invarianten hat man als Induktionsbereich die gesamte Menge MCN (siehe
Definition 8.16 und Corollar 8.21). (Die ausgezeichnete Menge M0 der Anfangsmarkierungen spielt damit keine besondere Rolle mehr.) Für diesen
Fall Mind = MCN lassen sich Invarianten – dargestellt durch Äquivalenzrelationen, d. h. gemäß Definition 6.15 – auch wie folgt charakterisieren:60

6

Gefärbte Netze

Bemerkung 6.19. Eine Äquivalenzrelation ∼ ⊆ MCN × MCN ist genau
dann eine Invariante der (CN , M0 )-Netzsysteme bezüglich der Schaltregel
E ⊆ ECN mit dem Induktionsbereich MCN , wenn gilt
∼E ⊆ ∼,
wobei ∼E die durch →E induzierte Äquivalenzrelation bezeichnet, also den
reflexiven und transitiven Abschluß von →E ∪ →E −1 :∼E := →E ∪ →E −1

∗

=

[

→E ∪ →E −1

n∈N

n

Diese Charaktisierung macht deutlich, daß bei den Invarianten mit
Mind = MCN keine Bedeutung hat, daß (MCN , →E ) ein gerichteter Graphist: Die Richtung des »Zeitpfeils« geht bei dieser Betrachtungsweise verloren.
Beispiel 6.20. Wir betrachten für G = Z n Z mit n ∈ Z das gefärbte Netz CN = CN G aus Beispiel 6.2. Dabei kann man, um einfachere Schreibweisen zu ermöglichen, MCN mit M(Cp ) = M(G) identifizieren, denn es gibt nur eine einzige Stelle; ähnlich kann man auch ECN
mit M(Dt1 ) × M(Dt2 ) = M(G) × M(G) identifizieren. Für die Fälle, daß
G = Z n Z mit einer geraden Zahl n ∈ Z ist, ist jedes Element von G entweder gerade oder ungerade. (Bei ungeradem n ist eine solche Aufteilung
nicht sinnvoll möglich.) Dann kann man eine Relation∼ ⊆ MCN × MCN
definieren mit m ∼ m0 genau dann, wenn die gewichtete Menge m0 − m
gleichviele gerade wie ungerade Elemente enthält – das heißt genauer:m ∼ m0:⇔

Die gewichtete Menge m0 − m ist endlich,und es giltX

(m0 − m)(g) =g∈Gg geradeX(m0 − m)(g).

g∈Gg ungerade

Diese Relation ∼ ist eine Äquivalenzrelation, wie man leicht sieht. Mankann bei G = Z n Z mit einem geraden n ∈ Z\{0} aufgrund der Zustandsübergangsrelationen →E zu beliebigen E ⊆ ECN vermuten, daß ∼ im Sinne von Definition 6.15 eine Invariante der (CN , MCN )-Netzsysteme bezüglich E mit Induktionsbereich MCN ist; wir werden dies später auf algebraischem Wege beweisen. Im Fall G = Z mit E = ECN dagegen ist ∼ offenbar
keine Invariante; man betrachte dann nämlich die Schaltfolge(χ{2n|n∈N} ,∅Z )(∅Z ,χ{2n+1|n∈N} )m := ∅Z −−−−−−−−−→ χN −−−−−−−−−−→ {|0|} =: m0 ,bei der im ersten Schritt die Transition t1 für jede gerade natürliche Zahl
einmal schaltet und im zweiten Schritt die Transition t2 für jede ungerade6 Gefärbte Netze

61

natürliche Zahl einmal schaltet. m0 −m ist endlich und hat nur ein einziges
Element, so daß m 6∼ m0 gelten muß. (Man sieht hieran auch, daß man ∼bei der gewünschten Bedeutung nicht für solche Paare (m, m0 ), für die die
Differenz m0 − m unendlich ist, so umdefinieren kann, daß ∼ doch noch zu
einer Invarianten mit den gewünschten Eigenschaften würde.)Wie dieses Beispiel zeigt, können verschiedene, aber ähnliche gefärbte
Netze Invarianten haben, die trotz der Unterschiede der Netze im wesentlichen gleich sind. Um die Eigenschaften der Farbmengen, der Schaltmodi
und der Kanten vom konkreten gefärbten Netz abstrahierend behandelnzu können, werden wir die Methoden der algebraischen Spezifikation verwenden.

7

Algebraische Netze

Als »algebraisches Netz« bezeichnen wir eine Beschreibung, die mittels
der im Abschnitt 2 vorgestellten Methoden der algebraischen Spezifikation ein »Skelett« für Netze festlegt. Zusammen mit zum Netz passenden
Algebren entstehen hieraus konkrete gefärbte Netze, wie sie im vorangegangenen Abschnitt 6 definiert wurden; diese werden als Interpretationen des algebraischen Netzes bezeichnet. (Entsprechend könnte man auch
Netzsysteme betrachten, bei denen zusätzlich Anfangsmarkierungen algebraisch anzugeben wären.) Das Verhalten der gefärbten Netze, d. h. die
zugehörigen Transitionssysteme (Definition 6.7), hängt außerdem von dergewünschten Schaltregel ab. Bereits am algebraischen Netz lassen sich jedoch manche Eigenschaften feststellen, die für jede Interpretation des algebraischen Netzes Gültigkeit haben; ein Beispiel hierfür bietet der folgende Abschnitt 8 über lineare Invarianten.
Definition 7.1. Ein algebraisches Netz ist ein Tupel
AN = P, T, (S, Ω, Ξ, G, T fin ), (sp )p∈P , (Xt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P) ,

wobei folgendes gilt:(i) P und T sind disjunkte Mengen. Die Elemente von P heißen Stellen(places) von AN , die Elemente von T heißen Transitionen von AN .
(ii) (S, Ω, Ξ, G, T fin ) ist eine Endlichkeitsspezifikation (Definition 4.2).
(iii) Für jedes p ∈ P ist sp ∈ S.
(iv) Für jedes t ∈ T ist Xt ⊆ Ξ ein Variablensystem bezüglich (S, Ω).
(v) Für jedes p ∈ P und jedes t ∈ T gilt Fp,t , Ft,p ∈ M TΩ,sp (Xt ) .
Geht man von einer Gleichungsspezifikation aus und nicht von einer
Endlichkeitsspezifikation, so kann man nach Bemerkung 4.4 trotzdem ein
algebraisches Netz gemäß obiger Definition erhalten, da eine der Gleichungsspezifikation gleichwertige Endlichkeitsspezifikation existiert.
Graphische Darstellungen von algebraischen Netzen erfolgen analog
wie bei gefärbten Netzen; siehe Seite 52 und das später folgende Beispiel 7.3.
Definition 7.2. Es sei
AN = P, T, (S, Ω, Ξ, G, T fin ), (sp )P , (Xt )T , (Fx,y )(P×T)∪(T×P)



ein algebraisches Netz. Dabei sei Xt = (Xt,s )s∈S für t ∈ T die Darstellungdes jeweiligen Variablensystems als Familie. Weiter sei
A = (As )s∈S , (fω )ω∈Ω



ein Modell von (S, Ω, Ξ, G, T fin ) (Definition 4.3). Für t ∈ T sei nun

Bt := α = (αs )s∈S ∀ s ∈ S : αs ∈ Abb(Xt,s , As )62

7 Algebraische Netze

63

die Menge aller Belegungen (Definition 1.17) von Xt . Damit hat man gemäß
Definition 1.22 für jedes p ∈ P und jedes t ∈ T eine AbbildunginterpretA : TΩ,sp (Xt ) → Abb(Bt , Asp ).
(Die Bezeichnung interpretA benutzen wir dabei, ohne darin das jeweils zugrundeliegende Variablensystem und die jeweilige »Zielsorte« ausdrücklichzu erwähnen, denn diese sind immer aus dem Zusammenhang zu erkennen.)Gemäß Definition 5.9 hat man damit auch Abbildungen±interpretA : M±
interpretA TΩ,sp (Xt ) → M Abb(Bt , Asp )

für die entsprechenden mit interpretA auswertungsverträglichen gewichteten Mengen. Sind sowohl alle Fp,t als auch alle Ft,p mit den jeweiligen Ab
bildungen auswertungsverträglich (d. h. Tp,t , Tt,p ∈ M±
interpretA TΩ,sp (Xt ) ),so heißt AN interpretierbar durch A. Die Interpretation von AN durch
A ist dann das gefärbte Netz (Definition 6.1)
P, T, (Asp )p∈P , (Bt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P)



mit
Fp,t := interpretA (Fp,t ),Ft,p := interpretA (Ft,p )für p ∈ P, t ∈ T.
(Zu einem beliebig vorgegebenen gefärbten Netz CN gibt es immer ein
algebraisches Netz AN , von dem CN eine Interpretation ist: Jede Farbmenge und jede Menge von Schaltmodi kann durch eine Sorte beschrieben werden, die zu jedem Element der jeweiligen Menge ein eigenes Konstantensymbol besitzt; jede in einer Kante vorkommende Abbildung von einem Dt
in ein Cp kann durch ein eigenes Operationssymbol vertreten werden.)Beispiel 7.3. Sei die Endlichkeitsspezifikation SPECF 1 := SPECF =(S, Ω, Ξ, G, T fin ) wie in Beispiel 4.8 definiert und sei
AN 1 := P, T, SPECF 1 , (sp )p∈P , (Xt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P)
das algebraische Netz mit
P := {p}, T := {t1 , t2 },sp := s1 ,Xt1 := Xt2 := {x1 },Fp,t1 := ∅TΩ,s1 ({x1 }) ,

Ft1 ,p := x1 , x1 +1 11 ,
Fp,t2 := x1 , x1 +1 11 ,Ft2 ,p := ∅TΩ,s1 ({x1 }) .

64

7 Algebraische Netze

SPECF 2 := SPEC SPECF sei die gemäß Bemerkung 4.4 aus der Gleichungsspezifikation SPEC := (S, Ω, Ξ, G) (vgl. Beispiel 2.21) gewonnene Endlichkeitsspezifikation und
AN 2 := P, T, SPECF 2 , (sp )p∈P , (Xt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P)



ein ansonsten AN 1 gleichendes algebraisches Netz.
Beide Netze können wie folgt dargestellt werden:p#t1{|x1 ,x1 +1 11}|t2{|x1 ,x1 +1 11}|

-

{x1 }

-

"!

s1

{x1 }


In Beispiel 6.2 hatten wir in Abhängigkeit von einer Menge G = Z n Z mitn ∈ Z ein gefärbtes Netz CN G definiert. Jenes Netz CN G läßt sich gegebenenfalls als Interpretation des algebraischen Netzes AN 1 und in jedem
Fall als Interpretation des algebraischen Netzes AN 2 auffassen, indem wir
auf die in Beispiel 2.21 angegebenen Algebren zurückgreifen:• Bei AN 2 schreibt die Endlichkeitsspezifikation keinerlei Endlichkeitsterme vor, und also kommen zunächst alle in Beispiel 2.21 genannten SPEC -Algebren A = (As )s∈S , (fω )ω∈Ω in Frage. In jedem
Fall ist AN 2 durch A interpretierbar, und bei n1 = n ist As1 =Z
n1 Z = G; gilt darüberhinaus f11 = 1 + n1 Z, so ist die Interpretation von AN 2 durch A gerade CN G .
• Bei AN 1 stellt der hinzukommende Endlichkeitsterm strengere Anforderungen an die Algebren. Zum für AN 2 Gesagten kommt hinzu,
daß n nicht 0 sein darf – bei n = n1 6= 0 ist CN G die Interpretation
von AN 1 durch die SPECF 1 -Algebra A, bei n = n1 = 0 dagegen ist A
gar keine SPECF 1 -Algebra, so daß AN 1 nicht durch A interpretierbar
sein kann.

8 Lineare Invarianten
Den Begriff »lineare Invariante« verwenden wir für ein Analogon der»S-Invarianten«, wie sie schon lange von Stellen-Transitions-Netzen her
bekannt sind ([20], [21]). Der hier verwendete Ansatz zur Definition linearer Invarianten algebraischer Petrinetze lehnt sich an [31] an. Da jedochin der vorliegenden Arbeit die Definitionen für Petrinetze durch das weitestmögliche Zulassen von Unendlichkeit allgemeiner sind, wird die Behandlung linearer Invarianten aufwendiger; dabei zeigt sich, warum wir
in der Definition algebraischer Petrinetze statt der üblichen Gleichungsspezifikationen die in Abschnitt 4 behandelten Endlichkeitsspezifikationen
zugrundegelegt haben.
Bei Stellen-Transitions-Netzen kann auf jeder Stelle nur eine Anzahl
ununterscheidbarer Marken liegen. Deshalb lassen sich die Veränderungen der Markierung, die beim Schalten von Transitionen möglich sind,durch eine Inzidenzmatrix mit ganzzahligen Komponenten darstellen. Eine S-Invariante ist dabei ein durch die Stellenmenge indizierter Vektorvon Zahlen [20]. Bei gefärbten Netzen dagegen können die Marken auf
einer Stelle voneinander verschieden sein. Die Inzidenzmatrix zu einem
gefärbten Netz enthält deshalb nicht ganze Zahlen, sondern (bei unseren
Netzen ohne flexible Kanten) gewichtete Mengen von Abbildungen, um dieverschiedenen Schaltmodi der Transitionen berücksichtigen zu können. Eine S-Invariante zu einem gefärbten Netz ist ein durch die Stellenmenge
indizierter Vektor, dessen Komponenten ebenfalls gewichtete Mengen vonAbbildungen sind.
Beim abstrahierenden Schritt von gefärbten zu algebraischen Netzen
treten an die Stelle der Abbildungen, deren Definitions- und Wertebereiche
erst durch konkrete Algebren festgelegt wären, geeignete Substitutionen.
Auf der abstrakten Ebene der Terme können mit Hilfe dieser Substitutionen Beobachtungen gemacht werden, die in jeder Algebra (in jeder Interpretation) durch Trägermengen, Konstanten und Operationen konkrete
Entsprechungen erhalten. Wir behandeln in Abschnitt 8.1 zunächst die abstrakte Ebene und definieren anhand der Termsicht, was eine lineare Invariante eines algebraischen Petrinetzes ist. Abschnitt 8.2 zeigt, welche konkrete Bedeutung solche Invarianten in den Interpretationen haben. Der
Zweck einiger Details der abstrakten Definitionen wird erst dann deutlich,wenn schließlich in Satz 8.20 die konkrete Invarianzeigenschaft zu einer
algebraisch dargestellten linearen Invarianten bewiesen wird.
Wir behandeln durchgängig nur die allgemeinste Schaltregel E = ECN ;laut Bemerkung 6.14 sind unsere Resultate zu Invarianten damit für beliebige Schaltregeln gültig. Für eingeschränkte Schaltregeln nur mit lokall-fin ) oder nur mit endlich agierenden
endlich agierenden Schritten (E ⊆ ECN
fin
Schritten (E ⊆ ECN ) sind lineare Invarianten einfacher handzuhaben, insbesondere sind Endlichkeitsspezifikationen dann entbehrlich. Diese Fälle
sind in [26] abgehandelt und werden hier nicht wiederholt, da in dieser Arbeit die Benutzung von Endlichkeitsspezifikationen im Vordergrund steht.
65

66

8.1

8 Lineare Invarianten

Algebraische Sicht

Definition 8.1. Sei
AN = P, T, (S, Ω, Ξ, G, T fin ), (sp )P , (Xt )T , (Fx,y )(P×T)∪(T×P)



ein algebraisches Netz (Σ := (S, Ω), SPEC := (S, Ω, Ξ, G), SPECF :=(S, Ω, Ξ, G, T fin )). Die algebraische Inzidenzmatrix (kurz: die Inzidenzmatrix) von AN ist definiert als
D := (Dp,t )(p,t)∈P×T
mit
Dp,t := −Fp,t + Ft,p ∈ M± TΩ,sp (Xt )

für p ∈ P, t ∈ T.
Die Zeilen der Matrix D werden durch P, die Spalten durch T indiziert.
Die Matrix D kann unendlich viele Zeilen und unendlich viele Spalten haben.
Bei S-Invarianten von Stellen-Transitions-Netzen spielt das Matrixprodukt aus einem P-indizierten Zeilenvektor, einer Gewichtung, mit der Inzidenzmatrix des jeweiligen Netzes eine wichtige Rolle. Analog dazu will
man auch bei algebraischen Netzen ein Matrixprodukt von geeigneten
P-indizierten Zeilenvektoren mit der P × T-Matrix D berechnen können.
Ein solches Produkt ist ein T-indizierter Zeilenvektor; seine Komponenten sind allgemein Elemente von abelschen Gruppen. Wie bei gewöhnlichen S-Invarianten kann eine Gewichtung nur dann eine lineare Invariante sein, wenn das Produkt aus der Gewichtung und der Inzidenzmatrix
den Nullvektor ergibt.
Diese Forderung reicht jedoch anders als bei herkömmlichen Petrinetzen nicht aus, wenn Schaltregeln zugelassen werden, die in einem einzelnen Schritt unendlich viele Marken betreffen können (vgl. Definition 6.5).
Solche Schaltregeln machen strengere Anforderungen an die Gewichtungen nötig; hierzu wird uns der Begriff der ECN -zulässigen Gewichtung dienen.
Die Komponenten des Produktes von Gewichtung und Inzidenzmatrix
liegen bei den hier vorgestellten
linearen Invarianten in abelschen Grupepen M±
T
(X
)
zu
einem
s
∈ S. (Verallgemeinerungen sind denkbart
fin
SPEC ,esdurch Betrachten anderer abelscher Gruppen, insbesondere Faktorgruppen der hier verwendeten entsprechend [3].) Diese
Gruppen kann man
als die Quotienten der Gruppen M±
T
(X
)
nach
Äquivalenzrelatiot
fin
Ω,e
s
T (X )

nen auffassen, welche durch die Äquivalenzrelationen ≡G,Σes t auf TΩ,es (Xt )(Definition 2.14) induziert werden (vgl. Definition 2.16). Ist nämlich allgemein ∼ ∈ A × A eine Äquivalenzrelation auf einer beliebigen Menge A, so definiert ∼ zunächst über die zugehörige kanonische Abbildung(a 7→ [a]) : A → A ∼ gemäß Definition 5.9 mit Bemerkung 5.10 eine Ab± A 
±bildung M 7→ [M ] : M±fin (A) → Mfin
∼ ; dabei ist für M ∈ Mfin (A)8 Lineare Invarianten

67

A
die endliche gewichtete Menge [M ] ∈ M±fin
∼ gegeben durch [M ](b) =PAa∈A M (a) für alle b ∈∼ . Nun definiert die Abbildung M 7→ [M ] in
[a]=b
 

±
natürlicher Weise eine neue Äquivalenzrelation ∼ ⊆ M±
fin (A) × Mfin (A)±
mit M ∼ N :⇔ [M ] = [N ]. Infolge der Konstruktion ist Mfin (A) ∼mit dieser Äquivalenzrelation auf M±
fin (A) im wesentlichen das gleiche wie± A 
Mfin∼ mit der zugrundeliegenden Äquivalenzrelation auf A und ist so
mit der Struktur einer abelschen Gruppe versehen.

Definition 8.2. Es sei wie in Definition 8.1 ein algebraisches
Netz AN gegeben. Für jedes s ∈ S sei ys ∈ Ξs eine Variable. Y := {ys } s∈S sei das aus
diesen Variablen gebildete Variablensystem. Ferner sei se ∈ S eine beliebige
Sorte. Eine algebraische Gewichtung (der Sorte se mit dem Variablensystem Y ) zu AN – kurz: eine Gewichtung – ist eine Familiei = (ip )p∈P
mit




ip ∈ M±fin TΩ,es {ysp } .

i wird als Zeilenvektor aufgefaßt.
Aufbauend auf bestimmten Substitutionen wird nun eine »Multiplikation« ←− zunächst für Terme definiert, dann gemäß Definition 5.14 auf geY

wichtete Mengen von Termen übertragen und schließlich daraus eine Matrixmultiplikation einer P-indizierten Zeile mit einer P × T-Matrix (jeweils
mit gewichteten Mengen von Termen als Komponenten) konstruiert.
Definition 8.3. Sei (S, Ω) eine Signatur, Ξ = (Ξs )s∈S ein Variablensystem
zu (S, Ω), Y = {ys } s∈S eine Variablensystem mit ys ∈ Ξs für jedes s ∈ S
sowie se ∈ S eine Sorte. Weiter sei X ⊆ Ξ ein beliebiges Variablensystem. Fürjedes s ∈ S wird eine Abbildung←− : TΩ,es {ys } × TΩ,s (X) → TΩ,es (X)Y

definiert durch

T1 ←− T2 := σ T2 (T1 ),
Y

ys

wobei
σ T2 : {ys } → TΩ (X)ysdie durch
σ T2 (ys ) := T2ysdefinierte Substitution (siehe Definitionen 1.10 und 1.11) ist.

68

8 Lineare Invarianten

Satz 8.4. Sei SPEC = (S, Ω, Ξ, G)
eine Gleichungsspezifikation (Definiti
on 2.3) und A = (A) , (fω )ω∈Ω eine SPEC -Algebra (Definition 2.5). Wei s s∈S
ter sei Y = {ys } s∈S ein Variablensystem (ys ∈ Ξs für s ∈ S), se ∈ S eine
Sorte und X ⊆ Ξ ein Variablensystem, so daß gemäß Definition 8.3 für jedes s ∈ S eine Abbildung←− : TΩ,es {ys } × TΩ,s (X) → TΩ,es (X)Y

definiert ist. Gemäß Definition 1.22 hat man für s ∈ S AbbildungeninterpretA : TΩ,es {ys } → Abb(As , Aes ),interpretA : TΩ,s (X) → Abb(B, As )undinterpretA : TΩ,es (X) → Abb(B, Aes ),

wobei


B := α = (αs )s∈S ∀ s ∈ S : αs ∈ Abb(Xs , As )die Menge aller Belegungen von X in der Algebra A bezeichnet und die
Menge der Belegungen von {ys } in A mit As identifiziert wird. Gemäß Definition 2.16 sei.
TSPEC (X) = TΣ (X)
T (X) ;
≡GΣ
für jedes s ∈ S sind die Elemente von TSPEC ,s (X) Äquivalenzklassen vonTΣ (X)
Termen aus TΩ,s (X) bezüglich der Relation ≡G,s. Dann induziert die AbbildunginterpretA : TΩ,es (X) → Abb(B, Aes )eine neue AbbildunginterpretA : TSPEC ,es (X) → Abb(B, Aes ),die durch die Forderung∀ T ∈ TΩ,es (X) : interpretA [T ] := interpretA (T )wohldefiniert ist (wobei [T ] die Äquivalenzklasse von T bezeichnet), und folgendes Diagramm ist für jedes s ∈ S kommutativ:(T,U )7→ T ←−UTΩ,es {ys } × TΩ,s (X)−−−−−−−−−−→ TSPEC ,es (X)interpret ×interpretyAA

Abb(As , Aes ) × Abb(B, As )

Y

◦

−−−→


interpretyA

Abb(B, Aes )8 Lineare Invarianten

69

Beweis. Zunächst zeigen wir, daßinterpretA : TSPEC ,es (X) → Abb(B, Aes )wohldefiniert ist. Dafür seien T1 , T2 ∈ TΩ,es (X) gegeben mit [T1 ] = [T2 ],T (X)d. h. mit T1 ≡G,Σes
T2 . Zu zeigen ist, daß interpretA (T1 ) = interpretA (T1 )gilt. Laut Definition 2.14 ist (X, T1 , T2 ) ∈ clR (G). Somit ist nach Satz 2.12
(X, T1 , T2 ) gültig in A, das heißt (Definition 2.4) für jede Belegung α ∈ B ist
α(T1 ) = α(T2 ).
Dies ist aber gerade gleichbedeutend mit
interpretA (T1 )(α) = interpretA (T2 )(α)
für jedes α ∈ B, und somit haben wir in der Tat
interpretA (T1 ) = interpretA (T2 ).
Um die Kommutativität des angegebenen Diagrammes nachzuweisen,
ist zu zeigen, daß die GleichunginterpretA [T ←− U ] = interpretA (T ) ◦ interpretA (U )Y

für alle T ∈ TΩ,es {ys } , U ∈ TΩ,S (X) erfüllt ist; das heißt, daß für jedes
α∈B




interpretA [T ←− U ] (α) = interpretA (T ) interpretA (U )(α)
Ygilt. Diese Gleichung kann auch wie folgt geschrieben werden, wenn man
interpretA (U )(α) = α(U ) ∈ As als eine Belegung {ys } → A auffaßt:α(T ←− U ) = α(U )(T )Y

Daß diese Gleichung in der Tat gilt, ergibt sich durch Induktion über die
Tiefe des Terms T ∈ TΩ,es {ys } mit Definition 1.18 und Definitionen 8.3
und 1.11, wobei der Induktionsanfang darauf beruht, daß infolge Definition 8.3
α {ys } ←− U = α(U ) = α(U )(ys )Y

ist.
Um Anomalien durch Unendlichkeiten zu vermeiden, werden zu einem
gegebenen algebraischen Netz mit Endlichkeitsspezifikation durch die folgenden Definitionen nur Gewichtungen zugelassen, die bestimmte Anforderungen erfüllen. Definition 8.5 enthält Voraussetzungen, unter denen
das gewünschte Matrixprodukt überhaupt erst definiert werden kann; Definition 8.6 verschärft diese Anforderungen noch so weiter, daß jede Komponente des Matrixproduktes endlich ist.

70

8 Lineare Invarianten

Definition 8.5. AN sei wie in Definition 8.1 ein algebraisches Netz undhabe die Inzidenzmatrix D = (Dp,t )(p,t)∈P×T . Weiter sei i = (ip )p∈P eine
algebraische
Gewichtung (Definition 8.2) der Sorte se mit VariablensystemY = {ys } s∈S . Die Gewichtung i heißt zulässig, wenn die folgenden Bedingungen erfüllt sind:(i) Für jedes p ∈ P und jedes t ∈ T sind ip und Dp,t im Sinne von Definition 5.14 miteinander verträglich bezüglich ←− (so daß die gewichtete
YMenge∈ M± TΩ,es (Xt )ip ←− Dp,tY

definiert ist).
(ii) Für jedes t ∈ T ist die Familie(ip ←− Dp,t )p∈PY

von gewichteten Mengen addierbar (Definition 5.7).
Ist das der Fall, so ist das Matrixprodukt i ←− D definiert als die Familie
Y(»Zeilenvektor«)i←− D := (i ←− D)t t∈T
Y

Y

mit
(i ←
− D)t :=YX

ip ←− Dp,tp∈PY∈ M± TΩ,es (Xt )

für t ∈ T.
Definition 8.6. Sei
AN = P, T, (S, Ω, Ξ, G, T fin ), (sp )P , (Xt )T , (Fx,y )(P×T)∪(T×P)



ein algebraisches Netz (mit zugrundeliegender Gleichungsspezifikation
SPEC := (S, Ω, Ξ, G) und Endlichkeitsspezifikation SPECF := (S, Ω, Ξ, G,T fin )) und i = (ip )p∈P eine zulässige algebraischeGewichtung zu AN . i habedie Sorte se und das Variablensystem Y = {ys } s∈§ . i heißt ECN -zulässig,
wenn folgende Bedingungen erfüllt sind:(i) Es gibt nur endlich viele p ∈ P mit ip 6= ∅T(ii) ip 6= ∅Te({ysp })Ω,se({ysp }).

Ω,sgilt nur für solche p ∈ P, für die die Menge der t ∈ T

mit Dp,t 6= ∅TΩ,sp (Xt ) endlich ist.
(iii) Für jedes p ∈ P mit ip 6= ∅Te({ysp })Ω,sund jedes t ∈ T ist die gewichtete

Menge Dp,t endlich (d. h. ∈ M±
fin TΩ,sp (Xt ) ).

8 Lineare Invarianten

71(iv) Für jedes p ∈ P gilt
ip ∈ M±fin clRfin

SPEC(T fin ) ;

die Elemente der gewichteten Mengen ip enthalten also nur solche
Terme, die für jede SPECF -Algebra Endlichkeitsterme sind (sieheSatz 4.6).
− D)t ∈ M±
Bemerkung 8.7. i sei ECN -zulässig. Dann gilt (i ←fin TΩ,es (Xt )

Y

für jedes t ∈ T.

Beweis. Wir erinnern daran, daß jedes ip endlich ist. Die Behauptung gilt
wegen (i) und (iii) aus Definition 8.6.
Da diegewichteten Mengen in den Komponenten des Matrixproduktes(i ←− D)t t∈T im Fall von ECN -zulässigen Gewichtungen endlich sind, geY

langt man von ihnen wie auf Seite 66 erläutert durch Quotientenbildung
T (X )
nach den Äquivalenzrelationen ≡G,Σes t in die abelschen GruppenM±
fin TSPEC ,es (Xt ) .


Wir benutzen im folgenden jedoch nicht explizit diese Gruppen, sondern
bleiben aus Gründen der Notation auf der Ebene der gewichteten Mengen
von Termen und bringen die Äquivalenzrelation statt dessen in der Definition der linearen Invarianten unter:
Definition 8.8. Sei
AN = P, T, (S, Ω, Ξ, G, T fin ), (sp )P , (Xt )T , (Fx,y )(P×T)∪(T×P)



ein algebraisches Netz mit der Inzidenzmatrix D = (Dp,t )(p,t)∈P×T ; Σ :=(S, Ω) sei die Signatur hierzu. Weiter sei i = (ip )p∈P eine algebraische Gewichtung einer Sorte se mit Variablensystem Y zu AN . Ist i ECN -zulässig
und gilt
T (X )(i ←− D)t ≡G,Σes t ∅T (Xt )
Y

Ω,s

e

für jedes t ∈ T, so heißt i lineare Invariante für ECN .

72

8 Lineare Invarianten

8.2

Bedeutung in den Interpretationen

Nun ist eine Verbindung der linearen Invarianten, wie wir sie abstrakt füralgebraische Netze mit Endlichkeitsspezifikation definiert haben, zu den
konkreten Interpretationen (Definition 7.2) dieser algebraischen Netze anzugeben. Dabei ist unser Ziel, eine Invariante im Sinne der in Abschnitt 6.3
vorgestellten Konzepte zu erhalten; das geschieht in Corollar 8.21.
Zunächst stellen wir eine Reihe von Lemmata über gewichtete Mengenvor, die in diesem Abschnitt benötigt werden.
Lemma 8.9. (Mi,j )(i,j)∈I×J sei eine Familie von gewichteten Mengen
Mi,j ∈ M± (A). Es gebe eine endliche Teilmenge Ie ⊆ I, so daß Mi,j = ∅Ae j ∈ J. (Wegen Mi,j 6= ∅A ⇒ i ∈ Ie und weil Ie endlich
ist für alle i ∈ I\I,ist, ist dann für jedes j ∈ J die Familie (Mi,j )i∈I offensichtlich addierbar.)
Außerdem sei für jedes i ∈ I die Familie (Mi,j )j∈J addierbar. Dann sindauch die Familien
X

Mi,j



j∈J

i∈I

,

X

Mi,j

i∈I



j∈J

und

(Mi,j )(i,j)∈I×J

addierbar, und es gilt
XX

Mi,j =XX

Mi,j =i∈Ie j∈Ji∈I j∈J

X

Mi,j =(i,j)∈I×J

Beweis. Für a ∈ A sei

XX

Mi,j =j∈J i∈Ie

XX

Mi,j .

j∈J i∈I
Ka := (i, j) ∈ I × J Mi,j (a) 6= 0 .
Dann ist
Ka =

[



{i} × j ∈ J Mi,j (a) 6= 0[{i} × j ∈ J Mi,j (a) 6= 0

i∈I

=

(8.1)

i∈Ie

e Bei (8.1) ist wegen der Endlichkeit von Ie undnach der Voraussetzung über I.
der Addierbarkeit jeder Familie (Mi,j )j∈J klar, daß man es mit einer Vereinigung
einer endlichen Anzahl endlicher Mengen zu tun hat: Deshalb ist auch Ka endlich,d. h. (Mi,j )(i,j)∈I×J ist addierbar.
Wegen der Endlichkeit von Ka und

[ 
Ka =
i ∈ I Mi,j (a) 6= 0 × {j}j∈Jkann es nur endlichviele j geben,
für die i ∈ I Mi,j (a) 6= 0 nicht leer ist, undP
nur für diese kanni∈I Mi,j (a) 6= 0 sein; daraus folgt die Addierbarkeit von
P.
i∈I Mi,j
j∈J

Wegen

i ∈ I\Ie⇒Xj∈J

Mi,j = ∅A

8 Lineare Invarianten

enthält die Familie

73

Pj∈J Mi,ji∈Inur endlich viele von ∅A verschiedene Kompo-

nenten, also ist auch sie addierbar.
Daß bei Vorliegen der Addierbarkeit die im Lemma angegebenen GleichungenGültigkeit haben, ist (wegen Mi,j = ∅A für i ∈ I\Ie und alle j) klar.

Lemma 8.10. A1 , A2 , A3 und C seien Mengen undψ : A1 × A2 × A3 → C±eine Abbildung. M1 ∈ M±
fin (A1 ) und M2 ∈ Mfin (A2 ) seien endliche gewich±tete Mengen und M3 ∈ M (A3 ) eine gewichtete Menge. Weiter seien B12
und B23 Mengen und

υ1 : A1 × A2 → B12 ,ϕ1 : B12 × A3 → C,

υ2 : A2 × A3 → B23 ,ϕ2 : A1 × B23 → C

Abbildungen mit

ϕ1 υ1 (a1 , a2 ), a3 = ϕ2 a1 , υ2 (a2 , a3 ) = ψ(a1 , a2 , a3 )(8.2)

für alle a1 ∈ A1 , a2 ∈ A2 und a3 ∈ A3 . Dabei seien M2 und M3 miteinander
verträglich bezüglich υ2 (so daß υ2 (M2 , M3 ) ∈ M± (B23 ) definiert ist), und
M1 sei verträglich mit υ2 (M2 , M3 ) bezüglich ϕ2 . Außerdem sei (mindestens)
eine der folgenden Bedingungen erfüllt:• Es ist M3 ∈ M±
fin (A3 ).
• Für jedes Paar (a1 , c) ∈ A1 × C mit a1 ∈ supp(M1 ) ist die Mengeb23 ∈ B23 ϕ2 (a1 , b23 ) = c

endlich.
Nach den Voraussetzungen sind (gemäß Bemerkung 5.19) M1 und M2 miteinander verträglich bezüglich υ1 (mit υ1 (M1 , M2 ) ∈ M±
fin (U12 )). Außerdem
gilt folgendes: υ1 (M1 , M2 ) ist verträglich mit M3 bezüglich ϕ1 , und es ist

ϕ1 υ1 (M1 , M2 ), M3 = ϕ2 M1 , υ2 (M2 , M3 ) .

(8.3)

Beweis. Für den Fall M3 ∈ M±
fin (A3 ) folgt die Behauptung mit Bemerkung 5.18
direkt aus (8.2) auf Seite 73.
Im folgenden gehen wir vom anderen Fall aus:
(8.4)∀(a1 , c) ∈ supp(M1 ) × C : b23 ∈ B23 ϕ2 (a1 , b23 ) = c ist endlich.
Für diesen zeigen wir zunächst: Zu beliebig gewählten a1 ∈ supp(M1 ), a2 ∈supp(M2 ), c ∈ C ist die MengeSa1 ,a2 := a3 ∈ supp(M3 ) ψ(a1 , a2 , a3 ) = c
endlich.
Aus (8.4) folgt, daß die MengeTa1 ,a2 := b23 ∈ B23 ∃ a3 ∈ supp(M3 ) : b23 = υ2 (a2 , a3 ), ϕ2 (a1 , b23 ) = c

74

8 Lineare Invarianten

endlich ist. Nun ist
Ta1 ,a2 = υ2 (a2 , a3 ) a3 ∈ Sa1 ,a2 ;das heißt, falls nicht bereits Sa1 ,a2 endlich ist, muß es ein b23 ∈ Ta1 ,a2 ⊆ B23 geben,
für das die Mengea3 ∈ Sa1 ,a2 υ2 (a2 , a3 ) = b23

unendlich ist. Das kann aber nicht sein, denn dann wäre (wegen a2 ∈ supp(M2 )und Sa1 ,a2 ⊆ supp(M3 )) M2 entgegen der Voraussetzung nicht verträglich mit M3
bezüglich υ2 . Somit ist Sa1 ,a2 in der Tat endlich.
Wir wollen jetzt nachweisen, daß υ1 (M1 , M2 ) mit M3 verträglich ist bezüglich
ϕ1 . Dafür ist zu zeigen, daß für jedes c ∈ C die Menge(b12 , a3 ) ∈ supp υ1 (M1 , M2 ) × supp(M3 ) ϕ1 (b12 , a3 ) = c

endlich ist. Weil ϕ1 (M 1 , M2 ) eine endliche gewichtete Menge und somit der Träger supp ϕ1 (M1 , M2 ) eine endliche
Menge ist, reicht es aus zu zeigen, daß für
beliebiges b12 ∈ supp υ1 (M1 , M2 ) die Menge
Sb12 := a3 ∈ supp(M3 ) ϕ1 (b12 , a3 ) = c
endlich ist. Jedes solche b12 hat eine Darstellung b12 = υ1 (a1 , a2 ) mit a1 ∈ supp(M1 )und a2 ∈ supp(M2 ); für diese ist wegen ϕ1 (b12 , a3 ) = ψ(a1 , a2 , a3 ) gerade Sb12 =Sa1 ,a2 , und die Endlichkeit dieser Menge haben wir bereits bewiesen.
Zu zeigen bleibt noch (8.3) auf Seite 73. Dafür ist nachzuweisen, daß für jedes
c∈C




ϕ1 υ1 (M1 , M2 ), M3 (c) = ϕ2 M1 , υ2 (M2 , M3 ) (c)(8.5)
gilt. Zunächst stellen wir fest, daß die Menge(a1 , a2 , a3 ) ∈ supp(M1 ) × supp(M2 ) × supp(M3 ) ψ(a1 , a2 , a3 ) = c
endlich ist: Denn supp(M1 ) und supp(M2 ) sind endlich, und zu jedem der Paare(a 1 , a2 ) ∈ supp(M1 ) × supp(M2 ) ist – wie weiter oben gezeigt – die Menge Sa1 ,a2 =a3 ∈ supp(M3 ) ψ(a1 , a2 , a3 ) = c endlich. Somit ist die SummeX
M1 (a1 ) · M2 (a2 ) · M3 (a3 )(a1 ,a2 ,a3 )∈supp(M1 )×supp(M2 )×supp(M3 )ψ(a1 ,a2 ,a3 )=c

definiert. Anhand Definition 5.14 erhält man, daß diese Summe gleich
ϕ1 υ1 (M1 , M2 ), M3 (c)sowie gleich
ϕ2 M1 , υ2 (M2 , M3 ) (c)ist. Zusammen ergibt sich (8.5).

Lemma 8.11. A1 , B1 , C1 und A2 , B2 , C2 seien Mengen und
f1 : A1 × B1 → C1 ,f2 : A2 × B2 → C2 ,g : A1 → A2 ,h : B1 → B2 ,i : C1 → C2

8 Lineare Invarianten

75

seien Abbildungen, für die das Diagramm
f1

A1 × B1 −−−→ C1

g×h
y



yi

A2 × B2 −−−→ C2
f2





kommutativ ist (d. h. für (a1 , b1 ) ∈ A1 ×B1 gilt i f1 (a1 , b1 ) = f2 g(a1 ), h(b1 ) .
Dann ist (für die durch f1 , f2 , g, h und i gemäß Definition 5.14 und Bemerkung 5.19 bzw. gemäß Definition 5.9 und Bemerkung 5.10 induzierten
Abbildungen) auch das folgende Diagramm kommutativ:
f1

±
±
M±
fin (A1 ) × Mfin (B1 ) −−−→ Mfin (C1 )


g×h
y



yi

±
±
M±
fin (A2 ) × Mfin (B2 ) −−−→ Mfin (C2 )f2

Beweis. Zu zeigen ist, daß
i f1 (M1 , N1 ) = f2 g(M1 ), h(N1 )±für alle (M1 , N1 ) ∈ M±
| , {|b1}| )fin (A1 ) × Mfin (B1 ) gilt. Für den Fall (M1 , N1 ) = {|a1 }mit a1 ∈ A1 , b1 ∈ B1 folgt das direkt aus der Voraussetzung. Der allgemeine Fall
folgt durch Induktion mit Bemerkungen 5.18 und 5.23.

Eine direkte Folgerung hieraus ist das folgende Lemma:
Lemma 8.12. C1 , C2 seien Mengen, i : C1 → C2 eine Abbildung, J eine
endliche Menge, und für jedes j ∈ J seien A1,j , A2,j , B1,j , B2,j Mengen und
f1,j : A1,j × B1,j → C1 ,f2,j : A2,j × B2,j → C2 ,gj : A1,j → A2,j ,hj : B1,j → B2,jAbbildungen, für die (wie bei Lemma8.11) das Diagramm
f1,j

A1,j × B1,j −−−→ C1

g ×h
y j j



yi

A2,j × B2,j −−−→ C2
f2,jkommutativ ist. Aus den gemäß Lemma 8.11 für jedes j erhaltenen kommutativen Diagrammen ergibt sich, daß auch das folgende Diagramm kom-

76

8 Lineare Invarianten

mutativ ist:
Q 

j∈J

Q 

j∈J



±
M±
fin (A1,j ) × Mfin (B1,j )Q (gj ×hj )
yj∈J



±
M±
fin (A2,j ) × Mfin (B2,j )

Q

f1,j

j∈J

−−−−→

Q

j∈J

−Q
−−−→
f2,j

Q

j∈J

M±
fin (C1 )
Q
 i
yj∈J

M±
fin (C2 )j∈J

Außerdem ist das Diagramm
Σ

Q

j∈J

±
M±
fin (C1 ) −−−→ Mfin (C1 )

Q
 i
yj∈J

Q

j∈J



yi

±
M±
fin (C2 ) −−−→ Mfin (C2 )Σkommutativ, wobei für k ∈ {1, 2}
Σ:

Y

±
M±
fin (Ck ) → Mfin (Ck )j∈J

die Abbildung ist, die Familien von gewichteten Mengen mit der endlichen
Q±
Indexmenge J aufaddiert (d. h. für γ ∈ j∈J M±
fin (Ck ), also γ(j) ∈ Mfin (Ck )P
für j ∈ J, ist Σ(γ) = j∈J γ(j)). Diese beiden Diagramme kann man zusammensetzen, wodurch man folgendes kommutative Diagramm erhält:
Σ◦

Q 

j∈J

Q 

j∈J



±
M±
fin (A1,j ) × Mfin (B1,j )Q (gj ×hj )
yj∈J



±
M±
fin (A2,j ) × Mfin (B2,j )

Q

f1,j

j∈J



−−−−−−−−→ M±
fin (C1 )


yi

±
−−−−Q
−−−−→
 Mfin (C2 )
Σ◦

f2,j

j∈J

Jetzt zeigen wir, wie in einem Modell der Endlichkeitsspezifikation eines algebraischen Netzes aus einer linearen Invarianten, also aus einer Familie von gewichteten Mengen von Termen, eine Familie von gewichteten
Mengen von Abbildungen gewonnen werden kann. Von letzterer gelangen
wir dann zu einer Äquivalenzrelation auf der Menge der Markierungen desinterpretierten Netzes und weisen nach, daß es sich dabei um eine Invariante gemäß der Definition 6.15 handelt.
Bemerkung 8.13. Sei ein Modell
A = (As )s∈S , (fω )ω∈Ω

der Endlichkeitsspezifikation (S, Ω, Ξ, G, T fin ) gegeben (siehe Definition 4.3). Gemäß Definition 1.22 hat man AbbildungeninterpretA : TΩ,es ({ys }) → Abb(As , Aes ),8 Lineare Invarianten

77

wobei hier Belegungen α : {ys } → As mit den jeweiligen Elementen von
As identifiziert werden. Für die mit interpretA auswertungsverträglichen(Definition 5.9) gewichteten Mengen erhält man hieraus Abbildungen±interpretA : M±
interpretA TΩ,es ({ys }) → M Abb(As , Ae
s) .





Bemerkung 8.14. Nach Bemerkung 5.10 ist±
M±
fin TΩ,es ({ys }) ⊆ MinterpretA TΩ,es ({ys }) ,und wegen







ip ∈ M±fin TΩ,es {ysp }ist somit für jedes p ∈ P die gewichtete MengeinterpretA (ip ) ∈ M±
fin Abb(Asp , Aes)

definiert.

Bemerkung 8.15. i sei ECN -zulässig. Nach Definition 8.6 sind dann fürjedes p ∈ P alle Elemente T von ip Endlichkeitsterme für A, d. h. für jedes
e endlich;e ∈ Aeas ist die Menge der Belegungen α : {ysp } → A mit αes (T ) = a
in der Sprache von Bemerkung 8.13 heißt das, die Menge

ist endlich.

ea ∈ Asp interpretA (T )(a) = a

Definition 8.16. Sei
AN = P, T, (S, Ω, Ξ, G, T fin ), (sp )P , (Xt )T , (Fx,y )(P×T)∪(T×P)



ein algebraisches Netz. Zu diesem Netz sei i eine lineare Invariante für ECN ,l-fin oder für E fin . Weiter sei ein Modell A = (A )für ECNs s∈S , (fω )ω∈Ω derCN
Endlichkeitsspezifikation (S, Ω, Ξ, G, T fin ) gegeben, durch das AN interpretierbar (Definition 7.2) ist. Nun sei die Familieι := (ιp )p∈P
definiert durch
ιp := interpretA (ip )für jedes p ∈ P (so daß ιp ∈ M±
fin Abb(Asp , Aes ) ist, siehe Bemerkung 8.14).
Weiter werde für Markierungen der Interpretation

CN := P, T, (Asp )p∈P , (Bt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P)



von AN (mit Bt und Fp,t wie in Definition 7.2) die Relation ∼ι ⊆ MCN ×MCN
dadurch definiert, daßm ∼ι m0
für m, m0 ∈ MCN (mit m = (mp )p∈P und m0 = (m0p )p∈P ) genau dann geltensoll, wenn die folgenden Bedingungen erfüllt sind (von denen die zweite unddritte auf der jeweils vorhergehenden aufbauen):

78

8 Lineare Invarianten(i) Für jedes p ∈ P ist die gewichtete Menge m0p − mp auswertungsverträglich mit ιp .
(ii) Die Familie ιp (m0p − mp ) p∈P ist addierbar.
(iii) Es istXιp (m0p − mp ) = ∅A .
esp∈P

Bemerkung 8.17. Die Relation ∼ι ist eine Äquivalenzrelation.
Beweis. Reflexivität, Symmetrie und Transitivität sind ohne weiteres anhand der Definitionen für Auswertungsverträglichkeit (Definition 5.9) undfür Addierbarkeit und Summenbildung (Definition 5.7) nachzuvollziehen.
Bemerkung 8.18. i sei ECN -zulässig. Für jedes Element f von ιp (p ∈ P
e ∈ Aebeliebig) und jedes as ist dann die Mengee}{a ∈ Asp | f (a) = a

endlich. Das folgt direkt aus Bemerkung 8.15, denn jedes Element von ιp
hat eine Darstellung interpretA (T ), wobei T ein Element von ip ist.
Bemerkung 8.19. Sei D = (Dp,t )(p,t)∈P×T die Inzidenzmatrix von AN . Fürdas in Definition 8.16 angegebene gefärbte Netz CN gilt wegen Fx,y =interpretA (Fx,y ) (Definition 7.2) und −Fp,t + Ft,p = Dp,t (Definition 8.1) nach
Bemerkung 5.23 die Gleichung−Fp,t + Ft,p = interpretA (Dp,t ).
Satz 8.20. Es liege die Situation von Definition 8.16 vor. Sind m, m0 ∈ MCN
gegeben mit m →E m0 (siehe Definition 6.8), so gilt m ∼ι m0 .
Beweis. Es sind nacheinander die Bedingungen (i), (ii) und (iii) aus Definition 8.16 zu prüfen. Zunächst bemerken wir, daß für jedes p ∈ P
m0p − mp = −Xt∈T

Fp,t (et ) +X

Ft,p (et )

(8.6)

t∈T

ist mit einem e = (et )t∈T ∈ ECN (siehe Definitionen 6.7 und 6.8). Wenn
D = (Dp,t )(p,t)∈P×T die Inzidenzmatrix von AN bezeichnet, folgt daraus
m0p − mp =X

− Fp,t (et ) + Ft,p (et )X− Fp,t + Ft,p (et )XinterpretA (Dp,t )(et )



t∈T

=

t∈T

=



(8.7)

t∈T

gemäß (in dieser Reihenfolge verwendet) Bemerkung 5.8, Bemerkung 5.20
und Bemerkung 8.19.

8 Lineare Invarianten

79

Zu (i) aus Definition 8.16: Wegen Bemerkung 8.18 ist jede gewichtete
Menge über Asp auswertungsverträglich mit jedem Element von ιp . Weil ιpaußerdem eine endliche gewichtete Menge ist, ist gemäß Bemerkung5.13
jede gewichtete Menge über Asp auswertungsverträglich mit ιp .
Zu (ii) aus Definition 8.16: Weil i ECN -zulässig ist (Definition 8.6), gibt
es nur endlich viele p ∈ P mit ip 6= ∅T ({ysp }) . Für p ∈ P mit ip = ∅T ({ysp })
Ω,s

Ω,s

e

e

ist auch ιp leer und gilt somit ιp (m0p − mp ) = ∅A . Also hat die Familieesιp (m0p − mp ) p∈P nur endlich viele von ∅A verschiedene Komponenten undes
ist folglich addierbar.
Zu (iii) aus Definition 8.16:
Sei zunächst p ∈ P vorgegeben mit ip 6= ∅T ({ysp }) . Dann gibt es


Ω,s

e

e ⊆ T mit
infolge von (ii) aus Definition 8.6 eine endliche Menge Tpe . Nach dem bereits geführten Beweis
interpretA (Dp,t )(et ) = ∅Asp für t ∈ T\Tp
von (i) aus Definition 8.16, angewandt auf einen Teilschritt von e gemäß
Bemerkung 6.6, ist interpretA (Dp,t )(et ) auswertungsverträglich mit ιp . Dae endlich ist, sind die beiden FamilienTpinterpretA (Dp,t )(et ) t∈T
e

p



und



ιp interpretA (Dp,t )(et )addierbar mit
ιp

 X



interpretA (Dp,t )(et ) =

ep
t∈T

X

ep
t∈T


ιp interpretA (Dp,t )(et )ept∈Te ohnehin interpret (D )(e ) = ∅(laut Bemerkung 5.20). Da für t ∈ T\T
p,t
t
p
Asp
A

und also auch ιp interpretA (Dp,t )(et ) = ∅A gilt, kann man die Summierunes
gen auf die gesamte Menge T ausdehnen:

ιp

X



interpretA (Dp,t )(et ) =

t∈T

X



ιp interpretA (Dp,t )(et ) .

t∈T

Diese Gleichung gilt sogar für jedes p ∈ P, denn bei ip = ∅Te({ysp })

ist

Ω,s

ιp = ∅Abb(Asp ,A ) , und die Gleichung ist dann trivialerweise erfüllt. Mit (8.7)
esfolgt für beliebiges p ∈ P
ιp (m0p − mp ) =Xιp interpretA (Dp,t )(et ) ,t∈Tund also ergibt sich (wegen der bereits bewiesenen Addierbarkeit – (ii) aus
Definition 8.16)
Xp∈Pιp (m0p − mp ) =XXιp interpretA (Dp,t )(et ) .

p∈P t∈T

Hierbei liegen die Voraussetzungen zur Anwendung von Lemma 8.9 vor:e bestehe aus den endlich vielen p mit i 6= ∅Pp
T ({ysp }) (siehe (i) in DefiniΩ,setion 8.6); darunter sind zwangsläufig alle p mit ιp 6= ∅Abb(Asp ,A ) ). Gemäßes

80

8 Lineare Invarianten

Lemma 8.9 erhält man nunXιp (m0p − mp ) =

p∈P

XX



ιp interpretA (Dp,t )(et ) .

t∈T p∈Pe

Zum Nachweis vonXιp (m0p − mp ) = ∅A

es

p∈P

reicht es deshalb aus zu zeigen, daß für jedes t ∈ TXιp interpretA (Dp,t )(et ) = ∅A

e
p∈P

ist.

(8.8)

es

e
Wir wollen zunächst zeigen, daß für p ∈ Pιp interpretA (Dp,t )(et ) = ιp ◦ interpretA (Dp,t ) (et )(8.9)

ist. Falls interpretA (Dp,t ) leer ist, gilt dies trivialerweise. Andernfalls
e ist
kommt Lemma 8.10 zum Einsatz: Für p ∈ Pιp ∈ M±
fin Abb(Asp , Aes) ,interpretA (Dp,t ) ∈ M±
fin Abb(Bt , Asp )e und wegen (iii) in Definition 8.6). Die Ab(letzteres gilt nach Wahl von P
bildung
ψp,t : Abb(Asp , Aes ) × Abb(Bt , Asp ) × Bt → Aes

sei definiert durchψp,t (g, f, a) := g f (a) .
Im folgenden Teil des Beweises werden p und t nicht variiert, deshalb können wir zur Vereinfachung der Notation ψ := ψp,t setzen. Die Abbildungenυ1 , ϕ1 , υ2 , ϕ2 in Lemma 8.10 wählen wir in natürlicher Weise wie folgt:υ1 := (g, f ) 7→ g ◦ f : Abb(Asp , Aes ) × Abb(Bt , Asp ) → Abb(Bt , Aes ),

ϕ1 := (f, a) 7→ f (a) : Abb(Bt , Aes ) × Bt → Aes ,υ2 := (f, a) 7→ f (a) : Abb(Bt , Asp ) × Bt → Asp ,

ϕ2 := (f, a) 7→ f (a) : Abb(Asp , Aes ) × Asp → Aes .

Damit gilt, wie bei Lemma 8.10 gefordert,

ϕ1 υ1 (g, f ), a = ϕ2 g, υ2 (f, a) = ψ(g, f, a)
für g ∈ Abb(Asp , Aes ), f ∈ Abb(Bt , Asp ) und a ∈ Bt . Die weitere Voraussetzung von Lemma 8.10 liest sich hier wie folgt:• et ist endlich, oder

8 Lineare Invarianten

81e ∈ Ae• für jedes f ∈ Abb(Asp , Aes ) mit f ∈ supp(ιp ) und jedes as ist dieMengee}{a ∈ Asp | f (a) = a

endlich.

e ∈ AeFür f ∈ supp(ιp ) und as ist nach Bemerkung 8.18 die Mengee}{a ∈ Asp | f (a) = a

endlich, also liegen die Voraussetzungen von Lemma 8.10 vor. Gemäß Lemma 8.10 folgt jetzt, daß die Gleichung (8.9) in der Tat gilt.
Mit (8.9) kann die linke Seite der Gleichung (8.8) auch alsXιp ◦ interpretA (Dp,t ) (et )ep∈Pe und nach Bemergeschrieben werden. Wegen der Endlichkeit von P
kung 5.20 ist die eben angegebene Summe gleichXιp ◦ interpretA (Dp,t ) (et ).

ep∈PSomit reicht es zum Nachweis von (8.8) aus, folgende Gleichung zu beweisen, in der et nicht mehr vorkommt:Xιp ◦ interpretA (Dp,t ) = ∅Abb(Bt ,A )(8.10)esetp∈P

e so gewählt, daß für p ∈ P\P
e notwendig i = ∅Wir hatten PpT

Für solche p ist ip ←− Dp,t = ∅T
Y

X

p∈P

e(Xt ), und ausΩ,se({ysp })

ist.

Ω,s

T (X )

ip ←− Dp,t ≡G,Σes t ∅TYe(Xt )Ω,s(gemäß Definition 8.5 und Definition 8.8) folgt demnachXep∈P

T (X )

ip ←− Dp,t ≡G,Σes t ∅TYe(Xt ).

(8.11)Ω,sLaut Satz 8.4 ist das Diagramm
(T,U )7→ T ←−UTΩ,es {ysp } × TΩ,sp (Xt )−−−−−−−−−−→ TSPEC ,es (Xt )interpret ×interpretyAA

Abb(Asp , Aes ) × Abb(Bt , Asp )

Y



◦

−−−→


interpretyA

Abb(Bt , Aes )82

8 Lineare Invarianten

für jedes sp kommutativ. Nach Lemma 8.12 ist somit auch das Diagramm
Q

Q

p∈P

e

Q

M±
T
fin

Ω,s

({ysp }) × M±
TΩ,sp (Xt )
fin



e



p∈P

es

e

Y



−−−−−−−−−−−−−−−−−−−→ M±
T
fin

e

Q
 (interpretA ×interpretA )
y
p∈e
P


±

M±
Abb(Asp , A ) × Mfin Abb(Bt , Asp )
fin

p∈P



(T,U )7→ T ←−U

Σ◦

Q




interpretAyM±
Abb(Bt , A )
fin
es

−−−
−−−−−
→Σ◦e(Xt )

SPEC ,s◦p∈Pee ist eine endliche Menge. Durch dieses Diagramm verkommutativ, denn P
folgt man nun, was mit(ip , Dp,t )p∈P
e∈

Y
e
p∈P



±
M±
fin TΩ,es ({ysp }) × Mfin TΩ,sp (Xt )e in der Tat endlich ist,geschieht. (Daß die gewichtete Menge Dp,t für p ∈ Pefolgt nach Wahl von P aus (ii) und (iii) in Definition 8.6.) Beim oberen Pfeil
gelangt man zu

Σ

 

ip ←
− Dp,t
Y





e =
p∈P

X



ip ←
− Dp,t = ∅T
Y

e
p∈P

laut (8.11), und wegen interpretA (∅Te(Xt )

SPEC ,s) = ∅Abb(Bt ,A ) (rechter Pfeil)

ist gemäß der Kommutativität des Diagramms auche(Xt )

SPEC ,sesΣ interpretA (ip ) ◦ interpretA (Dp,t ) p∈P
e = ∅Abb(Bt ,A )es(linker und unterer Pfeil). Das ist gerade die zu zeigende Gleichung (8.10).

Corollar 8.21. In der Situation von Definition 8.16 gilt
∼ECN ⊆ ∼ι(mit ∼E gemäß Bemerkung 6.19), das heißt, (∼ι , MCN ) ist dann eine Invariante (der (CN , M0 )-Netzsysteme mit beliebigem M0 ⊆ MCN ) bezüglich ECN
entsprechend Definition 6.15.
Beweis. Es seien m, m0 ∈ MCN gegeben mit m ∼ECN m0 . Dann gilt auchm ∼ι m0 ; das folgt wegen Bemerkung 8.17 und Satz 8.20 direkt aus derDefinition von ∼ECN .
Corollar 8.22. Speziell folgt somit: Ist m0 ∈ MCN und sind m, m0 ∈ [m0 i,
so gilt m ∼ι m0 .

8 Lineare Invarianten

83

Beispiel 8.23. Seien
AN 1 = P, T, SPECF 1 , (sp )p∈P , (Xt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P)



AN 2 = P, T, SPECF 2 , (sp )p∈P , (Xt )t∈T , (Fx,y )(x,y)∈(P×T)∪(T×P)

unddie algebraischen Netze aus Beispiel 7.3.
Die Inzidenzmatrix (Definition 8.1) gleichermaßen von AN 1 und von
AN 2 ist
D := (Dp,t )(p,t)∈{p}×{t1 ,t2 }mitDp,t1 := {|x1 , x1 +1 11}| ,Dp,t2 := −{|x1 , x1 +1 11}| ;optisch als Matrix mit in diesem Fall nur einer Zeile angeordnet alsoD = {|x1 , x1 +1 11}|− {|x1 , x1 +1 11}| .

Sei y ∈ Ξs1 eine beliebige Variable der Sorte s1 und Y := {y} ⊆ Ξ das
nur aus dieser Variable bestehende Variablensystem. Nun sei i := (ip )p∈{p}definiert durch∈ M±
fin TΩ,s2 ({y}) .


ip := {|ϕ(y)|} − {|ϕ(y +1 11 )|}i ist (gleichermaßen für AN 1 wie für AN 2 ) eine algebraische Gewichtung
der Sorte s2 gemäß Definition 8.2. Weil die Menge P und die Multimengen ip , Dp,t1 und Dp,t2 endlich sind, ist die Gewichtung i zulässig (Definition 8.5), so daß das Matrixprodukt i ←− D definiert ist:Yi←
− D = (i ←− D)t t∈{t1 ,t2 }
Y

Y

mit
(i ←
− D)t1 = ip ←− Dp,t1YY= {|ϕ(y)|} − {|ϕ(y +1 11 )|} ←− {|x1}| + {|x1 +1 11}|
n

o

n

Y

= ϕ(y) ←− x1 + ϕ(y) ←− x1 +1 11
Y

n

Y

o

n

o

− x1 +1 11− ϕ(y +1 11 ) ←− x1 − ϕ(y +1 11 ) ←YY= {|ϕ(x1 )|} + {|ϕ(x1 +1 11 )|} − {|ϕ(x1 +1 11 )|}|− ϕ (x1 +1 11 ) +1 11{z=∅TΩ,s ({x1 })2= {|ϕ(x1 )|} − ϕ (x1 +1 11 ) +1 11



}

o

84

8 Lineare Invariantenund (wegen Dp,t2 = −Dp,t1 )(i ←− D)t2 = −(i ←− D)t1YY= ϕ (x1 +1 11 ) +1 11

− {|ϕ(x1 )|}.

Nun ist die Bedingung aus Definition 8.6 zu prüfen: i ist ECN -zulässig
im Falle des Netzes AN 1 ; insbesondere ist dann nämlich
ip ∈ M± clRfin

SPEC(T fin )laut Beispiel 4.8. Betrachtet man jedoch AN 2 , so ist i nicht ECN -zulässig
wegen
ip 6∈ M± clRfin (T fin ) ;SPECdenn wie man sich anhand der Fälle mit n1 = 0 in Beispiel 2.21 klarmacht,
ist ϕ(y) nicht für jede SPECF 2 -Algebra ein Endlichkeitsterm und kann somit aufgrund der Korrektheit des Regelsystems nicht in clRfin (T fin ) lieSPEC
gen, es dürfte also nicht in ip vorkommen.
Jetzt soll gezeigt werden, daß i eine lineare Invariante für ECN ist, sofern i ECN -zulässig ist; d. h. im Fall von AN 1 . Zu prüfen sind nach dem
Vorhergehenden nur noch folgende Bedingungen:
T ({x })

∅TΩ,s2 (Xt ) ,T ({x })

∅TΩ,s2 (Xt ) .

1
Σ
(i ←
− D)t1 ≡G,s
2

Y

1
Σ
(i ←
− D)t2 ≡G,s2

Y

Wegen (i ←− D)t2 = −(i ←− D)t1 reicht es hierbei aus, nur eine dieser
YY

Kongruenzen nachzuweisen. Um das zu tun, stellen wir zunächst fest:T (∅)Σ
ϕ(11 +1 11 ) ≡G,sϕ(11 ) +1 ϕ(11 )
2

T (∅)

Σ
≡G,s
02 ,
2

T ({x })1Σ
(x1 +1 11 ) +1 11 ≡G,s1

ϕ (x1 +1 11 ) +1 11



x1 +1 (11 +1 11 ),TΣ ({x1 })≡G,sϕ(x1 ) +2 ϕ(11 +1 11 )2TΣ ({x1 })≡G,s2
ϕ(x1 );

alle diese Kongruenzen sind leicht anhand der Schlußregeln aus Definition 2.11 und der Gleichungsmenge G aus Beispiel 2.21 zu zeigen. Damit sehen wir für die bereits weiter oben ausgerechnete Darstellung von(i ←− D)t1 folgendes:Y{|ϕ(x1 )|} − ϕ (x1 +1 11 ) +1 11T ({x }){|ϕ(x1 )|} − {|ϕ(x1 )|}T ({x })

∅TΩ,s2 (Xt ) .

1
Σ
≡G,s
2

1
Σ
≡G,s
2

Also hat i tatsächlich die geforderte Eigenschaft und ist eine lineare Invariante.

8 Lineare Invarianten

85

Nun wollen wir Corollar 8.21 anwenden und Interpretationen der linearen Invarianten i angeben. Das Ziel dabei ist es, so zu einem Nachweis
für die in Beispiel 6.20 für bestimmte G vermuteten Invarianten der dortbehandelten gefärbten Netze CN G aus Beispiel 6.2 zu gelangen. In Beispiel 7.3 wurden einige Algebren angegeben, durch die AN 2 und in vielen
Fällen auch AN 2 interpretierbar ist: Sei
A := (As )s∈S , (fω )ω∈Ω



mit
As1 := Z n Z ,As2 := Z 2 Z ,fϕ (x) := x

mit einer geraden Zahl n ∈ Z\{0}, wobei die übrigen Operationen f+1 , f+2 ,f−1 , f−2 und die Konstanten f01 , f11 , f02 in natürlicher Weise (vgl. Beispiel 2.21) definiert seien und x = 0 + 2 Z = f02 für gerades x, x = 1 + 2 Z 6=f02 für ungerades x sei. Für solche Algebren hatten wir gesehen: A ist eine SPEC -Algebra, und AN 2 ist in jedem Fall durch A interpretierbar; aber
nur bei n 6= 0 ist A auch eine SPECF -Algebra, so daß AN 1 durch A interpretierbar ist.
Die Familie ι := (ιp )p∈{p} aus Definition 8.16 hat hier die (einzige) Komponenteιp := interpretA (ip ) = interpretA {|ϕ(y)|} − {|ϕ(y +1 11 )|} .
Bei den oben angegebenen Algebren istιp = {|(x 7→ x)|} − {|(x 7→ x + 1)|},d. h. mit G := As1 ist für ∆ ∈ M±
fin (G)ιp (∆) =X∆(g) · 0 +X∆(g) · 1 −g∈Gg gerade−X∆(g) · 1X∆(g) · 0g∈Gg ungeradeg∈Gg gerade(8.12)g∈G
g ungerade(wegen x + 1 = 1 für gerades, x + 1 = 0 für ungerades x). Es giltιp (∆) = ∅ Z 

2Z



genau dann, wennιp (∆) (0) = 0undιp (∆) (1) = 0

ist; diese beiden Einzelbedingungen sind wegen (8.12) und 0 6= 1 gleichwertig zueinander und zu
0=

X

g∈G
g gerade∆(g) −Xg∈G
g ungerade

∆(g).

86

8 Lineare Invarianten

Legt man ∼ι gemäß Definition 8.16 fest, so ergibt sich für m = (mp )p∈{p} ,m0 = (m0p )p∈{p} ∈ MCN G mit endlicher Differenz m0p − mp (=: ∆) also genau
das gleiche wie für die in Beispiel 6.20 angegebene Relation ∼.
Wir hatten für den Fall von AN 1 gesehen, daß i eine lineare Invariante für ECN ist. Die Relation ∼ι aus Definition 8.16 ist deshalb laut Corollar 8.21 eine Invariante, genau wie es in Beispiel 6.20 (für die dort ∼heißende Relation) vermutet wurde.
Im Fall von AN 2 dagegen ist i keine lineare Invariante für ECN . Das
stimmt mit der Beobachtung aus Beispiel 6.20 überein, daß bei G = Z,
E = ECN die dortige Relation ∼ keine Invariante sein kann.
Dieses Beispiel zeigt den Nutzen von Endlichkeitsspezifikationen: Es
ist gelungen, die Invariante von CN G über das algebraische Netz AN 1
nachzuweisen; ein solcher Nachweis ist dagegen über AN 2 (das bis auf
das Fehlen der Endlichkeitsterme in der zugrundeliegenden Spezifikation gleich AN 1 ist) nicht möglich, denn in manchen Interpretationen von
AN 2 gilt gar keine entsprechende Invarianzeigenschaft.

Literatur[1] N. B OURBAKI : Théorie des ensembles. Éléments de mathématique.
Paris, Hermann, 1970.
[2] S. C HRISTENSEN, N. D. H ANSEN : Coloured Petri Nets Extended with
Place Capacities, Test Arcs and Inhibitor Arcs. – M. A. Marsan, ed.:Application and Theory of Petri Nets 1993. Lecture Notes in Computer Science 691. Springer-Verlag, 1993. [ISBN 3-540-56863-8 und
0-387-56863-8][3] J. D ESEL , K.-P. N EUENDORF, M.-D. R ADOLA : Proving nonreachability by modulo-invariants. – Theoretical Computer Science 153 (1996)
49–64. [ISSN 0304-3975][4] H.-D. E HRICH , M. G OGOLLA , U. W. L IPECK : Algebraische Spezifikation abstrakter Datentypen. Stuttgart, B. G. Teubner, 1989. [ISBN3-519-02266-4][5] H. E HRIG, B. M AHR : Fundamentals of Algebraic Specification 1.
EATCS Monographs on Theoretical Computer Science 6. SpringerVerlag, 1985. [ISBN 3-540-13718-1 und 0-387-13718-1][6] H. E HRIG, B. M AHR : Fundamentals of Algebraic Specification 2.
EATCS Monographs on Theoretical Computer Science 21. SpringerVerlag, 1990. [ISBN 3-540-51799-5 und 0-387-51799-5][7] H. E HRIG, J. L OECKX , B. M AHR : A Remark on the Equational Calculus for Many-Sorted Algebras with Possibly Empty Carrier Sets. –Bulletin of the EATCS # 30 (October 1986) 61–66.
[8] P. A. F OJER , D. A. S IMOVICI : Mathematical Foundations of Computer Science 1. New York, Springer-Verlag, 1991. [ISBN 0-387-97450-4
und 3-540-97450-4][9] A. J. M. VAN G ASTEREN, G. T EL : Comments on “On the proof of a
distributed algorithm”: Always-true is not invariant. – Information
Processing Letters 35 (1990) 277–279. [ISSN 0020-0190][10] H. J. G ENRICH , K. L AUTENBACH , P. S. T HIAGARAJAN : Elementsof General Net Theory. – W. Brauer, ed.: Net Theory and Applications. Proceedings of the Advanced Course on General Net Theory ofProcesses and Systems. Hamburg, 1979. Lecture Notes in Computer
Science 84. Springer-Verlag, 1980. 21–163. [ISBN 3-540-10001-6 und
0-387-10001-6][11] J. A. G OGUEN, J. M ESEGUER : Completeness of many-sorted equational logic. – ACM SIGPLAN Notices 16 # 7 (July 1981) 24–32.
[12] J. A. G OGUEN, J. M ESEGUER : Remarks on Remarks on Many-Sorted
Equational Logic. – Bulletin of the EATCS # 30 (October 1986) 66–73.
87

88

Literatur[13] U. H UMMERT: Algebraische Theorie von High-Level-Netzen. Dissertation. Fachbereich 20 (Informatik) der Technischen Universität Berlin, 1989.
[14] K. J ENSEN : Coloured Petri Nets 1. Springer-Verlag, 1992. [ISBN3-540-55597-9 und 0-387-55597-9][15] K. J ENSEN : Coloured Petri Nets 2. Springer-Verlag, 1995. [ISBN3-540-58276-2 und 0-387-58276-2][16] E. J ESSEN, R. VALK : Rechensysteme: Grundlagen der Modellbildung.
Springer-Verlag, 1987. [ISBN 3-540-16383-2 und 0-387-16383-2][17] E. K INDLER : Invariants, composition, and substitution. – Acta informatica 32 (1995) 299–312. [ISSN 0001-5903][18] E. K INDLER , H. V ÖLZER : Flexibility in Algebraic Nets. InformatikBericht 89. Humboldt-Universität zu Berlin, Institut für Informatik,
1997.
[19] S. L ANG : Algebra.
0-201-55540-9]

[3rd

ed.]

Addison-Wesley,

1993.

[ISBN

[20] K. L AUTENBACH : Exakte Bedingungen der Lebendigkeit für eine
Klasse von Petri-Netzen. BMFT-GMD-82. Bonn, Gesellschaft für Mathematik und Datenverarbeitung, 1973.
[21] K. L AUTENBACH : Linear Algebraic Techniques for Place/Transition
Nets. – W. Brauer, W. Reisig, G. Rozenberg, eds.: Petri Nets: Central
Models and Their Properties. Advances in Petri Nets 1986, Part I.
Proceedings of an Advanced Course. Bad Honnef, September 1986.
Lecture Notes in Computer Science 254. Springer-Verlag, 1987. 142–
167. [ISBN 3-540-17905-4 und 0-387-17905-4][22] S. M AC L ANE : Categories for the Working Mathematician. [2nd ed.]
Graduate Texts in Mathematics 5. Springer-Verlag, 1998. [ISBN0-387-98403-8][23] G. M EMMI , G. R OUCAIROL : Linear Algebra in Net Theory. – W. Brauer, ed.: Net Theory and Applications. Proceedings of the Advanced
Course on General Net Theory of Processes and Systems. Hamburg, 1979. Lecture Notes in Computer Science 84. Springer-Verlag,
1980. 213–223. [ISBN 3-540-10001-6 und 0-387-10001-6][24] J. M ESEGUER , J. A. G OGUEN : Initiality, induction, and computability. – M. Nivat, J. C. Reynolds, eds.: Algebraic methods in semantics.
Cambridge University Press, 1985. 459–541. [ISBN 0521267935][25] J. M ESEGUER , U. M ONTANARI : Petri Nets Are Monoids. – Information and Computation 88 (1990) 105-155. [ISSN 0890-5401]

Literatur

89[26] B. M ÖLLER : Lineare Invarianten algebraischer Petrinetze. Studienarbeit. Universität Hamburg, 1999.
[27] J PADBERG : Abstract Petri Nets: Uniform Approach and Rule-Based
Refinement. Dissertation. TU Berlin, 1996.
[28] C. A. P ETRI : Nets, time and space. – Theoretical Computer Science
153 (1996) 3–48. [ISSN 0304-3975][29] W. R EISIG : Petri nets with individual tokens. – Theoretical Computer
Science 41 (1985) 185–213. [ISSN 0304-3975][30] W. R EISIG : Petri nets and algebraic specifications. – Theoretical Computer Science 80 (1991) 1–34. [ISSN 0304-3975][31] K. S CHMIDT: Symbolische Analysemethoden für algebraische Petrinetze. Berlin, Dieter Bertz Verlag, 1996. [ISBN 3-929470-54-3][32] H. S CHUBERT: Kategorien I. Heidelberger Taschenbücher 65.
Springer-Verlag, 1970.
[33] J. VAUTHERIN : Parallel systems specifications with coloured Petrinets and algebraic specifications. – G. Rozenberg, ed.: Advances inPetri Nets 1987. Lecture Notes in Computer Science 266. SpringerVerlag, 1987. 293–308. [ISBN 3-540-18086-9 und 0-387-18086-9][34] H. V ÖLZER : Verifikation Verteilter Algorithmen mit Algebraischen
Netzen. Diplomarbeit. Humboldt-Universität zu Berlin, Institut fürInformatik, 1995.
[35] W. W ECHLER : Universal Algebra for Computer Scientists. EATCS
Monographs on Theoretical Computer Science 25. Springer-Verlag,
1992. [ISBN 3-540-54280-9 und 0-387-54280-9]

90LiteraturIndex
Auswertung, 12
auswertungsverträglich, 48
Axiom, 23[ . ], 15[ . ]s , 15
∅A , 47→E , 55∼E , 60∼ECN , 82∼ι , 77[M ], 67
[M iE , 56
[miE , 56◦, 17◦a,b,c , 17
`R , 23
T (X)≡GΣ , 26{|x|}, 47{|x1 , . . ., xk }| , 47←−, 67, 70

Belegung, 12
Beweis, 23
beweisbar, 23
carrier set, 11
χA , 47
closure, 23clR (A), 23(CN , M0 )-Netzsysteme, 57
colour, 52
complete, 29
D, 66
doppelte Substition, 24
Dp,t , 66

Y(A1 )Σ0 , 34
(A1 )SPEC 0 , 35
Abb(A, B), 7
ableitbar, 23
Ableitung, 23
Abschluß, 23addierbar, 47
aktiviert, 55
Algebra, 11
Σ-Algebra, 11
SPEC -Algebra, 22
SPECF -Algebra, 38
trivial, 11
algebraische Gewichtung, 67
algebraische Inzidenzmatrix, 66
algebraische Spezifikation, 21
algebraisches Netz, 62
Alg(Σ), 18
Alg(SPEC ), 32
always-true, 58
AN , 62
Anfangsmarkierung, 57
arc, 52
Argumentsorte, 7
auf einer Stelle liegende Marken,
54→E , 55∼E , 60
echter Unterterm, 9∼ECN , 82
ECN -zulässig, 70
einfache Substition, 24
Einschränkung, 35, 45
einer Belegung, 13
einer Substitution, 10
Element, 46
Elementanzahl, 46
Elementarschritt, 56
endlich agierender Schritt, 56
endliche gewichtete Menge, 46
Endlichkeitsspezifikation, 38
Endlichkeitsterm, 38
Ereignis, 54
erreichbar, 56
Erweiterung
einer Endlichkeitsspezifikation, 45
einer Gleichungsspezifikation, 34
einer Signatur, 34
konservativ, 3591

92

vorsichtig, 35, 45
eval, 12evals , 12
Farbmenge, 52
final, 18
in C, 19
Σ-Algebra, 12, 19
SPEC -Algebra, 32
SPECF -Algebra, 43
Fins , 11FinΣ , 11
Folgerung, 23
formale Gleichung, 21
formaler Beweis, 23
Fp,t , 63
frei
Σ-Algebra, 19
SPEC -Algebra, 32
Ft,p , 63G, 22
gefärbtes Netz, 52
gefärbtes Netzsystem, 57
generiert, 13
gesättigt, 26
gewichtete Menge, 46leer, 46
Gewichtung, 46, 66
algebraisch, 67
Gleichung, 21
Gleichungsspezifikation, 21
Grundterm, 8Gruppekommutativ, 29
GS,Ω,Xi , 22
gültig, 21
Halbgruppe mit neutralem Element, 34
hom Mengen, 17
homC (a, b), 17
Homomorphismus, 13, 22
Identität, 17
Induktionsbereich, 57, 59
induktive Invariante, 58
initial, 18

Index

in C, 19
Σ-Algebra, 12, 19
SPEC -Algebra, 32
interpretA , 13, 63, 76
Interpretation, 63
interpretierbar, 63
Invariante, 57–59, 82
induktiv, 58
linear, 65, 71
Inverses, 17
Inzidenzmatrix, 65
algebraisch, 66
ι, 77∼ι , 77
isomorph, 17
Isomorphismus, 17
kanonische Abbildung, 15, 66
Kante, 52
Kantenbeschriftung, 52
Kategorie, 17
kommutative Gruppe, 29
Komposition, 14, 17
Kongruenz, 15, 22, 27
konservative Erweiterung, 35
Konstante, 11
Konstantensymbol, 7
korrekt, 25, 39
Länge eines Beweise, 23leere gewichtete Menge, 46leere Multimenge, 47
lineare Invariante, 65
für ECN , 71
linke Seite, 21
lokal-endlich agierender Schritt,56[M ], 67
M(A), 46
M± (A), 46
M±
fin (A), 46
MCN , 54
Marke, 54
Markierung, 54[M iE , 56
[miE , 56
Mehrfachkante, 53IndexM±
F (A), 48
M±
f (A), 48
Mfin (A), 46
minimales Variablensystem, 9M±M1 • (A2 ), 50±
M•M2 (A1 ), 50
Modell, 22, 38
Morphismus, 17Multimenge, 46leer, 47N, 7n-faches Element, 46
Nachfolgemarkierung, 54–55
Nebenläufigkeit, 52
Netz
algebraisch, 62
gefärbt, 52
Netzsystem
gefärbt, 57
nichtnegativ gewichtete Menge,46
Objekt, 17
Operation, 11
Operationssymbol, 7P(x), 18
place, 52, 62
Potenzmenge, 18
Prä-Schritt, 54
Prämisse, 23
Quotient, 15, 22
R, 23, 24`R , 23
rechte Seite, 21
Reflexivität, 24
Regelsystem, 23
Restriktion
einer Belegung, 13
einer Substitution, 10
Rfin , 39
Rfin
SPEC , 39
RS,Ω,Ξ , 24
S-Invariante, 65

93schalten, 54
Schaltmodus, 52
Schaltregel, 54
Schlußregel, 22
Schritt, 55
endlich agierend, 56
lokal-endlich agierend, 56
Seite (einer algebraische Gleichung), 21
Σ-Algebra
final, 12, 19
frei, 19
initial, 12, 19
trivial, 11
Σ-generiert, 13
Signatur, 7sort, 7, 22
Sorte, 7
Argumentsorte, 7
Wertsorte, 7
sortX , 9sound, 25
Spalte, 66
SPEC -Algebra, 22
final, 32
frei, 32
initial, 32SPEC cl , 32
SPECF -Algebra, 38
final, 43
Spezifikation
algebraisch, 21
Gleichungs-, 21
Stelle, 52, 62
Stellen-Transitions-Netz, 65
Subsignatur, 34
Subspezifikation, 34, 45
Substitution, 9doppelt, 24
einfach, 24
Substitutionsauswertung, 9Summe einer Familie von gewichteten Mengen, 47
supp, 46
support, 46
Symmetrie, 2494Term, 7–8
term(a), 8
Termalgebra, 11
Tiefe, 8TΩ , 8TΩ,s , 8TΩ,s (X), 8
TΩ (X), 8
Träger, 46
Trägermenge, 11Trans E , 54–55
Transition, 52, 62
Transitionssystem, 54
Transitivität, 24
triviale Algebra, 11triviale Σ-Algebra, 11TΣ , 11TΣ (X), 11
TSPEC , 32
TSPEC (X), 28
TSPEC ,s (X), 28
unendliche gewichtete Menge, 46
Universum, 18
Unterkategorie, 32
voll, 32
Unterterm, 9var(T ), 9
Variable, 7
Variablensystem, 7
einer formalen Gleichung, 21
minimal, 9vars (T ), 9
verträglich, 49
volle Unterkategorie, 32
vollständig, 29
vorsichtige Erweiterung, 35, 45
Wertsorte, 7Wort, 7{|x|}, 47{|x1 , . . ., xk }| , 47←−, 67, 70
Y

Zeile, 66

Indexzulässig, 70
ECN -zulässig, 70
Zustand, 54
Zustandsübergangsrelation, 54

Ich erkläre hiermit, daß ich die vorliegende Arbeit selbständig erstellt undkeine anderen als die angegebenen Hilfsmittel und Quellen verwendet habe.

Hamburg, den 1. Oktober 1999