X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=b74333ae103c15d51b08fa37cc708cc7c3f1503b;hp=445c32389ad91ccd8f874ddbd49ebb8f7fa71682;hb=951d8f0c4551cbc1adc75c80ae21c86bee6d1e80;hpb=35ce834593526d613598a431723cd5be7fe440af

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 445c323..b74333a 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -15,10 +15,6 @@
 }
 
 
-% A transformation example
-\definefloat[example][examples]
-\setupcaption[example][location=top] % Put captions on top
-
 \define[3]\transexample{
   \placeexample[here]{#1}
   \startcombination[2*1]
@@ -606,31 +602,44 @@ notations, which we will define here.
 
 \subsubsection{Other concepts}
 A \emph{global variable} is any variable that is bound at the
-top level of a program, or an external module. A local variable is any other
-variable (\eg, variables local to a function, which can be bound by lambda
-abstractions, let expressions and case expressions).
-
-A \emph{hardware representable} type is a type that we can generate
-a signal for in hardware. For example, a bit, a vector of bits, a 32 bit
-unsigned word, etc. Types that are not runtime representable notably
-include (but are not limited to): Types, dictionaries, functions.
-
-A \emph{builtin function} is a function for which a builtin
-hardware translation is available, because its actual definition is not
-translatable. A user-defined function is any other function.
+top level of a program, or an external module. A \emph{local variable} is any
+other variable (\eg, variables local to a function, which can be bound by
+lambda abstractions, let expressions and pattern matches of case
+alternatives).  Note that this is a slightly different notion of global versus
+local than what \small{GHC} uses internally.
+\defref{global variable} \defref{local variable}
+
+A \emph{hardware representable} (or just \emph{representable}) type or value
+is (a value of) a type that we can generate a signal for in hardware. For
+example, a bit, a vector of bits, a 32 bit unsigned word, etc. Types that are
+not runtime representable notably include (but are not limited to): Types,
+dictionaries, functions.
+\defref{representable}
+
+A \emph{builtin function} is a function supplied by the Cλash framework, whose
+implementation is not valid Cλash. The implementation is of course valid
+Haskell, for simulation, but it is not expressable in Cλash.
+\defref{builtin function} \defref{user-defined function}
+
+For these functions, Cλash has a \emph{builtin hardware translation}, so calls
+to these functions can still be translated. These are functions like
+\lam{map}, \lam{hwor} and \lam{length}.
+
+A \emph{user-defined} function is a function for which we do have a Cλash
+implementation available.
 
 \subsubsection{Functions}
 Here, we define a number of functions that can be used below to concisely
 specify conditions.
 
-\emph{gvar(expr)} is true when \emph{expr} is a variable that references a
+\refdef{global variable}\emph{gvar(expr)} is true when \emph{expr} is a variable that references a
 global variable. It is false when it references a local variable.
 
-\emph{lvar(expr)} is the inverse of \emph{gvar}; it is true when \emph{expr}
+\refdef{local variable}\emph{lvar(expr)} is the complement of \emph{gvar}; it is true when \emph{expr}
 references a local variable, false when it references a global variable.
 
-\emph{representable(expr)} or \emph{representable(var)} is true when
-\emph{expr} or \emph{var} has a type that is representable at runtime.
+\refdef{representable}\emph{representable(expr)} or \emph{representable(var)} is true when
+\emph{expr} or \emph{var} is \emph{representable}.
 
 \subsection{Binder uniqueness}
 A common problem in transformation systems, is binder uniqueness. When not
@@ -771,21 +780,66 @@ foo = λa.λx.(case a of
 
 \transexample{η-abstraction}{from}{to}
 
-\subsection{Extended β-reduction}
+\subsection{β-reduction}
+β-reduction is a well known transformation from lambda calculus, where it is
+the main reduction step. It reduces applications of labmda abstractions,
+removing both the lambda abstraction and the application.
+
+In our transformation system, this step helps to remove unwanted lambda
+abstractions (basically all but the ones at the top level). Other
+transformations (application propagation, non-representable inlining) make
+sure that most lambda abstractions will eventually be reducable by
+β-reduction.
+
+TODO: Define substitution syntax
+
+\starttrans
+(λx.E) M
+-----------------
+E[M/x]
+\stoptrans
+
+% And an example
+\startbuffer[from]
+(λa. 2 * a) (2 * b)
+\stopbuffer
+
+\startbuffer[to]
+2 * (2 * b)
+\stopbuffer
+
+\transexample{β-reduction}{from}{to}
+
+\subsection{Application propagation}
 This transformation is meant to propagate application expressions downwards
-into expressions as far as possible. In lambda calculus, this reduction
-is known as β-reduction, but it is of course only defined for
-applications of lambda abstractions. We extend this reduction to also
-work for the rest of core (case and let expressions).
+into expressions as far as possible. This allows partial applications inside
+expressions to become fully applied and exposes new transformation
+possibilities for other transformations (like β-reduction).
 
-For let expressions:
 \starttrans
 let binds in E) M
 -----------------
 let binds in E M
 \stoptrans
 
-For case statements:
+% And an example
+\startbuffer[from]
+( let 
+    val = 1
+  in 
+    add val
+) 3
+\stopbuffer
+
+\startbuffer[to]
+let 
+  val = 1
+in 
+  add val 3
+\stopbuffer
+
+\transexample{Application propagation for a let expression}{from}{to}
+
 \starttrans
 (case x of
   p1 -> E1
@@ -798,35 +852,21 @@ case x of
   pn -> En M
 \stoptrans
 
-For lambda expressions:
-\starttrans
-(λx.E) M
------------------
-E[M/x]
-\stoptrans
-
 % And an example
 \startbuffer[from]
-( let a = (case x of 
-            True -> id
-            False -> neg
-          ) 1
-      b = (let y = 3 in add y) 2
-  in
-    (λz.add 1 z)
-) 3
+( case x of 
+    True -> id
+    False -> neg
+) 1
 \stopbuffer
 
 \startbuffer[to]
-let a = case x of 
-           True -> id 1
-           False -> neg 1
-    b = let y = 3 in add y 2
-in
-  add 1 3
+case x of 
+  True -> id 1
+  False -> neg 1
 \stopbuffer
 
-\transexample{Extended β-reduction}{from}{to}
+\transexample{Application propagation for a case expression}{from}{to}
 
 \subsection{Let derecursification}
 This transformation is meant to make lets non-recursive whenever possible.
@@ -842,7 +882,7 @@ in scope for the function return value).
 Note that this transformation does not try to be smart when faced with
 recursive lets, it will just leave the lets recursive (possibly joining a
 recursive and non-recursive let into a single recursive let). The let
-rederursification transformation will do this instead.
+rederecursification transformation will do this instead.
 
 \starttrans
 letnonrec x = (let bindings in M) in N