summaryrefslogtreecommitdiff
path: root/tex/thesis/litreview
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/litreview')
-rw-r--r--tex/thesis/litreview/litreview.tex65
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}