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

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

Allereerst definiëren we het type $\Stack{a}$, omdat stacks veel voorkomen in
Smurf. Een $\Stack{a}$ (lees: een stack van elementen van type $a$) is een
simpel datatype met de volgende syntax:

\begin{grammar}
	<Stack[a]> ::= [<a>:<Stack[a]>] | `Nil'
	%todo formatting
\end{grammar}

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

$\popop$ is een partiële functie omdat $\pop\Nil$ niet gedefinieerd is.

\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*}