Was bisher geschah
Modellierung von
Aussagen durch logische Formeln
Daten durch Mengen, Multimengen, Folgen, Sprachen
Zusammenhängen und Eigenschaften von Elementen von Mengen
durch Relationen
Zuordnungen zwischen Elementen von Mengen durch Funktionen
im Zusammenhang in (algebraischen) Strukturen
Signatur Σ = (ΣF , ΣR )
definiert Symbole und Stelligkeiten / Typen (Syntax)
Σ-Struktur A = (A, J·KA ) mit
(Semantik)
Menge A 6= ∅ (Trägermenge)
(Individuenbereich, Universum)
Funktionen: ∀(f , n) ∈ ΣF : Jf KA : An → A
(Bedeutung der Funktionssymbole)
Relationen: ∀(R, n) ∈ ΣR : JRKA ⊆ An
(Bedeutung der Relationssymbole)
211
Wiederholung Signaturen
Definition der Symbole für Individuen (Konstanten) sowie deren
Eigenschaften und Beziehungen (Relationen, Funktionen)
Signatur Σ = (ΣF , ΣR ) mit Mengen
ΣF = {(f , n) | n ∈ } von Funktionssymbolen (mit Stelligkeit)
ΣR = {(R, n) | n ∈ } von Relationssymbolen (mit Stelligkeit)
N
N
Beispiele:
I
Σ = (ΣF , ΣR ) mit
√
ΣF = {(+, 2), ( , 1), (1, 0), (7, 0)} und
ΣR = {(≤, 2), (prim, 1)}
I
Σ = (ΣF , ΣR ) mit
ΣF = {(Mutter-von, 1)} und
ΣR = {(weiblich, 1), (verheiratet, 2), (Kind-von, 2), (=, 2)}
I
Σ = (ΣF , ΣR ) mit
ΣF = {(☼, 2), ($, 2)} und ΣR = ∅
212
Wiederholung Strukturen – Beispiel Halbring
klassische Definition (Menschen-lesbar):
Eine algebraische Struktur (A, ☼, $) heißt genau dann Halbring, wenn sie
die folgenden Bedingungen erfüllt:
I
I
(A, ☼) und (A, $) sind Halbgruppen und
$ ist distributiv über ☼
formale Definition (maschinell zu verarbeiten):
Signatur Σ = (ΣF , ΣR ) mit
Axiome (Anforderungen)
(
∧ (
∀x∀y ∀z
∧ (
∧ (
prominente Halbringe:
A = ( , J·KA )
B = (2 , J·KB )
C = ({0, 1}, J·KC )
D = (2M , J·KD )
∗
E = (2{a,b} , J·KE )
F = ( ∪ {+∞}, J·KF )
N
Z
R
mit
mit
mit
mit
mit
mit
ΣF = {(☼, 2), ($, 2)}, ΣR = {(=, 2)}
x☼(y ☼z) = (x☼y )☼z
)
x$(y $z) = (x$y )$z
)
x$(y ☼z) = (x$y )☼(x$z) )
(x☼y )$z = (x$z)☼(y $z) )
J☼KA = +
J☼KB = +
J☼KC = max
J☼KD = ∪
J☼KE = ∪
J☼KF = min
und
und
und
und
und
und
J$KA = ·
J$KB = ·
J$KC = min
J$KD = ∩
J$KE = ◦
J$KF = +
213
Mehrsortige Strukturen
Modellierung von Strukturen mit verschiedenen Sorten (Trägermengen,
Typen) = {Si | i ∈ I } von Elementen
Beispiele mehrsortiger Strukturen:
S
I
Vektorraum mit
Sorten: Skalar, Vektor
Operationen, z.B. smult: Skalar × Vektor → Vektor
Relationen, z.B. gleichlang ⊆ Vektor × Vektor
I
Sorten: Menschen, Bücher
Relation: A ⊆ Menschen × Bücher
wobei (m, b) ∈ A gdw. m ist Autor von b
I
Sorten: Menschen, , Orte
Relation: B ⊆ Menschen ×
× Orte
wobei (m, j, o) ∈ B gdw. m wurde im Jahr j in o geboren
I
Stapel (von Elementen, z.B. Bücher, Teller, Zahlen, . . . ) mit
Sorten: Bool, Element, StapelhElementi
(polymorph)
Operationen, z.B.
push: StapelhElementi× Element → StapelhElementi
Relationen, z.B. ist-leer ⊆ StapelhElementi
N
N
214
Mehrsortige Signaturen
S
mehrsortige Signatur Σ = ( , ΣF , ΣR ) besteht aus
S
ΣF
ΣR
= {Si | i ∈ I }: Menge der Sorten
: Menge der Funktionssymbole
mit Argument- und Ergebnistypen (f :
: Menge der Relationssymbole
mit Argumenttypen (s ⊆ ∗ )
S∗ → S)
S
Beispiel: Bücher mit Autoren und Erscheinungsjahr
Z
Sorten B (Bücher), P (Personen), (Jahreszahlen),
2B (Mengen von Büchern), also = {B, P, , 2B }
Funktionssymbole (mit Argument-und Ergebnistypen):
:B →
Erscheinungsjahr
erstes-Buch-von
:P
→B
ΣF =
gemeinsame-Buecher-von : P 2 → 2B
S
Z
Z
Relationen (mit Argumenttypen):
ist-Autor-von
ΣR =
sind-Coautoren
⊆P ×B
⊆ P2
215
Mehrsortige Σ-Strukturen
S
gegeben: mehrsortige Signatur Σ = ( , ΣF , ΣR )
S
mehrsortige Σ-Struktur A = ({AS | S ∈ }, J·KA ) mit
S
I
für jede Sorte S ∈ eine nichtleere Menge AS
(Trägermenge, Universum der Sorte)
I
für jedes Funktionssymbol f : S1 . . . Sn → S
eine Funktion Jf KA : AS1 × . . . × ASn → AS
I
für jedes Relationssymbol R ⊆ S1 × . . . × Sn
eine Relation JRKA ⊆ AS1 × . . . × ASn
216
Mehrsortige Strukturen in der Informatik
Programmierung:
Datentypen (Sorten) int, float, bool, string
mit Operationen (Signatur), z.B.:
floor
duplicate
length
>
:
:
:
:
float
string × int
string
float × float
→
→
→
→
int
string
int
bool
Datenbanken:
Tabellen sind extensionale Darstellungen (meist) mehrsortiger
Relationen
217
Formale Darstellung algebraischer Strukturen
(abstrakte Algebra, abstrakter Datentyp, ADT)
I
I
I
I
I
S
Signatur Σ = ( , ΣF , ΣR ) mit
S
Menge von Sortensymbolen,
Menge ΣF von Funktionssymbolen
mit Stelligkeit / Typdeklaration
Menge ΣR von Relationssymbolen
mit Stelligkeit / Typdeklaration
Menge von Axiomen beschreibt Zusammenhänge zwischen
den Symbolen
(meist prädikatenlogische Formeln, Gleichungen)
ADT zur Definition von Software-Schnittstellen:
Festlegung der
Syntax in Sorten und Signatur (z.B. Java-Interfaces)
Semantik (Anforderungen an Implementierung) in Axiomen
218
Terme
Beispiele: für (einsortige) Signatur Σ = (ΣF , ΣR ) mit
ΣF = {(3, 0), (5, 0), (+, 2), (·, 2)} und ΣR = {(>, 2)} und Menge
= {x, y , z} von Variablen
X
I
Ausdrücke 3 + x, 5, y , ((y + 5) · (3 · x)) + x sind korrekt aus
Symbolen aus ΣF und
zusammengesetzt
I
Ausdrücke 3x+, +5, 3(x + y ), (3x5) + z sind nicht korrekt aus
Symbolen aus ΣF und
zusammengesetzt
X
X
Definition (induktiv)
X
Die Menge Term(ΣF , ) aller Terme über der (funktionalen) Signatur
ΣF mit Variablen aus der Menge
ist definiert durch:
IA: Jede Variable x ∈
X
X ist ein Term.
(
X ⊆ Term(ΣF , X))
IS: Sind (f , n) ∈ ΣF (f ist n-stelliges Funktionssymbol) und t1 , . . . , tn
Terme aus Term(ΣF , ),
dann ist f (t1 , . . . , tn ) ein Term aus Term(ΣF , ).
X
X
verschiedene Darstellungen von Termen möglich,
z.B. Baum, Infix-, Präfix-, Postfixform
219
Grundterme
Terme ohne Variablen heißen Grundterme.
Term (ΣF , ∅) ist Menge aller Grundterme über Signatur ΣF
Beispiele:
für ΣF = {(f , 1), (g , 2), (h, 2), (c, 0)} und = {x, y , z} gilt
c ∈ Term(ΣF , ∅) ⊆ Term(ΣF , )
(Grundterm)
(kein Grundterm)
z ∈ Term(ΣF , ), aber z 6∈ Term(ΣF , ∅)
f (c) ∈ Term(ΣF , ∅) ⊆ Term(ΣF , )
h(f (x), c) ∈ Term(ΣF , ), aber h(f (x), c) 6∈ Term(ΣF , ∅)
f 6∈ Term(ΣF , ), h(c) 6∈ Term(ΣF , ), x(c) 6∈ Term(ΣF , )
X
X
X
X
X
X
X
X
Warum gilt für alle Signaturen ΣF ohne Konstantensymbole
Term (ΣF , ∅) = ∅?
(ÜA)
220
Spezialfall: aussagenlogische Formeln
Terme über der funktionalen Signatur
ΣF = {(t, 0), (f, 0), (¬, 1), (∨, 2), (∧, 2), (→, 2), (↔, 2)}
mit Aussagenvariablen aus P
sind genau alle aussagenlogischen Formeln ϕ ∈ AL(P)
Für diese Signatur ΣF gilt also AL(P) = Term(ΣF , P)
Beispiele: für P = {a, b, c, d}
I
a ∨ (c → b) ∈ AL(P) = Term(ΣF , P)
I
(b → t) ∧ (b → f) ∈ AL(P) = Term(ΣF , P)
I
(a¬b) ∧ (b → f) 6∈ AL(P) = Term(ΣF , P)
I
(f → t) ∈ AL(P) = Term(ΣF , P),
sogar (f → t) ∈ AL(∅) = Term(ΣF , ∅)
221
Mehr Beispiele
I
I
Q
für ΣF = {(+, 2), (−, 2), (·, 2), (/ 2)} ∪ {(q, 0) | q ∈ } ist
Term(ΣF , ∅) die Menge aller arithmetischen Ausdrücke
(Terme) mit rationalen Zahlen (z.B. 3/5+1/4),
Term(ΣF , {a, b, c}) die Menge aller arithmetischen Ausdrücke
(Terme) mit rationalen Zahlen und Variablen aus der Menge
{a, b, c} (z.B. (3 · a) + ((2 · b)/c)),
ΣF = {(apfel, 0), (banane, 0), (kirsche, 2), (pflaume, 2)}
I
I
I
I
apfel ∈ Term(ΣF , ∅), Grundterm
kirsche (x, pflaume(y , banane)) ∈ Term(ΣF , {x, y , z})
kein Grundterm
banane(apfel(pflaume, kirsche(pflaume))) 6∈ Term(ΣF ,
pflaume(apfel, kirsche(banane, apfel)) ∈ Term(ΣF , ∅)
X)
222
Größe von Termen
Für jeden Term t ∈ Term(ΣF ,
definiert durch:
IA: falls t = x ∈
X) ist seine Größe size(t) (induktiv)
X, dann size(t) = 1
IS: falls t = f (t1 , . . . , tn ), dann
size(t) = 1 +
n
X
size(ti )
i=1
Beispiele für ΣF = {(f , 1), (g , 2), (h, 2), (c, 0)} und
I
size(c) = 1
I
size(z) = 1
I
size(f (c)) = 2
I
size(h(f (x), c)) = 4
X = {x, y , z}:
223
Menge aller Variablen in einem Term
X
Für jeden Term t ∈ Term(ΣF , ) ist die Menge var(t) aller in t
vorkommenden Variablen (induktiv) definiert durch:
IA: falls t = x ∈
X (Variable), dann var(t) = {x}
IS: falls t = f (t1 , . . . , tn ) mit (f , n) ∈ ΣF , dann
var(t) = var(t1 ) ∪ · · · ∪ var(tn )
Beispiel: Für t = f (g (x, a), g (f (a, y ), x)) gilt var(t) = {x, y }
224
Wert von Grundtermen in Strukturen
gegeben: funktionale Signatur ΣF = {(f , n) | n ∈
Σ-Struktur A = (A, J·KA )
N}
Definition (induktiv)
Der Wert des ΣF -Grundtermes t = f (t1 , . . . , tn ) ∈ Term(ΣF , ∅)
in der ΣF -Struktur A = (A, J·KA ) ist
JtKA = Jf KA (Jt1 KA , . . . , Jtn KA )
Fehlt hier der Induktionsanfang?
nein, ist als Spezialfall enthalten:
Für Terme t = c mit (c, 0) ∈ ΣF (Konstante) gilt JtKA = JcKA
(Bedeutung der Konstante c in A, gegeben in Definition von A)
225
Beispiel
Signatur Σ = (ΣF , ΣR ) mit
ΣF = {(apfel, 0), (banane, 0), (kirsche, 2), (pflaume, 2)}
ΣR = {(rettich, 1), (tomate, 2)}
s = apfel t = pflaume(apfel, kirsche(banane, apfel))
Σ-Struktur A = (A, J·KA ) mit
A =
N
JapfelKA = 5
für alle (x, y ) ∈
für alle (x, y ) ∈
A2 :
A2 :
JbananeKA = 3
JkirscheKA (x, y ) = x + y
JpflaumeKA (x, y ) = x · y
JrettichKA = {0, . . . , 10}
JtomateKA = {(2n, n) | n ∈
JsKA = JapfelKA = 5 JtKA = . . .
N}
226
Weiteres Beispiel
s = apfel t = pflaume(apfel, kirsche(banane, apfel))
Σ-Struktur B = (B, J·KB ) mit
B = {0, 1}
JapfelKB = 0
für alle (x, y ) ∈
B 2:
JbananeKB = 1
JkirscheKB (x, y ) = min(x, y )
für alle (x, y ) ∈ B 2 : JpflaumeKB (x, y ) = max(x, y )
JrettichKB = {0}
JtomateKB = {(0, 0), (0, 1), (1, 1)}
JsKB = JapfelKB = 0,
JtKB = . . .
227
Weiteres Beispiel
s = apfel t = pflaume(apfel, kirsche(banane, apfel))
Σ-Struktur C = (C , J·KC ) mit
C
= Menge aller Studenten hier
JapfelKC = Student hinten rechts
für alle (x, y ) ∈
C 2:
JbananeKC = Student daneben
JkirscheKC (x, y ) = x
für alle (x, y ) ∈ C 2 : JpflaumeKC (x, y ) = y
JrettichKC = {x ∈ C | x ist blond}
JtomateKC = {(x, y ) ∈ C 2 | x hilft y }
JsKC = JapfelKC = Student hinten rechts
JtKC = . . .
228
Noch ein Beispiel
s = apfel t = pflaume(apfel, kirsche(banane, apfel))
Σ-Struktur D = (D, J·KD ) mit
D = 2N
JapfelKD = ∅
JbananeKD =
N
für alle M, N ∈ D: JkirscheKD (M, N) = M ∩ N
für alle M, N ∈ D: JpflaumeKD (M, N) = M ∪ N
JrettichKD = {M ⊆
N | |M| ∈ N}
JtomateKD = {(M, N) ∈ D 2 | M ⊆ N}
JsKD = JapfelKD = ∅,
JtKD = . . .
229
Äquivalenz von Grundtermen in einer Struktur
ΣF -Grundterme s, t ∈ Term(ΣF , ∅) mit JsKA = JtKA heißen
äquivalent in A (s ≡A t).
In den Beispielen oben gilt
s 6≡A t
s
≡B
t
s
6≡C
t
s ≡D t
schon bekannter Spezialfall:
semantische Äquivalenz aussagenlogischer Formeln
(ohne Aussagenvariablen)
230
© Copyright 2024 ExpyDoc
