Denotationelle Semantik

Die denotationelle Semantik (Funktionensemantik) ist in der Theoretischen Informatik eine von mehreren Möglichkeiten, eine formale Semantik für eine formale Sprache zu definieren. Die formale Sprache dient hierbei als mathematisches Modell für eine echte Programmiersprache. Somit kann die Wirkungsweise eines Computerprogramms formal beschrieben werden.

Konkret kann man etwa bei einer gegebenen Belegung für Eingabevariablen das Endergebnis für eine Menge von Ausgabevariablen mit der denotationellen Semantik berechnen. Es sind auch allgemeinere Korrektheitsbeweise möglich.

Bei der denotationellen Semantik werden partielle Funktionen verwendet, die Zustandsräume aufeinander abbilden. Ein Zustand ist hier eine Belegung von Variablen mit konkreten Werten. Die denotationelle Semantik wird induktiv über die syntaktischen Anweisungskonstrukte der formalen Sprache definiert. Abhängig von der gewünschten Programmsemantik werden die partiellen Funktionen gewählt.

Definition der semantischen Funktion $\ f$

Sei $\mathcal{Z}$ die Menge aller möglichen Zustände. Die Wirkung, die eine Anweisung $\ A$ auf einen Zustand hat, ist formal gesprochen eine Abbildung

$f[A]:\mathcal{Z}\rightarrow\mathcal{Z}$,

die einem Zustand $z\in\mathcal{Z}$ einen Folgezustand $z'\in\mathcal{Z}$ zuordnet.

$\ f$ bezeichnet die semantische Funktion und ordnet jedem Anweisungskonstrukt eine Bedeutung zu, indem sie eine Zustandsänderung des Programms bewirkt.

Nachfolgend wird die Wirkung der wichtigsten Kontrollstrukturen einer Programmiersprache auf einen Zustand untersucht.

• Die Bedeutung der leeren Anweisung $\ null$:

$f[null](z)\ =\ z$.

Die leere Anweisung, angewendet auf einen Zustand $\ z$, verändert den Zustand nicht.

• Die Semantik einer Anweisungsfolge kann folgendermaßen beschrieben werden:

$f[A_1,A_2](z)\ =\ f[A_2](f[A_1](z))$.

Die Bedeutung dieser Befehlssequenz, ist die Wirkung von $\ A_2$ angewendet auf den Zustand, der sich ergibt nachdem $\ A_1$ auf $\ z$ ausgeführt wurde.

• Für die Wirkung einer Zuweisung auf einen Zustand gilt:

$f[x:=E](z)\ =\ \begin{cases} \perp, &wenn\ [E](z)=\perp \\ z', &sonst \end{cases}$.

Das Programm terminiert nicht ($\ \perp$), wenn die Anweisung (oder der Ausdruck) $\ [E]$ angewendet auf Zustand $\ z$ nicht terminiert. In allen anderen Fällen geht das Programm in einen Zustand $\ z'$ über.

• Für die zwei-seitige Alternative gilt:

$f[if\ B\ then\ C_1\ else\ C_2](z)= \begin{cases} f[C_1](z), & wenn\ B[z] = true \\ f[C_2](z), & wenn\ B[z]=false \\ \perp, &sonst \end{cases}$.

Der Folgezustand entspricht $\ [C_1]$ angewendet auf $\ z$, wenn $\ B[z]=true$. Wenn $\ B[z]=false$ so wird der nachfolgende Zustand durch $\ [C_2]$ angewendet auf $\ z$ bestimmt. In allen anderen Fällen terminiert das Programm nicht.

• Die Bedeutung der Wiederholung definiert sich rekursiv zu:

$f[while\ B\ do\ L](z)=\begin{cases} z, &wenn\ [B](z)=false \\ \perp, &wenn\ [B](z)=\perp\ \or\ [L](z)=\perp \\ f[while\ B\ do\ L]([L](z)), &sonst\end{cases}$.

Falls $\ [B](z)=false$ so bewirkt die While-Anweisung keine Zustandsänderung.

Wenn $\ [B](z)=\perp$ oder $\ [L](z)=\perp$ so terminiert das gesamte Programm nicht.

In allen anderen Fällen wird erneut die Wiederholungsanweisung $\ [while\ B\ do\ L]$ auf den Zustand der sich nach Ausführung von $\ [L](z)$ ergibt, angewendet.

Durch diese rekursive Definition kann man nicht auf die Wirkung dieser Anweisung schließen. Man ist daher an dem Fixpunkt der While-Schleife interessiert.

Fixpunkt der While-Semantik

Der Fixpunkt der While-Schleife wird nachfolgend anhand eines einfachen Beispiels erläutert.

$\ while\ x\not=y\ do\ y:=y+1$

Solange x ungleich y wird der Wert der Variablen y um 1 erhöht.

Um den Fixpunkt dieser Gleichung zu bestimmen, bedient man sich des Tarskischen Fixpunktsatzes. Dieser Satz besagt, dass für eine geordnete Menge $\ \mathcal{M}$, welche ein kleinstes Element besitzt, und eine streng monotone Funktion, welche $\ \mathcal{M}$ auf sich selbst abbildet, ein kleinster Fixpunkt existiert.

