diff options
| -rw-r--r-- | rules.tex | 1 | ||||
| -rw-r--r-- | ruleslambda.tex | 17 | ||||
| -rw-r--r-- | smurf.sty | 3 |
3 files changed, 20 insertions, 1 deletions
@@ -12,6 +12,7 @@ afleidingsboom te maken (in tegenstelling tot bijvoorbeeld een errorstatus aan de rechterkant van transities toe te voegen), omdat dit het redeneren over Smurfprogramma's makkelijker zal maken. +\input{ruleslambda} %\input{rulespush} \input{ruleshead} %\input{rulestail} diff --git a/ruleslambda.tex b/ruleslambda.tex new file mode 100644 index 0000000..3556610 --- /dev/null +++ b/ruleslambda.tex @@ -0,0 +1,17 @@ +% vim: set spelllang=nl: +\subsection{$\lambda$} + +We hebben één axioma nodig om het basisgeval van het lege programma af te +handelen. Deze regel geeft aan dat het lege programma niets doet: het gebruikt +geen input, geeft geen output, en verandert de state niet. + +$$ +\begin{prooftree} + \axjustifies + \trans + {\lambda}{\ip}{\st} + {\ip}{\Nil}{\st} + \using{\rlambdans} +\end{prooftree} +$$ + @@ -2,6 +2,7 @@ % General \def\isdef{\stackrel{\text{def}}{=}} +\def\axjustifies{\thickness0em\justifies} % Parsing \def\parsepgmop{\mathit{Parse}} @@ -57,12 +58,12 @@ % Rules \def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]} +\def\rlambdans{\rule{$\lambda$}{ns}} \def\rheadns{\rule{head}{ns}} \def\rgetns{\rule{get}{ns}} \def\rputns{\rule{put}{ns}} \def\rinputns{\rule{input}{ns}} \def\routputns{\rule{output}{ns}} - \def\rexecns{\rule{exec}{ns}} % Common names |