diff options
Diffstat (limited to 'tex/thesis')
| -rw-r--r-- | tex/thesis/litreview/litreview.tex | 65 |
1 files changed, 30 insertions, 35 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex index f54ed97..1ac34d5 100644 --- a/tex/thesis/litreview/litreview.tex +++ b/tex/thesis/litreview/litreview.tex @@ -25,46 +25,41 @@ assignment, conditional or loop as having the denotation $\llb s \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$ -\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$ - }{ +\begin{figure}[H] + \begin{minipage}{\textwidth} + Syntax: + \end{minipage} \\[0.1cm] + \begin{minipage}{0.8\textwidth} + $P ::= S$ \\ + $S ::= S_1;S_2 \mid \b{if}~ B ~\b{then}~ S_1 ~\b{else~} S_2 \mid I := E$ \\ + $E ::= E_1 + E_2 \mid I \mid N$ \\ + $B ::= E_1 = E_2 \mid \lnot B$ \\ + $I ::= $ variable identifiers \\ + $N ::= \N$ + \end{minipage} + \\[0.5cm] + \begin{minipage}{\textwidth} + Semantics: + \end{minipage} \\[0.1cm] + \begin{minipage}{0.8\textwidth} $\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$ - }{ + $\b{P}\llb S \rrb = \b{S}\llb S \rrb \{\}$ \\[0.2cm] + $\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$ - }{ + $\b{S}\llb S_1;S_2 \rrb = \lambda v . (\b{S}\llb S_2 \rrb (\b{S}\llb S_1 \rrb(v)))$ \\ + $\b{S}\llb \b{if}~ B ~\b{then}~ S_1 ~\b{else~} S_2 \rrb = \lambda v . (\b{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 \b{E}\llb E \rrb(v) \})$ \\[0.2cm] + $\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 E_1 + E_2 \rrb = \lambda v . (\b{E}\llb E_1 \rrb(v) + \b{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{E}\llb N \rrb = \lambda v . N$ \\[0.2cm] + $\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 - }{~} - \halfpages{ - $N ::= \N$ - }{~} + $\b{B}\llb E_1 = E_2 \rrb = \lambda v . (\b{if}~ \b{E}\llb E_1 \rrb(v) = \b{E}\llb E_2 \rrb(v) ~\b{then}~ 1 ~\b{else}~ 0)$ + \end{minipage} + \caption{Denotational semantics for a simple language.} \label{fig:denotational-semantics-example} \end{figure} |