Replace a starttyping with starthaskell.

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

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 2768ba2c0a2c89e87e989471bd5d7a3c53ea5e4c..a1dec0a854efabd08ff58e32c07b2d3845dd99b4 100644 (file)
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -473,8 +473,8 @@
       \stopdesc
 
     To understand this notation better, the step by step application of
       \stopdesc
 
     To understand this notation better, the step by step application of

-    the η-abstraction transformation to a simple \small{ALU} will be
-    shown. Consider η-abstraction, which is a common transformation from
+    the η-expansion transformation to a simple \small{ALU} will be
+    shown. Consider η-expansion, which is a common transformation from

     labmda calculus, described using above notation as follows:
 
     \starttrans
     labmda calculus, described using above notation as follows:
 
     \starttrans


@@ -483,12 +483,12 @@
     λx.E x            \lam{E} is not a lambda abstraction.
     \stoptrans
 
     λx.E x            \lam{E} is not a lambda abstraction.
     \stoptrans
 

-    η-abstraction is a well known transformation from lambda calculus. What
+    η-expansion is a well known transformation from lambda calculus. What

     this transformation does, is take any expression that has a function type
     and turn it into a lambda expression (giving an explicit name to the
     argument). There are some extra conditions that ensure that this
     transformation does not apply infinitely (which are not necessarily part
     this transformation does, is take any expression that has a function type
     and turn it into a lambda expression (giving an explicit name to the
     argument). There are some extra conditions that ensure that this
     transformation does not apply infinitely (which are not necessarily part

-    of the conventional definition of η-abstraction).
+    of the conventional definition of η-expansion).

 
     Consider the following function, in Core notation, which is a fairly obvious way to specify a
     simple \small{ALU} (Note that it is not yet in normal form, but
 
     Consider the following function, in Core notation, which is a fairly obvious way to specify a
     simple \small{ALU} (Note that it is not yet in normal form, but


@@ -632,7 +632,7 @@
     \stoplambda
 
     The other alternative is left as an exercise to the reader. The final
     \stoplambda
 
     The other alternative is left as an exercise to the reader. The final

-    function, after applying η-abstraction until it does no longer apply is:
+    function, after applying η-expansion until it does no longer apply is:

 
     \startlambda 
     alu :: Bit -> Word -> Word -> Word
 
     \startlambda 
     alu :: Bit -> Word -> Word -> Word


@@ -820,41 +820,41 @@
     \in{section}[sec:normalization:transformation].
 
     \subsection{General cleanup}
     \in{section}[sec:normalization:transformation].
 
     \subsection{General cleanup}

-      These transformations are general cleanup transformations, that aim to
-      make expressions simpler. These transformations usually clean up the
-       mess left behind by other transformations or clean up expressions to
-       expose new transformation opportunities for other transformations.
-
-       Most of these transformations are standard optimizations in other
-       compilers as well. However, in our compiler, most of these are not just
-       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]
+      \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:

 
 

-          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.
+        \startlambda
+          E[A=>B]
+        \stoplambda

 
 

-          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:
+        This means expression \lam{E} with all occurences of \lam{A} replaced
+        with \lam{B}.
+        \stopframedtext
+      }

 
 

-          \startlambda
-            E[A=>B]
-          \stoplambda
+      These transformations are general cleanup transformations, that aim to
+      make expressions simpler. These transformations usually clean up the
+      mess left behind by other transformations or clean up expressions to
+      expose new transformation opportunities for other transformations.

 
 

-          This means expression \lam{E} with all occurences of \lam{A} replaced
-          with \lam{B}.
-          \stopframedtext
-        }
+      Most of these transformations are standard optimizations in other
+      compilers as well. However, in our compiler, most of these are not just
+      optimizations, but they are required to get our program into intended
+      normal form.

 
       \subsubsection[sec:normalization:beta]{β-reduction}
         β-reduction is a well known transformation from lambda calculus, where it is
 
       \subsubsection[sec:normalization:beta]{β-reduction}
         β-reduction is a well known transformation from lambda calculus, where it is


