4 - Operational Semantics

2019-11-01 11:00 CST
2019-12-20 11:35 CST
CC BY-NC 4.0

Recall: language = syntax + semantics

Semantics of a language:

• Operational semantics
• Denotational semantics
• Axiomatic semantics

What is Operational Semantics

Operational semantics defines program executions: sequence of steps, formulated as transitions of an abstract machine (AM).

Recall: AM = Expression/statement + States

• Small-step semantics: describe each single step of the execution
• Big-step semantics: describe the overall result of the execution

States

$$(\text{State})\ \sigma \in \text{Var} \rightarrow \text{Values}$$

Examples: $\sigma_1 = \{ (x, 2), (y, 3), (a, 10) \} = \{ x \leadsto 2, y \leadsto 3, a \leadsto 10 \}$.

Recall

$$\sigma \{ x \leadsto n \} \overset{\text{def}}{=} \lambda z. \ \begin{cases} \sigma(z), & z \neq x, \\ n, & z = x. \end{cases}$$

We have $\sigma_1 \{ y \leadsto 7 \} = \{ x \leadsto 2, y \leadsto 7, a \leadsto 10 \}$.

Small-step Structural Operational Semantics (SOS)

Systematic definition of operational semantics:

• The program syntax is inductively-defined
• We can also define the semantics of a program in terms of the semantics of its parts
• “Structural”: syntax oriented （语法制导） and inductive

Small-step SOS for Expression Evaluation

Define a transition $(e, \sigma) \rightarrow (e', \sigma')$ with addition: (the calculation priority is from left to right)

$${(e_1, \sigma) \rightarrow (e_1', \sigma) \over (e_1 + e_2, \sigma) \rightarrow (e_1' + e_2, \sigma)}$$

$${(e_2, \sigma) \rightarrow (e_2', \sigma) \over (\textbf{n} + e_2, \sigma) \rightarrow (\textbf{n} + e_2', \sigma)}$$

$${\lfloor \textbf{n}_1 \rfloor \lfloor + \rfloor \lfloor \textbf{n}_2 \rfloor = \lfloor \textbf{n} \rfloor \over (\textbf{n}_1 + \textbf{n}_2, \sigma) \rightarrow (\textbf{n}, \sigma)}$$

Example:

\begin{aligned} & ((\textbf{10} + \textbf{12}) + (\textbf{13} + \textbf{20}), \sigma) \\ & \rightarrow (\textbf{22} + (\textbf{13} + \textbf{20}), \sigma) \\ & \rightarrow (\textbf{22} + \textbf{33}, \sigma) \\ & \rightarrow (\textbf{55}, \sigma) \end{aligned}

Transitisons for subtraction:

$${(e_1, \sigma) \rightarrow (e_1', \sigma) \over (e_1 - e_2, \sigma) \rightarrow (e_1' - e_2, \sigma)}$$

$${(e_2, \sigma) \rightarrow (e_2', \sigma) \over (\textbf{n} - e_2, \sigma) \rightarrow (\textbf{n} - e_2', \sigma)}$$

$${\lfloor \textbf{n}_1 \rfloor \lfloor - \rfloor \lfloor \textbf{n}_2 \rfloor = \lfloor \textbf{n} \rfloor \over (\textbf{n}_1 - \textbf{n}_2, \sigma) \rightarrow (\textbf{n}, \sigma)}$$

Transition for evaluating variables:

$${ \sigma(x) = \lfloor \textbf{n} \rfloor \over (x, \sigma) \rightarrow (\textbf{n}, \sigma) }$$

Example: $\sigma = \{ x \leadsto 10, y \leadsto 42 \}$,

$$(x+y, \sigma) \rightarrow (\textbf{10} + y, \sigma) \rightarrow \cdots$$

Small-step SOS for Boolean Expressions

Overload the symbol $\rightarrow$ (actually have different type with the $\rightarrow$ above). Define transitions for comparisons:

