Syntax zu Semantik Syntax
Kalkül
Regelsystem mit dem sich Formeln aus anderen systematisch herleiten lassen.
Formale Beweise.
Theorie (In der Logik)
Menge von Formeln die aus einer Menge Axiome
A \small \mathcal A A
Dann spricht man von einer axiomatischen Theorie.
Semantik
Wahrheit, Gültigkeit, Interpretation, Modell
Intendierte Semantik
Meaning function
M : T ↦ ω \mathcal{M}: \mathcal{T} \mapsto \omega M : T ↦ ω
M : E N V × T ↦ ω \mathcal{M}: E N V \times \mathcal{T} \mapsto \omega M : EN V × T ↦ ω
E N V ENV EN V ist die Menge aller I I I
Interpretation
Speicherbelegung, Variablenbelegung, Environments
I : I V S ↦ D I: I V S \mapsto D I : I V S ↦ D
zB
I : { x ‾ , y ‾ , z ‾ , … } ↦ ω
I:\{\underline{\mathrm{x}}, \underline{\mathrm{y}}, \underline{z}, \ldots\} \mapsto \omega
I : { x , y , z , … } ↦ ω
Modellstrukturen 💡
Für
M \mathcal M M
bei Zahlenbegriffen, braucht man zusätzlich zur Menge
ω \omega ω
noch eine Modellstruktur wie zB
N , Z \small \N, \Z N , Z
.
Modellstruktur D \mathcal D D
sind Abstrakte Datentypen.
Allgemeines semantisches Konzept um zu
bestimmen worauf sich Dinge beziehen
.
Bestimmt Mengen an Funktionen für die Symbole.
Alle Funktionen sind total.
Σ ( D ) = ⟨ D ; P , K , F ⟩ \Sigma(\mathcal{D})=\langle D ; P, K, F\rangle Σ ( D ) = ⟨ D ; P , K , F ⟩
D D D
P P P P : D n ↦ { f , t } P: D^{n} \mapsto\{\mathbf{f}, \mathbf{t}\} P : D n ↦ { f , t } (Wahrheitswerte)
K K K K ⊆ D K \subseteq D K ⊆ D
F F F F : D n ↦ D F:D^{n} \mapsto D F : D n ↦ D
Beispiele Ganze Zahlen
Z = { … , − 2 , − 1 , 0 , 1 , 2 , … } Z=\{\ldots,-2,-1,0,1,2, \ldots\} Z = { … , − 2 , − 1 , 0 , 1 , 2 , … }
Z = ⟨ Z ; { < } , Z , { + , − , ∗ } ⟩
\mathbb{Z}=\langle Z ;\{<\}, Z,\{+,-, *\}\rangle
Z = ⟨ Z ; { < } , Z , { + , − , ∗ }⟩
Natürliche Zahlen
ω = { 0 , 1 , 2 , … } \omega=\{0,1,2, \ldots\} ω = { 0 , 1 , 2 , … }
N = ⟨ ω ; { < } , { 0 , 1 } , { + , − ˙ , ∗ } ⟩
\mathbb{N}=\langle\omega ;\{<\},\{0,1\},\{+, \dot{-}, *\}\rangle
N = ⟨ ω ; { < } , { 0 , 1 } , { + , − ˙ , ∗ }⟩
Ident zu
Z \Z Z
x − ˙ y = { x − y f u ¨ r x ≥ y 0 f u ¨ r x < y
x ~\dot{-}~y= \begin{cases}x-y & \text { für } x \geq y \\ 0 & \text { für }
x<y\end{cases}
x − ˙ y = { x −
y
0 f u ¨ r x ≥
y
f u ¨ r x <
y
Binäre Stacks
S = ⟨ S ; { ist 0 ? , ist1 ? , istleer? } , { ε } , { push 0 , push1, pop } ⟩
\mathbb{S}=\langle S ;\{\text { ist } 0 ?, \text { ist1 } ? \text {, istleer?
}\},\{\varepsilon\},\{\text { push } 0 \text {, push1, pop }\}\rangle
S = ⟨ S ; { ist 0 ? , ist1 ? , istleer? } , { ε } , { push 0 , push1, pop }⟩
Domäne
Stacks dargestellt durch
S = { 0 ‾ , 1 ‾ } ∗ S=\{\underline{0}, \underline{1}\}^{*} S = { 0 , 1 } ∗
Wichtig: Domäne bestimmt nicht die Struktur. Andere Datentypen über der selben Domäne wären Binärezahlen oder
Binärstrings.
Prädikate
istleer? ( s ) ⟺ s = ε ist0? ( s ) ⟺ es gibt ein s ′ sodass s = 0 ‾ s ′ ist1? ( s ) ⟺ es gibt ein s ′ sodass s = 1 ‾ s ′
\begin{aligned}\text { istleer?}(s) & \Longleftrightarrow s=\varepsilon \\\text {
ist0?}(s) & \Longleftrightarrow \text { es gibt ein } s^{\prime} \text { sodass }
s=\underline{0} s^{\prime} \\\text { ist1?}(s) & \Longleftrightarrow \text { es gibt ein
} s^{\prime} \text { sodass } s=\underline{1} s^{\prime}\end{aligned}
istleer? ( s ) ist0? ( s ) ist1? ( s ) ⟺ s = ε ⟺ es gibt ein s ′ sodass s = 0 s ′ ⟺ es gibt ein s ′ sodass s = 1 s ′
Funktionen
push 0 ( s ) = 0 ‾ s push 1 ( s ) = 1 ‾ s pop ( s ) = { ε f u ¨ r s = ε s
′
f u ¨ r s = 0 ‾ s
′
oder s = 1 ‾ s
′
\begin{aligned}\operatorname{push} 0(s) &=\underline{0} s \\\operatorname{push} 1(s)
&=\underline{1} s \\\operatorname{pop}(s) &= \begin{cases}\varepsilon & \text {
für } s=\varepsilon \\s^{\prime} & \text { für } s=\underline{0} s^{\prime} \text { oder
} s=\underline{1} s^{\prime}\end{cases}\end{aligned}
push 0 ( s ) push 1 ( s ) pop ( s ) = 0 s = 1 s = {
ε
s
′
f
u
¨
r
s
=
ε
f
u
¨
r
s
=
0
s
′
oder
s
=
1
s
′
Familie
Fam X = ⟨ D X ; P X , K X , F X ⟩
\operatorname{Fam} \mathbf{X}=\left\langle D_{X} ; P_{X}, K_{X}, F_{X}\right\rangle
Fam X = ⟨ D
X
; P
X
, K
X
, F
X
⟩
D X = Personen X
(Menge der Mitglieder der Familie X)
P X = { Geschwister, Onkel, weiblich, m a ¨ nnlich } K X = {
Abdul, Berta, Chris, Dorlan, Ege,...
} F X = { Vater, Mutter }
\begin{aligned}&D_{X}=\text { Personen}_{X} \text {(Menge der Mitglieder der Familie X)
} \\&P_{X}=\{\text { Geschwister, Onkel, weiblich, männlich }\} \\&K_{X}=\{\text {
Abdul, Berta, Chris, Dorlan, Ege,... }\} \\&F_{X}=\{\text { Vater, Mutter
}\}\end{aligned}
D
X
= Personen
X
(Menge der Mitglieder der Familie X)
P
X
= {
Geschwister, Onkel, weiblich, m
a ¨ nnlich }
K
X
= {
Abdul, Berta, Chris, Dorlan, Ege,...
}
F
X
= { Vater, Mutter }
Signaturen Signatur Σ ( D ) \Sigma(\mathcal{D}) Σ ( D ) von Modellstruktur D \mathcal{D} D
bestimmt Alphabet der Sprache, die Bezug auf Gegenstände in
D \mathcal D D
K S ( D ) K S(\mathcal{D}) K S ( D )
P S n ( D ) , F S n ( D ) PS_{n}(\mathcal{D}), FS_{n}(\mathcal{D}) P S n ( D ) , F S n ( D ) n n n
Beispiele Ganze Zahlen
Σ ( Z ) : \Sigma(\mathbb{Z}): Σ ( Z ) :
P S 2 ( Z ) = { ≤ } P S n ( Z ) = { } f u ¨ r n ≠ 2 K S ( Z ) = { … , − 2 ‾ , − 1 ‾ , 0 ‾ , 1 ‾ , 2 ‾ , … } F S 2 ( Z ) = { + ‾ , − ‾ , ∗ ‾ } F S n ( Z ) = { } f u ¨ r n ≠ 2
\begin{aligned}&P S_{2}(\mathbb{Z})=\{\leq\} \\& P S_{n}(\mathbb{Z})=\{\} \text {
für } n \neq 2 \\&K S(\mathbb{Z})=\{\ldots, \underline{-2}, \underline{-1},
\underline{{0}}, \underline{1}, \underline{2}, \ldots\} \\&F
S_{2}(\mathbb{Z})=\{\underline +, \underline -, \underline{*}\} \\& F
S_{n}(\mathbb{Z})=\{\} \text { für } n \neq 2\end{aligned}
P
S
2 ( Z ) = { ≤ }
P
S
n
( Z ) = { } f u ¨ r n = 2
K
S
( Z ) = { … , − 2 , − 1 , 0 , 1 , 2 , … }
F
S
2 ( Z ) = { + , − , ∗ }
F
S
n
( Z ) = { } f u ¨ r n = 2
Natürliche Zahlen
P S 2 ( N ) = { ≤ } P S_{2}(\mathbb{N})=\{\leq\} P S 2 ( N ) = { ≤ }
P S n ( N ) = { } f u ¨ r n ≠ 2
P S_{n}(\mathbb{N})=\{\} \text { für } n \neq 2
P S n ( N ) = { } f u ¨ r n = 2
K S ( N ) = { 0 ‾ , 1 ‾ }
K S(\mathbb{N})=\{\underline{0}, \underline{1}\}
K S ( N ) = { 0 , 1 }
F S 2 ( N ) = { + ‾ , − ˙ ‾ , ∗ ‾ }
F S_{2}(\mathbb{N})=\{\underline +, \underline{\dot{-}}, \underline{{*}}\}
F S 2 ( N ) = { + , − ˙ , ∗ }
F S n ( N ) = { } f u ¨ r n ≠ 2
F S_{n}(\mathbb{N})=\{\} \text { für } n \neq 2
F S n ( N ) = { } f u ¨ r n = 2
Binäre Stacks
P S 1 ( S ) = { ist0? ‾ , ist1? ‾ , istleer? ‾ } P S n ( S ) = { } f u ¨ r n > 1 K S ( S ) = { ε ‾ } F S 1 ( S ) = { push0 ‾ , push1 ‾ , pop ‾ } F S n ( S ) = { } f u ¨ r n > 1
\begin{aligned}&P S_{1}(\mathbb{S})=\{\underline{\text { ist0? }}, \underline{\text { ist1?
}}, \underline{\text { istleer? }}\} \\&P S_{n}(\mathbb{S})=\{\} \text { für } n>1
\\&K S(\mathbb{S})=\{\underline{\varepsilon}\} \\&F S_{1}(\mathbb{S})=\{\underline{\text
{ push0 }}, \underline{\text { push1 }}, \underline{\text { pop }}\} \\&F
S_{n}(\mathbb{S})=\{\} \text { für } n>1\end{aligned}
P
S
1 ( S ) = { ist0? , ist1? ,
istleer?
} P
S
n
( S ) = { } f u ¨ r n > 1 K S ( S ) = { ε } F
S
1 ( S ) = { push0 , push1 , pop } F
S
n
( S ) = { } f u ¨ r n > 1
Man muss hier unterscheiden zwischen
ε ‾ \underline \varepsilon ε ε \varepsilon ε
Familie
P S 1 ( FamX ) = { weiblich, m a ¨ nnlich ‾ } , P S 2 ( FamX ) = { Geschwister ‾ , Onkel ‾ } , P S n ( FamX ) = { } f u ¨ r n > 2 K S ( FamX ) = { Ahmed ‾ , Berta ‾ , Chris ‾ , Dorlan ‾ , Ege ‾ , … } F S 1 ( FamX ) = { Vater ‾ , Mutter ‾ } F S n ( FamX ) = { } f u ¨ r n > 1
\begin{aligned}&P S_{1}(\text { Fam} \text{X})=\{\underline{\text { weiblich, } \text {
männlich }}\}, \\&P S_{2}(\text { Fam} \text{X})=\{\underline{\text { Geschwister }},
\underline{\text { Onkel }}\}, \\&P S_{n}(\text { FamX })=\{\} \text { für } n>2 \\&K
S(\text { FamX })=\{\underline{\text { Ahmed }}, \underline{\text { Berta }}, \underline{\text {
Chris }}, \underline{\text { Dorlan }}, \underline{\text { Ege }}, \ldots\} \\&F S_{1}(\text
{ FamX })=\{\underline{\text { Vater }}, \underline{\text { Mutter }}\} \\& F S_{n}(\text {
FamX })=\{\} \text { für } n>1\end{aligned}
P
S
1 ( Fam X ) = {
weiblich,
m
a
¨
nnlich } , P
S
2 ( Fam X ) = {
Geschwister
, Onkel } , P
S
n
( FamX ) = { } f u ¨ r n > 2 K S ( FamX ) = { Ahmed , Berta , Chris , Dorlan , Ege , … } F
S
1 ( FamX ) = { Vater , Mutter } F
S
n
( FamX ) = { } f u ¨ r n > 1
Beispiele Arithmetische Ausdrücke
Arithmetische Ausdrücke über Modellstruktur
Z \small\Z Z
0 ‾ \small \underline 0 0 als Symbol, nicht als natürliche Zahl mit Wert gemeint.
Syntax: Additive Terme
Kontextfreie Grammatik
T = L ( G ) \mathcal{T}=\mathcal{L}(G) T = L ( G )
G = ⟨ { T } , { ( ‾ , ) ‾ , + ‾ , 0 ‾ , … , 9 ‾ } , P , T ⟩
G=\langle\{T\},\{\underline{(}, \underline{)}, \underline +, \underline{0}, \ldots, \underline{9}\},
P, T\rangle
G = ⟨{ T } , { ( , ) , + , 0 , … , 9 } , P , T ⟩
P = { T → 0 ‾ ∣ ⋯ ∣ 9 ‾ ∣ ( ‾ T + ‾ T ) ‾ }
P=\left\{T \rightarrow \underline{0}\mid\cdots\mid \underline{9} \mid \underline{(}{T} \underline{+}
T \underline{)}\right\}
P = { T → 0 ∣ ⋯ ∣ 9 ∣ ( T + T ) }
Induktive Definition
T \mathcal T T
{ 0 ‾ , … 9 ‾ } ⊆ T
\{\underline{0}, \ldots \underline{9}\} \subseteq \mathcal{T}
{ 0 , … 9 } ⊆ T
t 1 , t 2 ∈ T ⟹ ( ‾ t 1 + ‾ t 2 ) ‾ ∈ T
t_{1}, t_{2} \in \mathcal{T} \implies \underline(t_{1} \underline + t_{2}\underline) \in \mathcal{T}
t 1 , t 2 ∈ T ⟹ ( t 1 + t 2 ) ∈ T
Intendierte Semantik
Hier benötigt man zusätzlcih die Modellstruktur N \N N .
Induktive Definition für Meaning Function:
M ( 0 ‾ ) = 0 , … , M ( 9 ‾ ) = 9
\mathcal{M}(\underline{0})=0, \ldots, \mathcal{M}(\underline{9})=9
M ( 0 ) = 0 , … , M ( 9 ) = 9
M ( t 1 + ‾ t 2 ) = M ( t 1 ) + M ( t 2 )
\mathcal{M}\left(t_{1} \underline +
t_{2}\right)=\mathcal{M}\left(t_{1}\right)+\mathcal{M}\left(t_{2}\right)
M ( t 1 + t 2 ) = M ( t 1 ) + M ( t 2 ) t ∈ T t \in \mathcal T t ∈ T
Variablen Erweiterung des Beispiels
Neue Produktion:
T → x ‾ ∣ y ‾ ∣ z ‾
T \rightarrow \underline{\mathrm{x}}\mid \underline{\mathrm{y}} \mid \underline{\mathrm{z}}
T → x ∣ y ∣ z
M ( I , 0 ‾ ) = 0 , … , M ( I , 9 ‾ ) = 9
\mathcal{M}(I, \underline{0})=0, \ldots, \mathcal{M}(I, \underline{9})=9
M ( I , 0 ) = 0 , … , M ( I , 9 ) = 9
M ( I , v ) = I ( v ) \mathcal{M}(I, v)=I(v) M ( I , v ) = I ( v ) v ∈ { x ‾ , y ‾ , z ‾ , … }
v \in\{\underline{\mathrm{x}}, \underline{\mathrm{y}}, \underline{\mathrm{z}}, \ldots\}
v ∈ { x , y , z , … }
M ( I , ( t 1 ± t 2 ) ) = M ( I , t 1 ) + M ( I , t 2 )
\mathcal{M}\left(I,\left(t_{1} \pm t_{2}\right)\right)=\mathcal{M}\left(I, t_{1}\right)+\mathcal{M}\left(I,
t_{2}\right)
M ( I , ( t 1 ± t 2 ) ) = M ( I , t 1 ) + M ( I , t 2 ) t ∈ T t \in \mathcal T t ∈ T
Gleiche Syntax mit induktiver Definition
In beiden Fällen, die selbe Definition der Semantik.
Interpretation
Man kann frei wählen
M ( x ‾ ) = 1 \mathcal{M}(\underline{\mathrm{x}})=1 M ( x ) = 1 M ( x ‾ ) = 2 \mathcal{M}(\underline{\mathrm{x}})=2 M ( x ) = 2
I : { x ‾ , y ‾ , z ‾ , … } ↦ ω
I:\{\underline{\mathrm{x}}, \underline{\mathrm{y}}, \underline{z}, \ldots\} \mapsto \omega
I : { x , y , z , … } ↦ ω
Hierarchisierung Zuvor keine Hierarchisierung von Operatoren (welcher Vorrang hat) wegen Klammern.
Hierarchie: (Ziffer → Nummer → Term)
T T T
N N N
Z Z Z
Syntax
T = L ( G ) \mathcal{T}=\mathcal{L}(G) T = L ( G )
G = ⟨ { T , Z , N } , { ( ‾ ) ‾ , + ‾ , 0 ‾ , … , 9 ‾ } , P , T ⟩
G=\langle\{T, Z, N\},\{{\underline{(}} {\underline{)}}, \underline{+}, \underline{{0}}, \ldots,
\underline{9}\}, P, T\rangle
G = ⟨{ T , Z , N } , { ( ) , + , 0 , … , 9 } , P , T ⟩
P = { T → ( T + T ) ∣ N N → N Z ∣ Z Z → 0 ‾ ∣ ⋯ ∣ 9 ‾ }
\begin{aligned}P=\{& T \rightarrow(T+T) \mid N \\& N \rightarrow N Z \mid Z \\&Z \rightarrow
\underline{0} \mid \cdots \mid \underline{9}\}\end{aligned}
P = { T → ( T + T ) ∣ N N → NZ ∣ Z Z → 0 ∣ ⋯ ∣ 9 }
Dadurch gilt: Z ⊆ N ⊆ T Z \subseteq N \subseteq T Z ⊆ N ⊆ T
Semantik
M Z ( 0 ‾ ) = 0 , … , M Z ( 9 ‾ ) = 9
\mathcal{M}_{Z}(\underline{0})=0, \ldots, \mathcal{M}_{Z}(\underline{9})=9
M Z ( 0 ) = 0 , … , M Z ( 9 ) = 9
M N ( n z ) = M N ( n ) ⋅ 10 + M Z ( z )
\mathcal{M}_{N}(n z)=\mathcal{M}_{N}(n) \cdot 10+\mathcal{M}_{Z}(z)
M N ( n z ) = M N ( n ) ⋅ 10 + M Z ( z ) n ∈ N , z ∈ Z n \in \mathrm{N}, z \in \mathrm{Z} n ∈ N , z ∈ Z
M N ( n ) = M Z ( n ) \mathcal{M}_{N}(n)=M_{Z}(n) M N ( n ) = M Z ( n ) n ∈ Z n \in \mathrm{Z} n ∈ Z
M T ( ( ‾ t 1 + ‾ t 2 ) ‾ ) = M T ( t 1 ) + M T ( t 2 )
\mathcal{M}_{T}(\underline(t_{1} \underline +
t_{2}\underline))=\mathcal{M}_{T}\left(t_{1}\right)+\mathcal{M}_{T}\left(t_{2}\right)
M T ( ( t 1 + t 2 ) ) = M T ( t 1 ) + M T ( t 2 ) t 1 , t 2 ∈ T t_{1}, t_{2} \in \mathcal{T} t 1 , t 2 ∈ T
M T ( t ) = M N ( t ) \mathcal{M}_{T}(t)=\mathcal{M}_{N}(t) M T ( t ) = M N ( t ) t ∈ N t \in N t ∈ N
Multiplikation (führt zu Mehrdeutigkeit) Syntax
Grammatik
E = L ( G ) \mathcal{E}=\mathcal{L}(G) E = L ( G )
E → 0 ‾ ∣ ⋯ ∣ 9 ‾
E \rightarrow \underline{0}\mid\cdots\mid \underline{9}
E → 0 ∣ ⋯ ∣ 9
E → E + ‾ E E \rightarrow E ~\underline + ~E E → E + E
E → E ∗ ‾ E E \rightarrow E ~\underline* ~E E → E ∗ E
Induktive Definition
E \mathcal E E
{ 0 ‾ , … 9 ‾ } ⊆ E
\{\underline{0}, \ldots \underline{9}\} \subseteq \mathcal{E}
{ 0 , … 9 } ⊆ E
e 1 + ‾ e 2 ∈ E e_{1} ~\underline + ~e_{2} \in \mathcal{E} e 1 + e 2 ∈ E e 1 , e 2 ∈ E e_{1}, e_{2} \in \mathcal{E} e 1 , e 2 ∈ E
e 1 ∗ ‾ e 2 ∈ E e_{1} ~\underline{*}~ e_{2} \in \mathcal{E} e 1 ∗ e 2 ∈ E e 1 , e 2 ∈ E e_{1}, e_{2} \in \mathcal{E} e 1 , e 2 ∈ E
Regulärer Ausdruck (ohne Semantik)
E → 0 ‾ F ∣ ⋯ ∣ 9 ‾ F E \rightarrow \underline{0} F|\cdots| \underline{9} F E → 0 F ∣ ⋯ ∣ 9 F
F → + ‾ E ∣ ∗ E ∣ ϵ F \rightarrow \underline + E|* E| \epsilon F → + E ∣ ∗ E ∣ ϵ
Semantik
Rekursive Definition von meaning function (keine eindeutige Funktion)
M ( 0 ‾ ) = 0 , … \mathcal{M}(\underline{0})=0, \ldots M ( 0 ) = 0 , …
M ( e 1 + ‾ e 2 ) = M ( e 1 ) + M ( e 2 )
\mathcal{M}\left(e_{1} \underline + e_{2}\right) =
\mathcal{M}\left(e_{1}\right)+\mathcal{M}\left(e_{2}\right)
M ( e 1 + e 2 ) = M ( e 1 ) + M ( e 2 )
M ( e 1 ∗ ‾ e 2 ) = M ( e 1 ) ⋅ M ( e 2 )
\mathcal{M}\left(e_{1} \underline * e_{2}\right) =\mathcal{M}\left(e_{1}\right) \cdot
\mathcal{M}\left(e_{2}\right)
M ( e 1 ∗ e 2 ) = M ( e 1 ) ⋅ M ( e 2 )
Mehrdeutigkeit
Mangelnde Hierarchie (Prioritäts-Regel: Multiplikation vor Addition).
Ableitungen entsprechen nicht der intendierten Semantik. Semantik ist nicht eindeutig und dadurch keine Funktion mehr.
Beispiel
M ( 3 ‾ + 3 ‾ ∗ 3 ‾ ) = M ( 3 ‾ ) + M ( 3 ‾ ∗ 3 ‾ ) = M ( 3 ‾ ) + M ( 3 ‾ ) ⋅ M ( 3 ‾ ) = 12
\mathcal{M}(\underline{3}+\underline{3} *
\underline{3})=\mathcal{M}(\underline{3})+\mathcal{M}(\underline{3} *
\underline{3})=\mathcal{M}(\underline{3})+\mathcal{M}(\underline{3}) \cdot
\mathcal{M}(\underline{3})=12
M ( 3 + 3 ∗ 3 ) = M ( 3 ) + M ( 3 ∗ 3 ) = M ( 3 ) + M ( 3 ) ⋅ M ( 3 ) = 12
M ( 3 ‾ + ‾ 3 ‾ ∗ ‾ 3 ‾ ) = M ( 3 ‾ + 3 ‾ ) ⋅ M ( 3 ‾ ) = ( M ( 3 ‾ ) + M ( 3 ‾ ) ) ⋅ M ( 3 ‾ ) = 18
\mathcal{M}(\underline{3} \underline +\underline{3} \underline{*}
\underline{3})=\mathcal{M}(\underline{3}+\underline{3}) \cdot
\mathcal{M}(\underline{3})=(\mathcal{M}(\underline{3})+\mathcal{M}(\underline{3})) \cdot
\mathcal{M}(\underline{3})=18
M ( 3 + 3 ∗ 3 ) = M ( 3 + 3 ) ⋅ M ( 3 ) = ( M ( 3 ) + M ( 3 )) ⋅ M ( 3 ) = 18
Auflösung der Mehrdeutigkeit
Wir können die Prioritätsregel in Semantik M \mathcal M M einbauen (siehe oben) oder in Syntax E \mathcal E E einbauen:
Syntax
H \mathcal H H ist die kleinste Menge mit
{ 0 ‾ , 1 ‾ , … , 9 ‾ } ⊆ H
\{{\underline{0}}, \underline{1}, \ldots, \underline{9}\} \subseteq \mathcal{H}
{ 0 , 1 , … , 9 } ⊆ H
e 1 , e 2 ∈ H → e 1 ∗ ‾ e 2 ∈ H
e_{1}, e_{2} \in \mathcal{H} \rightarrow e_{1} \underline * e_{2} \in \mathcal{H}
e 1 , e 2 ∈ H → e 1 ∗ e 2 ∈ H
E \mathcal E E ist die kleinste Menge mit
H ⊆ E \mathcal{H} \subseteq \mathcal{E} H ⊆ E
e 1 , e 2 ∈ E → e 1 + ‾ e 2 ∈ E
e_{1}, e_{2} \in \mathcal{E} \rightarrow e_{1} \underline + e_{2} \in \mathcal{E}
e 1 , e 2 ∈ E → e 1 + e 2 ∈ E
Semantik
M H ( 0 ‾ ) = 0 , … , M H ( 9 ‾ ) = 9
\mathcal{M}_{\mathcal{H}}(\underline{0})=0, \ldots, \mathcal{M}_{\mathcal{H}}(\underline{9})=9
M H ( 0 ) = 0 , … , M H ( 9 ) = 9
M H ( e 1 ∗ ‾ e 2 ) = M H ( e 1 ) ⋅ M H ( e 2 )
\mathcal{M}_{\mathcal{H}}(e_{1} \underline{*} e_{2})=\mathcal{M}_{\mathcal{H}}(e_{1}) \cdot
\mathcal{M}_{\mathcal{H}}(e_{2})
M H ( e 1 ∗ e 2 ) = M H ( e 1 ) ⋅ M H ( e 2 )
M E ( e ) = M H ( e )
\mathcal{M}_{\mathcal{E}}(e)=\mathcal{M}_{\mathcal{H}}(e)
M E ( e ) = M H ( e ) e ∈ H e \in \mathcal{H} e ∈ H
M E ( e 1 + ‾ e 2 ) = M E ( e 1 ) + M E ( e 2 )
\mathcal{M}_{\mathcal{E}}(e_{1} \underline +
e_{2})=\mathcal{M}_{\mathcal{E}}(e_{1})+\mathcal{M}_{\mathcal{E}}(e_{2})
M E ( e 1 + e 2 ) = M E ( e 1 ) + M E ( e 2 )
Beispiel
M E ( 2 ‾ ∗ ‾ 3 ‾ + ‾ 4 ‾ ) = M E ( 2 ‾ 3 ‾ 3 ‾ ) + M E ( 4 ‾ ) = M H ( 2 ‾ 3 ‾ 3 ‾ ) + M H ( 4 ‾ ) = M H ( 2 ‾ ) ⋅ M H ( 3 ‾ ) + 4 = 2 ⋅ 3 + 4 = 10
\begin{aligned}\mathcal{M}_{\mathcal{E}}(\underline{2} \underline{ *} \underline{3} \underline
+\underline{4}) &=\mathcal{M}_{\mathcal{E}}(\underline{2} \underline{3}
\underline{3})+\mathcal{M}_{\mathcal{E}}(\underline{4}) \\&=\mathcal{M}_{\mathcal{H}}(\underline{2}
\underline{3} \underline{3})+\mathcal{M}_{\mathcal{H}}(\underline{4})
\\&=\mathcal{M}_{\mathcal{H}}(\underline{2}) \cdot \mathcal{M}_{\mathcal{H}}(\underline{3})+4
\\&=2 \cdot 3+4=10\end{aligned}
M
E
( 2 ∗ 3 + 4 ) = M
E
( 2 3 3 ) + M
E
( 4 ) = M
H
( 2 3 3 ) + M
H
( 4 ) = M
H
( 2 ) ⋅ M
H
( 3 ) + 4 = 2 ⋅ 3 + 4 = 10
Terme Terme über Modellstrukturen
Terme
T ( D ) \small \mathcal{T(D)} T ( D ) D \small \mathcal D D
Syntax
Keine Prädikate.
I V S ⊆ T ( D ) \small I V S \subseteq \mathcal{T}(\mathcal{D}) I V S ⊆ T ( D )
wobei
IVS: { x ‾ , y ‾ , z ‾ , … , x ‾ 1 , … }
\small \text { IVS: }\left\{\underline{\mathrm{x}}, \underline{\mathrm{y}}, \underline{\mathrm{z}},
\ldots, \underline{\mathrm{x}}_{1}, \ldots\right\}
IVS: { x , y , z , … , x 1 , … }
K S ( D ) ⊆ T ( D )
\small K S(\mathcal{D}) \subseteq \mathcal{T}(\mathcal{D})
K S ( D ) ⊆ T ( D ) f ′ ( ‾ t 1 , ‾ … , ‾ t n ) ‾ ∈ T ( D )
\small f^{\prime}\underline(t_{1} \underline, \ldots \underline , t_{n} \underline ) \in
\mathcal{T}(\mathcal{D})
f ′ ( t 1 , … , t n ) ∈ T ( D )
wenn
f ′ ∈ F S n ( D ) \small f^{\prime} \in F S_{n}(\mathcal{D}) f ′ ∈ F S n ( D ) t 1 , … , t n ∈ T ( D )
\small t_{1}, \ldots, t_{n} \in \mathcal{T}(\mathcal{D})
t 1 , … , t n ∈ T ( D )
Semantik
Keine Prädikate - deshalb entspricht der gesamte Ausdruck immer nur einem Domänenobjekt.
M T : ENV ( D ) × T ( D ) ↦ D
\small \color{pink} \mathcal{M}_{\mathcal{T}}: \operatorname{ENV}(\mathcal{D}) \times
\mathcal{T}(\mathcal{D}) \mapsto D
M
T
: ENV ( D ) × T ( D ) ↦ D
M T ( I , v ) = I ( v ) \small \mathcal{M}_{\mathcal{T}}(I, v)=I(v) M T ( I , v ) = I ( v )
wenn
v ∈ I V S \small v \in I V S v ∈ I V S
M T ( I , c ′ ) = c
\small \mathcal{M}_{\mathcal{T}}\left(I, c^{\prime}\right)=c
M T ( I , c ′ ) = c
wenn
c ′ ∈ K S ( D ) \small c^{\prime} \in K S(\mathcal{D}) c ′ ∈ K S ( D )
3.
M T ( I , f ′ ( t 1 , … , t n ) ) = f ( M T ( I , t 1 ) , … , M T ( I , t n ) )
\small \mathcal{M}_{\mathcal{T}}\left(I, f^{\prime}\left(t_{1}, \ldots,
t_{n}\right)\right)=f\left(\mathcal{M}_{\mathcal{T}}\left(I, t_{1}\right), \ldots,
\mathcal{M}_{\mathcal{T}}\left(I, t_{n}\right)\right)
M T ( I , f ′ ( t 1 , … , t n ) ) = f ( M T ( I , t 1 ) , … , M T ( I , t n ) )
Boolesche Ausdrücke Boolsche Ausdrücke über Modellstrukturen
Syntax
B A ( D ) \small \mathcal {BA(D)} B A ( D )
p ( ‾ t 1 , … , t n ) ‾ ∈ B A ( D )
\small p \underline{(} t_{1}, \ldots, t_{n} \underline{)} \in \mathcal{B} \mathcal{A}(\mathcal{D})
p ( t 1 , … , t n ) ∈ B A ( D ) (Atomformel)
wenn
p ∈ P S n ( D ) \small p \in P S_{n}(\mathcal{D}) p ∈ P S n ( D ) t 1 , … , t n ∈ T ( D )
\small t_{1}, \ldots, t_{n} \in \mathcal{T}(\mathcal{D})
t 1 , … , t n ∈ T ( D )
t 1 = ‾ t 2 \small t_1 \underline = t_2 t 1 = t 2
wenn
t 1 , t 2 ∈ T ( D ) \small t_1, t_2 \in \mathcal{T}(\mathcal{D}) t 1 , t 2 ∈ T ( D )
¬ ‾ F , ( ‾ F ∧ ‾ G ) ‾ , ( ‾ F ∨ ‾ G ) ‾ ∈ B A ( D )
\small \underline \neg F,~ \underline{(} F \underline \wedge G \underline{)},~ \underline{(} F
\underline{\vee} G \underline{)} \in \mathcal{B} \mathcal{A}(\mathcal{D})
¬ F , ( F ∧ G ) , ( F ∨ G ) ∈ B A ( D )
wenn
F , G ∈ B A ( D )
\small F, G \in \mathcal{B} \mathcal{A}(\mathcal{D})
F , G ∈ B A ( D )
Semantik
M B A : E N V × B A ( D ) → { t , f }
\small \color{pink} \mathcal{M}_{\mathcal{B} \mathcal{A}}: E N V \times \mathcal{B} \mathcal{A}(\mathcal{D})
\rightarrow\{\mathbf{t}, \mathbf{f}\}
M
B
A : EN V × B A ( D ) → { t , f }
M B A ( I , p ′ ( t 1 , … , t n ) ) = p ( M T ( I , t 1 ) , … , M T ( I , t n ) )
\small \mathcal{M}_{\mathcal{B} \mathcal{A}}\left(I, p^{\prime}\left(t_{1}, \ldots,
t_{n}\right)\right)=p\left(\mathcal{M}_{\mathcal{T}}\left(I, t_{1}\right), \ldots,
\mathcal{M}_{\mathcal{T}}\left(I, t_{n}\right)\right)
M B A ( I , p ′ ( t 1 , … , t n ) ) = p ( M T ( I , t 1 ) , … , M T ( I , t n ) )
wobei
p p p p ′ ∈ P S n ( D ) \small p^{\prime} \in P S_{n}(\mathcal{D}) p ′ ∈ P S n ( D )
M B A ( I , t 1 ≡ t 2 ) = t
\small \mathcal{M}_{\mathcal{B A}}(I, t1 \equiv t_2)=\mathbf{t}
M B A ( I , t 1 ≡ t 2 ) = t
wenn
M T ( I , t 1 ) = M T ( I , t 2 )
\small \mathcal{M}_{\mathcal{T}}(I, t_1)=\mathcal{M}_{\mathcal{T}}(I, t_2)
M T ( I , t 1 ) = M T ( I , t 2 ) f \small \mathbf{f} f
M B A ( I , ¬ F ) = { t falls M B A ( I , F ) = f f falls M B A ( I , F ) = t
\small \mathcal{M}_{\mathcal{B} \mathcal{A}}(I, \neg F)= \begin{cases}\mathbf{t} & \text { falls }
\mathcal{M}_{\mathcal{B} \mathcal{A}}(I, F)=\mathbf{f} \\ \mathbf{f} & \text { falls }
\mathcal{M}_{\mathcal{B} \mathcal{A}}(I, F)=\mathbf{t}\end{cases}
M B A ( I , ¬ F ) = { t f falls M
B
A ( I , F ) = f falls M
B
A ( I , F ) = t M B A ( I , ( ‾ F ∧ ‾ G ) ‾ ) = { t falls M B A ( I , F ) = t und M B A ( I , G ) = t f sonst
\small \mathcal{M}_{\mathcal{B A}}(I,\underline (F \underline \wedge G\underline ))=
\begin{cases}\mathbf{t} & \text { falls } \mathcal{M}_{\mathcal{B} \mathcal{A}}(I, F)=\mathbf{t}
\text { und } \mathcal{M}_{\mathcal{B} \mathcal{A}}(I, G)=\mathbf{t} \\ \mathbf{f} & \text { sonst
}\end{cases}
M B A ( I , ( F ∧ G ) ) = { t f falls M
B
A ( I , F ) = t und M
B
A ( I , G ) = t sonst M B A ( I , ( ‾ F ∨ ‾ G ) ‾ ) = { t falls M B A ( I , F ) = t oder M B A ( I , G ) = t f sonst
\small \mathcal{M}_{\mathcal{B A}}(I,\underline (F \underline \vee G\underline ))=
\begin{cases}\mathbf{t} & \text { falls } \mathcal{M}_{\mathcal{B} \mathcal{A}}(I, F)=\mathbf{t}
\text { oder } \mathcal{M}_{\mathcal{B} \mathcal{A}}(I, G)=\mathbf{t} \\ \mathbf{f} & \text { sonst
}\end{cases}
M B A ( I , ( F ∨ G ) ) = { t f falls M
B
A ( I , F ) = t oder M
B
A ( I , G ) = t sonst
Einfache Programmiersprache A
ssigned
L
anguge
A L ( D ) \small AL(\mathcal D) A L ( D ) D \mathcal D D
Syntax
A L ( D ) \small AL(\mathcal D ) A L ( D )
v ← ‾ t ∈ A L ( D ) v \underline \larr t \in A L(\mathcal{D}) v ← t ∈ A L ( D ) v ∈ I V S v \in I V S v ∈ I V S t ∈ T ( D ) t \in \mathcal{T}(\mathcal{D}) t ∈ T ( D ) begin ‾ α ; β end ‾ ∈ A L ( D )
\underline{\text{begin}}~ \alpha \text {; } \beta ~\underline{\text{end}} \in A L(\mathcal{D})
begin α ; β end ∈ A L ( D ) α , β ∈ A L ( D ) \alpha, \beta \in A L(\mathcal{D}) α , β ∈ A L ( D ) if ‾ B then ‾ α else ‾ β ∈ A L ( D )
\underline{\text{if}}~ B ~\underline{\text{then}}~ \alpha ~\underline{\text{else}}~ \beta \in A
L(\mathcal{D})
if B then α else β ∈ A L ( D ) α , β ∈ A L ( D ) \alpha, \beta \in A L(\mathcal{D}) α , β ∈ A L ( D ) B ∈ B A ( D ) B \in \mathcal{B} \mathcal{A}(\mathcal{D}) B ∈ B A ( D ) while ‾ B do ‾ α ∈ A L ( D )
\underline{\text{while}}~ B ~\underline{\text{do}}~ \alpha \in A L(\mathcal{D})
while B do α ∈ A L ( D ) α ∈ A L ( D ) \alpha\in A L(\mathcal{D}) α ∈ A L ( D ) B ∈ B A ( D ) B \in \mathcal{B} \mathcal{A}(\mathcal{D}) B ∈ B A ( D )