Denotational semantics

The denotational semantics (function semantics ; English: denotational semantics ) is one of several possibilities in theoretical computer science to define a formal semantics for a formal language . The formal language serves as a mathematical model for a real programming language . The mode of operation of a computer program can thus be formally described.

Specifically, given a given assignment for input variables, the end result for a set of output variables can be calculated using denotational semantics. More general proofs of correctness are also possible.

In denotational semantics, partial functions are used that map state spaces to one another. A state here is an assignment of variables with concrete values. Denotational semantics are inductively defined using the syntactic instruction constructs of the formal language. The partial functions are selected depending on the desired program semantics.

In addition to denotational semantics, there are also operational semantics and axiomatic semantics to describe the semantics of formal languages.

Definition of the semantic function f

Let be the set of all possible states. The effect that an instruction has a condition, spoken formally a picture ${\displaystyle {\mathcal {Z}}}$ ${\displaystyle \ A}$

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

which assigns a subsequent state to a state . ${\displaystyle z\in {\mathcal {Z}}}$ ${\displaystyle z'\in {\mathcal {Z}}}$

${\displaystyle \ f}$ denotes the semantic function and assigns a meaning to each instruction construct by causing a change in the state of the program.

The effect of the most important control structures of a programming language on a state is examined below.

• The meaning of the empty statement : ${\displaystyle \ null}$

${\displaystyle f[null](z)\ =\ z}$.

The empty statement applied to a state does not change the state. ${\displaystyle \ z}$

• The semantics of an instruction sequence can be described as follows:

${\displaystyle f[A_{1},A_{2}](z)\ =\ f[A_{2}](f[A_{1}](z))}$.

The meaning of this command sequence is the effect of applied on the state that results after the execution on . ${\displaystyle \ A_{2}}$ ${\displaystyle \ A_{1}}$ ${\displaystyle \ z}$

• The following applies to the effect of an assignment on a state:

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

The program does not terminate ( ) if the statement (or expression) applied to the state does not terminate. In all other cases the program goes into one state . ${\displaystyle \ \bot }$ ${\displaystyle \ [E]}$ ${\displaystyle \ z}$ ${\displaystyle \ z'}$

• For the two-sided alternative, the following applies:

${\displaystyle f[if\ B\ then\ C_{1}\ else\ C_{2}](z)={\begin{cases}f[C_{1}](z),&\mathrm {wenn} \ B[z]=true\\f[C_{2}](z),&\mathrm {wenn} \ B[z]=false\\\bot ,&\mathrm {sonst} \end{cases}}}$.

The subsequent state corresponds to applied to if . If so, the subsequent state is determined by applied to . In all other cases the program does not terminate. ${\displaystyle \ [C_{1}]}$ ${\displaystyle \ z}$ ${\displaystyle \ B[z]=true}$ ${\displaystyle \ B[z]=false}$ ${\displaystyle \ [C_{2}]}$ ${\displaystyle \ z}$

• The meaning of the repetition is defined recursively as:

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

If so, the While statement does not change the state. ${\displaystyle \ [B](z)=false}$

If or , the entire program does not terminate. ${\displaystyle \ [B](z)=\bot }$ ${\displaystyle \ [L](z)=\bot }$

In all other cases, the iteration statement is reapplied to the state that results after the execution of . ${\displaystyle \ [while\ B\ do\ L]}$ ${\displaystyle \ [L](z)}$

This recursive definition cannot be used to infer the effect of this statement. One is therefore interested in the fixed point of the function, which describes the semantics of the while loop.

Fixed point of the while semantics

The fixed point of the function, which describes the semantics of the While Loop, is explained below using a simple example.

${\displaystyle \ while\ x\not =y\ do\ y:=y+1}$

As long as not equal , the value of the variable is increased by 1. ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle y}$

To determine the fixed point of this equation, one uses the Tarskian fixed point theorem . This theorem says that for an ordered set that has a smallest element and a strictly monotonic function that maps to itself, a smallest fixed point exists. ${\displaystyle \ {\mathcal {M}}}$ ${\displaystyle \ {\mathcal {M}}}$

In order for the theorem to be applicable, an ordered set must first be defined for the example.

Let be the partial function of the while loop from the example. This maps one state, consisting of the assignment for the variables of the same name, to another state with the variable assignment . The variables and are whole numbers. ${\displaystyle w\colon (\mathbb {Z} \times \mathbb {Z} )\rightarrow (\mathbb {Z} \times \mathbb {Z} )}$ ${\displaystyle (x,y)}$ ${\displaystyle (x',y')}$ ${\displaystyle x}$ ${\displaystyle y}$

Now be the set of all partial functions . ${\displaystyle {\mathcal {P}}_{(\mathbb {Z} \times \mathbb {Z} )}}$ ${\displaystyle \ w}$

The partial order for two partial functions , is defined as follows: ${\displaystyle \sqsubseteq }$ ${\displaystyle \ w}$ ${\displaystyle \ w'\in {\mathcal {P}}_{(\mathbb {Z} \times \mathbb {Z} )}}$

${\displaystyle \ w\sqsubseteq w'\Leftrightarrow \operatorname {dom} (w)\subseteq \operatorname {dom} (w')\wedge (w(x,y)=(x',y')\Rightarrow w'(x,y)=(x',y'))}$.

The partial mapping is less than or equal to if and only if the domain of is a subset of the domain of . It must also be the case that if a state change to causes and function of maps. ${\displaystyle \ w}$ ${\displaystyle \ w'}$ ${\displaystyle \ w}$ ${\displaystyle \ w'}$ ${\displaystyle \ w(x,y)}$ ${\displaystyle \ (x',y')}$ ${\displaystyle \ w'(x,y)}$ ${\displaystyle \ (x',y')}$

The smallest element of the set is the nowhere defined function . ${\displaystyle {\mathcal {P}}_{(\mathbb {Z} \times \mathbb {Z} )}}$ ${\displaystyle \bot }$

In order to be able to use Tarski's theorem, a strictly monotonous function that maps to itself is still missing . A function is defined for this: ${\displaystyle {\mathcal {P}}_{(\mathbb {Z} \times \mathbb {Z} )}}$ ${\displaystyle \ f}$

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

According to the example above, the following applies : ${\displaystyle \ f}$

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

Furthermore let:

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

Now all requirements of the fixed point theorem are fulfilled, there is a fixed point.

The fixed point is calculated by forming the limit of the function . ${\displaystyle \ f}$

In order to be able to infer the limit value, one begins with the calculation of individual function values.

• ${\displaystyle \ w_{0}(x,y)=\bot }$as is the smallest element of the set . ${\displaystyle \ w_{0}}$ ${\displaystyle {\mathcal {P}}_{(\mathbb {Z} \times \mathbb {Z} )}}$

• ${\displaystyle \ w_{1}(x,y)}$is according to the definition of the function : ${\displaystyle \ f}$

${\displaystyle \ w_{1}(x,y)=f(w_{0})(x,y)={\begin{cases}(x,y),&\mathrm {wenn} \ x=y\\w_{0}(x,y+1)=\bot ,&\mathrm {sonst} \end{cases}}}$.

• ${\displaystyle \ w_{2}(x,y)}$ results in:

${\displaystyle \ w_{2}(x,y)=f(w_{1})(x,y)={\begin{cases}(x,y),&\mathrm {wenn} \ x=y\\w_{1}(x,y+1)={\begin{cases}(x,y+1),&\mathrm {wenn} \ x=y+1\\\bot ,&\mathrm {sonst} \end{cases}}\end{cases}}}$.

• For can be formulated: ${\displaystyle \ w_{n}}$

${\displaystyle \ w_{n}(x,y)=f(w_{n-1})(x,y)={\begin{cases}(x,x),&\mathrm {wenn} \ x-(n-1)\leq y\leq x\\\bot ,&\mathrm {sonst} \end{cases}}}$.

The limit value is now: ${\displaystyle \ w_{\infty }=w_{n}\ \forall \ n\in \mathbb {N} }$

${\displaystyle w_{\infty }(x,y)={\begin{cases}(x,x),&\mathrm {wenn} \ -\infty \leq y\leq x\\\bot ,&\mathrm {sonst} \end{cases}}}$.

For the fixed point it must now apply that . ${\displaystyle \ f(w_{\infty })(x,y)=w_{\infty }(x,y)}$

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

This can be transformed to:

${\displaystyle \ f(w_{\infty })(x,y)={\begin{cases}(x,x),&\mathrm {wenn} \ -\infty \leq y\leq x\\\bot ,&\mathrm {sonst} \end{cases}}}$.

Thus applies . The fixed point has been found. The meaning of the while loop in the example results from the fixed point. The loop terminates if , and returns the tuple . If so, the loop does not terminate. ${\displaystyle \ f(w_{\infty })(x,y)=w_{\infty }(x,y)}$ ${\displaystyle \ y\leq x}$ ${\displaystyle \ (x,x)}$ ${\displaystyle \ y>x}$

literature

• Peter Schroeder-Heister : Semantics, denotational , in: Jürgen Mittelstraß (Hrsg.): Encyclopedia Philosophy and Philosophy of Science. 2nd Edition. Volume 7: Re - Te. Stuttgart, Metzler 2018, ISBN 978-3-476-02106-9 , pp. 341–342 (non-technical general description; with bibliography)