$${(e_1, \sigma) \rightarrow (e_1', \sigma) \over (e_1 - e_2, \sigma) \rightarrow (e_1' = e_2, \sigma)}$$

$${(e_2, \sigma) \rightarrow (e_2', \sigma) \over (\textbf{n} - e_2, \sigma) \rightarrow (\textbf{n} = e_2', \sigma)}$$

$${\lfloor \textbf{n}_1 \rfloor \lfloor = \rfloor \lfloor \textbf{n}_2 \rfloor \over (\textbf{n}_1 = \textbf{n}_2, \sigma) \rightarrow (\textbf{true}, \sigma)}$$

$${\neg (\lfloor \textbf{n}_1 \rfloor \lfloor = \rfloor \lfloor \textbf{n}_2 \rfloor) \over (\textbf{n}_1 = \textbf{n}_2, \sigma) \rightarrow (\textbf{false}, \sigma)}$$

Transitions for negation:

$${ (b, \sigma) \rightarrow (b', \sigma) \over (\neg b, \sigma) \rightarrow (\neg b', \sigma) }$$

$${ \over (\neg \textbf{true}, \sigma) \rightarrow (\textbf{false}, \sigma) }$$

$${ \over (\neg \textbf{false}, \sigma) \rightarrow (\textbf{true}, \sigma) }$$

Small-step SOS for Statements

Overload the symbol $\rightarrow$ again. The statement execution relation has the form of $(c, \sigma) \rightarrow (c', \sigma')$ or $(c, \sigma) \rightarrow \sigma'$ (termination).

Skip

$${ \over (\textbf{skip}, \sigma) \rightarrow \sigma }$$

Assignment

$${ (e, \sigma) \rightarrow (e', \sigma) \over (x := e, \sigma) \rightarrow (x := e', \sigma) }$$

$${ \over (x := \textbf{n}, \sigma) \rightarrow \sigma \{ x \leadsto \lfloor \textbf{n} \rfloor \} }$$

Example:

$$(x := \textbf{10} + \textbf{12}, \sigma) \rightarrow (x := \textbf{22}, \sigma) \rightarrow \sigma \{ x \leadsto 22 \}$$

Sequential Composition

$${ (c_0, \sigma) \rightarrow (c_0', \sigma') \over (c_0; c_1, \sigma) \rightarrow (c_0'; c_1, \sigma') }$$

$${ (c_0, \sigma) \rightarrow \sigma' \over (c_0; c_1, \sigma) \rightarrow (c_1, \sigma')}$$

Example:

\begin{aligned} & (x := \textbf{10} + \textbf{12}; x := x + 1, \sigma) \\ & \rightarrow (x := \textbf{22}; x := x + 1, \sigma) \\ & \rightarrow (x := x + 1, \sigma \{ x \leadsto 22 \}) \\ & \rightarrow (x := \textbf{22} + 1, \sigma \{ x \leadsto 22 \}) \\ & \rightarrow (x := \textbf{23}, \sigma \{ x \leadsto 22 \}) \\ & \rightarrow \sigma \{ x \leadsto 23 \} \end{aligned}

If-Else

