diff options
| -rw-r--r-- | tex/thesis/litreview/litreview.tex | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex index bde7160..f54ed97 100644 --- a/tex/thesis/litreview/litreview.tex +++ b/tex/thesis/litreview/litreview.tex @@ -2,6 +2,7 @@ \newcommand{\PP}{\mathsf{PP}} \newcommand{\States}{\mathsf{States}} \newcommand{\state}{\mathsf{state}} +\renewcommand{\b}[1]{\mathbf{#1}} \chapter{Literature Review} \label{chap:litreview} @@ -23,40 +24,40 @@ assignment, conditional or loop as having the denotation $\llb s \rrb: \rrb = \llb s_2 \rrb \circ \llb s_1 \rrb$. As an example, we'll define some denotational semantics for a simple -language. Here our $\state$ will be a partial function $\state: I \to N$ +language. Here our $\state$ will be a partial function $\state: I \to \N$ \newcommand\halfpage[1]{\begin{minipage}{0.45\textwidth}#1\end{minipage}} \newcommand\halfpages[2]{\halfpage{#1}\hfill\halfpage{#2}} \begin{figure}[here] \halfpages{Syntax:}{Semantics:} \halfpages{ - $P :: S$ + $P::= S$ }{ - $P: \state \to \state$ \\ - $P\llb S \rrb = S\llb S \rrb \{\}$ + $\b{P}: \state \to \state$ \\ + $\b{P}\llb S \rrb = S\llb S \rrb \{\}$ } \halfpages{ $S ::= S_1;S_2 \mid if ~B~ then ~S_1~ else ~S_2~ \mid I := E$ }{ - $S: \state \to \state$ \\ - $S\llb S_1;S_2 \rrb = \lambda v . (S\llb S_2 \rrb (S\llb S_1 \rrb(s)))$ \\ - $S\llb if ~B~ then ~S_1~ else ~S_2~ \rrb = \lambda v . (S \llb S_b \rrb(v))$ \\ - where $b = B\llb B \rrb (v) + 1$ \\ - $S\llb I := E \rrb = \lambda v: (v \oplus \{ I \mapsto E \})$ + $\b{S}: \state \to \state$ \\ + $\b{S}\llb S_1;S_2 \rrb = \lambda v . (S\llb S_2 \rrb (S\llb S_1 \rrb(s)))$ \\ + $\b{S}\llb if ~B~ then ~S_1~ else ~S_2~ \rrb = \lambda v . (S \llb S_b \rrb(v))$ \\ + where $b = \b{B}\llb B \rrb (v) + 1$ \\ + $\b{S}\llb I := E \rrb = \lambda v: (v \oplus \{ I \mapsto E \})$ } \halfpages{ $E ::= E_1 + E_2 \mid I \mid N$ }{ - $E: \state \to \N$ \\ - $E\llb E_1 + E_2 \rrb = \lambda v . (E\llb E_1 \rrb(v) + E\llb E_2 \rrb(v))$ \\ - $E\llb I \rrb = \lambda v . v(I)$ \\ - $E\llb N \rrb = \lambda v . N$ + $\b{E}: \state \to \N$ \\ + $\b{E}\llb E_1 + E_2 \rrb = \lambda v . (E\llb E_1 \rrb(v) + E\llb E_2 \rrb(v))$ \\ + $\b{E}\llb I \rrb = \lambda v . v(I)$ \\ + $\b{E}\llb N \rrb = \lambda v . N$ } \halfpages{ $B ::= E_1 = E_2 \mid \lnot B$ }{ - $B: \state \to \{0,1\}$ \\ - $B\llb E_1 = E_2 \rrb = \lambda v . (if ~\llb E_1 \rrb(v) = \llb E_2 \rrb(v) ~then~ 1 ~else~ 0)$ + $\b{B}: \state \to \{0,1\}$ \\ + $\b{B}\llb E_1 = E_2 \rrb = \lambda v . (if ~\llb E_1 \rrb(v) = \llb E_2 \rrb(v) ~then~ 1 ~else~ 0)$ } \halfpages{ $I ::= $ variable identifier |