@@ -1099,7 +1099,7 @@
       of the other value definitions in let bindings and making the final
       return value a simple variable reference.
 
       of the other value definitions in let bindings and making the final
       return value a simple variable reference.
 

-      \subsubsection[sec:normalization:eta]{η-abstraction}
+      \subsubsection[sec:normalization:eta]{η-expansion}

         This transformation makes sure that all arguments of a function-typed
         expression are named, by introducing lambda expressions. When combined with
         β-reduction and non-representable binding inlining, all function-typed
         This transformation makes sure that all arguments of a function-typed
         expression are named, by introducing lambda expressions. When combined with
         β-reduction and non-representable binding inlining, all function-typed


@@ -1123,7 +1123,7 @@
             False -> λy.id y) x
         \stopbuffer
 
             False -> λy.id y) x
         \stopbuffer
 

-        \transexample{eta}{η-abstraction}{from}{to}
+        \transexample{eta}{η-expansion}{from}{to}

 
       \subsubsection[sec:normalization:appprop]{Application propagation}
         This transformation is meant to propagate application expressions downwards
 
       \subsubsection[sec:normalization:appprop]{Application propagation}
         This transformation is meant to propagate application expressions downwards


@@ -1284,7 +1284,7 @@
         Note that the return value is not simplified if its not
         representable.  Otherwise, this would cause a direct loop with
         the inlining of unrepresentable bindings. If the return value is
         Note that the return value is not simplified if its not
         representable.  Otherwise, this would cause a direct loop with
         the inlining of unrepresentable bindings. If the return value is

-        not representable because it has a function type, η-abstraction
+        not representable because it has a function type, η-expansion

         should make sure that this transformation will eventually apply.
         If the value is not representable for other reasons, the
         function result itself is not representable, meaning this
         should make sure that this transformation will eventually apply.
         If the value is not representable for other reasons, the
         function result itself is not representable, meaning this


@@ -1776,11 +1776,11 @@
         lambda abstraction.
 
         To reduce all higher-order values to one of the above items, a number
         lambda abstraction.
 
         To reduce all higher-order values to one of the above items, a number

-        of transformations we have already seen are used. The η-abstraction
+        of transformations we have already seen are used. The η-expansion

         transformation from \in{section}[sec:normalization:eta] ensures all
         function arguments are introduced by lambda abstraction on the highest
         level of a function. These lambda arguments are allowed because of
         transformation from \in{section}[sec:normalization:eta] ensures all
         function arguments are introduced by lambda abstraction on the highest
         level of a function. These lambda arguments are allowed because of

-        \in{item}[item:toplambda] above. After η-abstraction, our example
+        \in{item}[item:toplambda] above. After η-expansion, our example

         becomes a bit bigger:
 
         \startlambda
         becomes a bit bigger:
 
         \startlambda


@@ -1791,7 +1791,7 @@
               ) q
         \stoplambda
 
               ) q
         \stoplambda
 

-        η-abstraction also introduces extra applications (the application of
+        η-expansion also introduces extra applications (the application of

         the let expression to \lam{q} in the above example). These
         applications can then propagated down by the application propagation
         transformation (\in{section}[sec:normalization:appprop]). In our
         the let expression to \lam{q} in the above example). These
         applications can then propagated down by the application propagation
         transformation (\in{section}[sec:normalization:appprop]). In our


@@ -1810,8 +1810,8 @@
         representable type). Completely applied top level functions (like the
         first alternative) are now no longer invalid (they fall under
         \in{item}[item:completeapp] above). (Completely) applied lambda
         representable type). Completely applied top level functions (like the
         first alternative) are now no longer invalid (they fall under
         \in{item}[item:completeapp] above). (Completely) applied lambda

-        abstractions can be removed by β-abstraction. For our example,
-        applying β-abstraction results in the following:
+        abstractions can be removed by β-expansion. For our example,
+        applying β-expansion results in the following:

 
         \startlambda
         λy.λq.let double = λx. x + x in
 
         \startlambda
         λy.λq.let double = λx. x + x in