$${ (b, \sigma) \rightarrow (b', \sigma) \over (\textbf{if } b \textbf{ then } c_0 \textbf{ else } c_1, \sigma) \rightarrow (\textbf{if } b' \textbf{ then } c_0 \textbf{ else } c_1, \sigma') }$$

$${ \over (\textbf{if true then } c_0 \textbf{ else } c_1, \sigma) \rightarrow (c_0, \sigma') }$$

$${ \over (\textbf{if false then } c_0 \textbf{ else } c_1, \sigma) \rightarrow (c_1, \sigma') }$$

While-Do

$${ \over (\textbf{while } b \textbf{ do } c, \sigma) \rightarrow (\textbf{if } b \textbf{ then } (c; \textbf{while } b \textbf{ do } c) \textbf{ else skip}, \sigma)}$$

Zero-or-multiple Steps

Define $\longrightarrow^*$ as the reflexive transivtive closure of $\longrightarrow$.

$n$-step transitions:

$${ \over (c, \sigma) \longrightarrow^0 (c, \sigma)}$$

$${(c, \sigma) \longrightarrow^0 (c', \sigma') \ \ \ \ (c', \sigma') \longrightarrow^n (c'', \sigma'') \over (c, \sigma) \longrightarrow^{n+1} (c'', \sigma'')}$$

We have $(c, \sigma) \longrightarrow^* (c', \sigma')$ if and only if exists $n$ that $(c, \sigma) \longrightarrow^n (c', \sigma')$.

Some Facts About $\longrightarrow$

• Theorem (Determinism): If $(c, \sigma) \longrightarrow (c', \sigma')$ and $(c, \sigma) \longrightarrow (c'', \sigma'')$, then $(c', \sigma') = (c'', \sigma'')$.
• Corollary (Confluence): If $(c, \sigma) \longrightarrow^* (c', \sigma')$ and $(c, \sigma) \longrightarrow^* (c'', \sigma'')$, then there exists $c'''$ and $\sigma'''$ such that $(c', \sigma') \longrightarrow (c''', \sigma''')$ and $(c'', \sigma'') \longrightarrow (c''', \sigma''')$.
• Normalization: there are no infinite sequences of configurations. Every evaluation path eventually reaches a normal form.

Normal forms:

• For expressions, the normal forms are $(\textbf{n}, \sigma)$ for numeral $\textbf{n}$.
• For booleans, the normal forms are $(\textbf{true}, \sigma)$ and $(\textbf{false}, \sigma)$.

However, the transition relation on $(c, \sigma)$ is not normalizing. (we can have infinite loops). o Theorem: for any state $\sigma$, there is no $\sigma'$ such that $$(\textbf{while true do skip}, \sigma) \longrightarrow^* \sigma'$$

Going Wrong

Introduce another configuration: $\textbf{abort}$.

The following will lead to $\textbf{abort}$:

• Divide by 0
• Access non-existing data

$\textbf{abort}$ cannot step anymore.

Going wrong is not going stuck.

Local Variable Declaration

Statements:

$$c ::= \dots \vert \textbf{newvar } x := e \textbf{ in } c$$

An unsatisfactory attempt:

$${ \sigma x = \lfloor \textbf{n} \rfloor \over (\textbf{newvar } x := e \textbf{ in } c, \sigma) \longrightarrow (x := e; c; x := \textbf{n}, \sigma)}$$

is unsatisfactory because the value of local variable $x$ could be exposed to external observers while $c$ is executing. This is a problem when we have concurrency.

Big-Step Semantics

Big-step semantics describes the overall result of the execution:

$${\over (\textbf{n}, \sigma) \Downarrow \lfloor \textbf{n} \rfloor}$$

$${\sigma x = n \over (x, \sigma) \Downarrow n}$$

$${(e_1, \sigma) \Downarrow n_1 \ \ \ \ (e_2, n) \Downarrow n_2 \over (e_1 \textbf{ op } e_2, \sigma) \Downarrow n_1 \lfloor \textbf{op} \rfloor n_2}$$

Some Facts About $\Downarrow$

Theorem (Determinism): for all $e, \sigma, n, n'$, if $(e, \sigma) \Downarrow n$ and $(e, \sigma) \Downarrow n'$, then $n = n'$.

Theorem (Totality): for all $e, \sigma$, there exists $n$ such that $(e, \sigma) \Downarrow n$.

THeorem (Equivalence to small-step semantics): $$(e, \sigma) \Downarrow \lfloor \textbf{n} \rfloor \text{ iff } (e, \sigma) \longrightarrow^* (\textbf{n}, \sigma)$$