Damit der Satz angewendet werden kann, muss zuerst eine geordnete Menge für das Beispiel definiert werden.

Sei $w:(\mathbb{Z}\times\mathbb{Z})\rightarrow(\mathbb{Z}\times\mathbb{Z})$ die partielle Funktion der While-Schleife aus dem Beispiel. Diese bildet einen Zustand, bestehend aus der Belegung für die Variablen (x,y) in einen anderen Zustand mit der Variablenbelegung (x',y') ab. Die Variablen x und y sind dabei ganze Zahlen.

Sei nun $\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ die Menge aller partiellen Funktionen $\ w$.

Die partielle Ordnung $\sqsubseteq$ für zwei partielle Funktionen $\ w$, $\ w' \in \mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ sei wie folgt definiert:

$\ w \sqsubseteq w' \Leftrightarrow \ dom(w) \subseteq dom(w') \wedge w(x,y)=(x',y') \rightarrow w'(x,y)=(x',y')$.

Die partielle Abbildung $\ w$ ist kleiner als $\ w'$ genau dann, wenn der Definitionsbereich von $\ w$ eine Teilmenge des Definitionsbereichs von $\ w'$ ist. Zudem muss gelten, dass wenn $\ w(x,y)$ eine Zustandsänderung nach $\ (x',y')$ bewirkt, so muss auch Funktion $\ w'(x,y)$ in $\ (x',y')$ abbilden.

Das kleinste Element der Menge $\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ ist die nirgends definierte Funktion $\perp$.

Um den Satz von Tarski verwenden zu können, fehlt nun noch eine streng monotone Funktion, die $\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ auf sich selbst abbildet. Dazu wird eine Funktion $\ f$ definiert:

$\ f:\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}\rightarrow \mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$.

Laut obigen Beispiel gilt für $\ f$:

$\ f(w)(x,y)=\begin{cases}(x,y), &wenn\ x=y \\ w(x,y+1), &sonst \end{cases}$.

Weiterhin sei:

$\ w_{n+1}=f(w_n)\ \forall n\isin\mathbb{N}$.

Nun sind alle Voraussetzungen des Fixpunktsatzes erfüllt, es existiert ein Fixpunkt.

Den Fixpunkt berechnet man durch Grenzwertbildung der Funktion $\ f$.

Um auf den Grenzwert schließen zu können, beginnt man mit dem Ausrechnen einzelner Funktionswerte.

• $\ w_0(x,y)= \perp$, da $\ w_0$ das kleinste Element der Menge $\mathcal{P}_{(\mathbb{Z}\times\mathbb{Z})}$ ist.

• $\ w_1(x,y)$ ist laut Definition der Funktion $\ f$:

$\ w_1(x,y)=f(w_0)(x,y)=\begin{cases}(x,y),&wenn\ x=y \\ w_0(x,y+1)=\perp,&sonst\end{cases}$.

• $\ w_2(x,y)$ ergibt sich zu:

$\ w_2(x,y)=f(w_1)(x,y)=\begin{cases}(x,y),&wenn\ x=y \\ w_1(x,y+1)=\begin{cases}(x,y+1),&wenn\ x=y+1 \\ \perp,&sonst \end{cases}\end{cases}$.

• Für $\ w_n$ kann formuliert werden:

$\ w_n(x,y)=f(w_{n-1})(x,y)=\begin{cases}(x,x),&wenn\ x-(n-1) \le y \le x \\ \perp,& sonst\end{cases}$.

Der Grenzwert $\ w_{\infty} = w_n \ \forall \ n \isin \mathbb{N}$ sei nun:

$w_{\infty}(x,y)=\begin{cases}(x,x),&wenn\ -\infty \le y \le x \\ \perp,& sonst\end{cases}$.

Für den Fixpunkt muss nun gelten, dass $\ f(w_{\infty})(x,y)=w_{\infty}(x,y)$.

$\ f(w_{\infty})(x,y)=\begin{cases}(x,y),&wenn \ x=y \\ w_{\infty}(x,y+1)= \begin{cases}(x,x), &wenn\ -\infty \le y < x \\ \perp,&sonst\end{cases}\end{cases}$.

Dies kann umgeformt werden zu:

$\ f(w_{\infty})(x,y)=\begin{cases}(x,x), &wenn\ -\infty \le y \le x \\ \perp,&sonst\end{cases}$.

Somit gilt $\ f(w_{\infty})(x,y)=w_{\infty}(x,y)$. Der Fixpunkt ist gefunden. Die Bedeutung der While-Schleife aus dem Beispiel ergibt sich aus dem Fixpunkt. Die Schleife terminiert, wenn $\ y \le x$, und liefert das Tupel $\ (x,x)$. Falls $\ y > x$, so terminiert die Schleife nicht.

Siehe auch

• Formale Semantik
• operationelle Semantik
• axiomatische Semantik