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

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

Allereerst definiëren we het type $\Stack{a}$, omdat we veel met stacks
doen 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}}
\begin{grammar}
	<Stack \bracka> ::= [<a>:<Stack \bracka>] | \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
\emph{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*}