Labda regel

3 files changed, 20 insertions, 1 deletions

diff --git a/rules.tex b/rules.tex
index b6acb25..d17c1d6 100644
--- a/rules.tex
+++ b/rules.tex
@@ -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}
+$$
+
diff --git a/smurf.sty b/smurf.sty
index 78d1bbd..de227bf 100644
--- a/smurf.sty
+++ b/smurf.sty
@@ -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