X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=db743fc9a049d716c931747ca7cb09180723980a;hp=e2f3a968dec9a656c8970f2439375e6ec7868302;hb=b1a9ce14b51423bf676df768278fd6b6d6579ca1;hpb=feee31da167a3c0505d2683d3e81e2597743f1a6

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index e2f3a96..db743fc 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -1610,8 +1610,7 @@
         simply inline the let bindings that have a polymorphic type,
         which should (eventually) make sure that the polymorphic
         expression is applied to a type and/or dictionary, which can
-        \refdef{beta-reduction}
-        then be removed by β-reduction.
+        then be removed by β-reduction (\in{section}[sec:normalization:beta]).
 
         Since both type and dictionary arguments are not representable,
         \refdef{representable}
@@ -1713,7 +1712,7 @@
         η-abstraction 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:approp]). In our
+        transformation (\in{section}[sec:normalization:appprop]). In our
         example, the \lam{q} and \lam{r} variable will be propagated into the
         let expression and then into the case expression:
 
@@ -1788,17 +1787,17 @@
         expression shows an example:
 
         \startlambda
-        app2 :: (Word -> Word) -> Word -> Word
-        app2 = λf.λa.f (f a)
+        twice :: (Word -> Word) -> Word -> Word
+        twice = λf.λa.f (f a)
 
         main = λa.app (λx. x + x) a
         \stoplambda
 
-        This example shows a function \lam{app2} that takes a function as a
+        This example shows a function \lam{twice} that takes a function as a
         first argument and applies that function twice to the second argument.
         Again, we've made the function monomorphic for clarity, even though
         this function would be a lot more useful if it was polymorphic. The
-        function \lam{main} uses \lam{app2} to apply a lambda epression twice.
+        function \lam{main} uses \lam{twice} to apply a lambda epression twice.
 
         When faced with a user defined function, a body is available for that
         function. This means we could create a specialized version of the
@@ -1808,23 +1807,23 @@
         Applying this transformation to the example gives:
 
         \startlambda
-        app2' :: Word -> Word
-        app2' = λb.(λf.λa.f (f a)) (λx. x + x) b
+        twice' :: Word -> Word
+        twice' = λb.(λf.λa.f (f a)) (λx. x + x) b
 
         main = λa.app' a
         \stoplambda
 
         The \lam{main} function is now in normal form, since the only higher
         order value there is the top level lambda expression. The new
-        \lam{app2'} function is a bit complex, but the entire original body of
-        the original \lam{app2} function is wrapped in a lambda abstraction
+        \lam{twice'} function is a bit complex, but the entire original body of
+        the original \lam{twice} function is wrapped in a lambda abstraction
         and applied to the argument we've specialized for (\lam{λx. x + x})
         and the other arguments. This complex expression can fortunately be
         effectively reduced by repeatedly applying β-reduction: 
 
         \startlambda
-        app2' :: Word -> Word
-        app2' = λb.(b + b) + (b + b)
+        twice' :: Word -> Word
+        twice' = λb.(b + b) + (b + b)
         \stoplambda
 
         This example also shows that the resulting normal form might not be as