defio.tex


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

% vim: set spelllang=nl:
\subsection{Input en output}
\label{sec:def:io}

Allereerst definiëren we het type $\Stack{a}$. De stack is onmisbaar voor
nagenoeg elk Smurfprogramma en zullen we dus ook veel gebruiken in onze
semantiekregels. Een $\Stack{a}$ (lees: een stack van elementen van type $a$)
is een simpel datatype met de volgende syntax:

\def\inbrackets#1{$\mathrm{[}#1\mathrm{]}$}
\def\bracka{\inbrackets{a}}
\def\StackA{{\normalfont\textbf{Stack}} \bracka}
\begin{grammar}
	<\StackA> ::= [<a>:<\StackA>] | \Nil
\end{grammar}

Op een stack zijn twee instructies gedefinieerd:
\begin{gather*}
	\pushop : a \times \Stack{a} \to \Stack{a} \\
	\push{e}{\stk} \isdef [e:\stk] \\[1em]
	\popop : \Stack{a} \hookrightarrow a \times \Stack{a} \\
	\pop{[e:\stk]} \isdef (e,\stk) \\
\end{gather*}

In de documentatie \cite{safalra} wordt niet beschreven wat er gebeurt wanneer
een $\popop$ wordt uitgevoerd op een lege stack. In de Perl-interpreter van de
taal wordt ervoor gekozen om het programma abrupt te termineren met een error.
Wij hebben ervoor gekozen om $\popop$ als een partiële functie te zien waar
$\pop\Nil$ ongedefinieerd blijft zodat er geen afleidingsbomen bestaan voor
programma's waar dit gebeurt.

\medskip
We zullen de input en output beide als $\Stack{\String}$ modelleren. In feite
zal zelfs blijken dat we op $\Input$ de operatie $\pushop$ niet nodig hebben,
en op $\Output$ de operatie $\popop$ niet zullen gebruiken. Informeel
beschouwen we $\Input$ als een `bron' van $\String$s en $\Output$ als een `put'
van $\String$s. Formeel:

\begin{align*}
	\Input &\isdef \Stack{\String} \\ \Output &\isdef \Stack{\String}
\end{align*}