summaryrefslogtreecommitdiff
path: root/ruleslambda.tex
diff options
context:
space:
mode:
authorCamil Staps2016-04-28 15:58:48 +0200
committerCamil Staps2016-04-28 15:58:48 +0200
commitbb7ef3b4fd0b9fce274039d1eb6edc7c28c97084 (patch)
tree41d18e0a8b8862d8ec1ae16f399b651211b97d90 /ruleslambda.tex
parentFix Get regel (diff)
Labda regel
Diffstat (limited to 'ruleslambda.tex')
-rw-r--r--ruleslambda.tex17
1 files changed, 17 insertions, 0 deletions
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}
+$$
+