Add sitenote about arguments vs. inputs.

[matthijs/master-project/report.git] / Chapters / Normalization.tex

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 8de37949200931e5eeae8d337b29e949e03843f9..d564d231405a00ab7f31622ef525b15f987c2218 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -1441,6 +1441,9 @@
         this.
 
     \subsection{Case normalisation}
+      The transformations in this section ensure that case statements end up
+      in normal form.
+
       \subsubsection{Scrutinee simplification}
         This transform ensures that the scrutinee of a case expression is always
         a simple variable reference.
@@ -1470,10 +1473,31 @@
         \transexample{letflat}{Case normalisation}{from}{to}
 
 
+        \placeintermezzo{}{
+          \defref{wild binders}
+          \startframedtext[width=7cm,background=box,frame=no]
+          \startalignment[center]
+            {\tfa Wild binders}
+          \stopalignment
+          \blank[medium]
+            In a functional expression, a \emph{wild binder} refers to any
+            binder that is never referenced. This means that even though it
+            will be bound to a particular value, that value is never used.
+
+            The Haskell syntax offers the underscore as a wild binder that
+            cannot even be referenced (It can be seen as introducing a new,
+            anonymous, binder everytime it is used).
+            
+            In these transformations, the term wild binder will sometimes be
+            used to indicate that a binder must not be referenced.
+          \stopframedtext
+        }
+
       \subsubsection{Case normalization}
         This transformation ensures that all case expressions get a form
         that is allowed by the intended normal form. This means they
-        will become one of: \refdef{intended normal form definition}
+        will become one of:
+
         \startitemize
         \item An extractor case with a single alternative that picks a field
         from a datatype, \eg\ \lam{case x of (a, b) -> a}.
@@ -1515,7 +1539,6 @@
             Cn wn,0 ... wn,m -> yn
         \stoptrans
 
-        \refdef{wild binder}
         Note that this transformation applies to case expressions with any
         scrutinee. If the scrutinee is a complex expression, this might
         result in duplication of work (hardware). An extra condition to
@@ -1567,7 +1590,7 @@
 
       \subsubsection[sec:transformation:caseremoval]{Case removal}
         This transform removes any case expression with a single alternative and
-        only wild binders.\refdef{wild binder}
+        only wild binders.\refdef{wild binders}
 
         These "useless" case expressions are usually leftovers from case simplification
         on extractor case (see the previous example).
@@ -2217,11 +2240,13 @@
     developed in the final part of the research, leaving no more time
     for verifying these properties. In fact, it is likely that the
     current transformation system still violates some of these
-    properties in some cases and should be improved (or extra conditions
-    on the input hardware descriptions should be formulated).
+    properties in some cases (see
+    \in{section}[sec:normalization:non-determinism] and
+    \in{section}[sec:normalization:stateproblems]) and should be improved (or
+    extra conditions on the input hardware descriptions should be formulated).
 
     This is most likely the case with the completeness and determinism
-    properties, perhaps als the termination property. The soundness
+    properties, perhaps also the termination property. The soundness
     property probably holds, since it is easier to manually verify (each
     transformation can be reviewed separately).
 
@@ -2418,7 +2443,7 @@
       each node in the normal set is also in the intended normal set.
       Reasoning about our intended normal set is easier, since we know
       how to generate it from its definition. \refdef{intended normal
-      form definition}.
+      form definition}
 
       Fortunately, we can also prove the complement (which is
       equivalent, since $A \subseteq B \Leftrightarrow \overline{B}