X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=3d53853a58129f8b8cf90e5a22b8da3f02f75d30;hp=714ce88c0c6a663b2c7cf517db11f0243718ed87;hb=901c9881c60ac1897aa8efb63d082798272e1ae7;hpb=469c28edabf61f131bd29bb76838b615a84acc9a

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 714ce88..3d53853 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -28,11 +28,7 @@
   core can describe expressions that do not have a direct hardware
   interpretation.
 
-  \todo{Describe core properties not supported in \VHDL, and describe how the
-  \VHDL we want to generate should look like.}
-
   \section{Normal form}
-    \todo{Refresh or refer to distinct hardware per application principle}
     The transformations described here have a well-defined goal: To bring the
     program in a well-defined form that is directly translatable to hardware,
     while fully preserving the semantics of the program. We refer to this form as
@@ -629,9 +625,11 @@
 
       In particular, we define no particular order of transformations. Since
       transformation order should not influence the resulting normal form,
-      \todo{This is not really true, but would like it to be...} this leaves
-      the implementation free to choose any application order that results in
-      an efficient implementation.
+      this leaves the implementation free to choose any application order that
+      results in an efficient implementation. Unfortunately this is not
+      entirely true for the current set of transformations. See
+      \in{section}[sec:normalization:non-determinism] for a discussion of this
+      problem.
 
       When applying a single transformation, we try to apply it to every (sub)expression
       in a function, not just the top level function body. This allows us to
@@ -641,8 +639,6 @@
       In the following sections, we will be using a number of functions and
       notations, which we will define here.
 
-      \todo{Define substitution (notation)}
-
       \subsubsection{Concepts}
         A \emph{global variable} is any variable (binder) that is bound at the
         top level of a program, or an external module. A \emph{local variable} is any
@@ -799,8 +795,34 @@
        optimizations, but they are required to get our program into intended
        normal form.
 
+        \placeintermezzo{}{
+          \defref{substitution notation}
+          \startframedtext[width=8cm,background=box,frame=no]
+          \startalignment[center]
+            {\tfa Substitution notation}
+          \stopalignment
+          \blank[medium]
+
+          In some of the transformations in this chapter, we need to perform
+          substitution on an expression. Substitution means replacing every
+          occurence of some expression (usually a variable reference) with
+          another expression.
+
+          There have been a lot of different notations used in literature for
+          specifying substitution. The notation that will be used in this report
+          is the following:
+
+          \startlambda
+            E[A=>B]
+          \stoplambda
+
+          This means expression \lam{E} with all occurences of \lam{A} replaced
+          with \lam{B}.
+          \stopframedtext
+        }
+
+      \defref{beta-reduction}
       \subsubsection[sec:normalization:beta]{β-reduction}
-        \defref{beta-reduction}
         β-reduction is a well known transformation from lambda calculus, where it is
         the main reduction step. It reduces applications of lambda abstractions,
         removing both the lambda abstraction and the application.
@@ -867,7 +889,8 @@
         This transformation is not needed to get an expression into intended
         normal form (since these bindings are part of the intended normal
         form), but makes the resulting \small{VHDL} a lot shorter.
-        
+       
+        \refdef{substitution notation}
         \starttrans
         letrec
           a0 = E0
@@ -1084,7 +1107,7 @@
 
         \transexample{apppropcase}{Application propagation for a case expression}{from}{to}
 
-      \subsubsection{Let recursification}
+      \subsubsection[sec:normalization:letrecurse]{Let recursification}
         This transformation makes all non-recursive lets recursive. In the
         end, we want a single recursive let in our normalized program, so all
         non-recursive lets can be converted. This also makes other
@@ -1799,6 +1822,7 @@
         solves (part of) the polymorphism, higher order values and
         unrepresentable literals in an expression.
 
+        \refdef{substitution notation}
         \starttrans
         letrec 
           a0 = E0
@@ -1990,7 +2014,7 @@
         let y = (a * b) in y + y
         \stoplambda
 
-      \subsection{Non-determinism}
+      \subsection[sec:normalization:non-determinism]{Non-determinism}
         As an example, again consider the following expression:
 
         \startlambda