Fix two references.
[matthijs/master-project/report.git] / Chapters / Normalization.tex
index 0f6d0eb23ecdff6c32920ee5b4ea20b6ee67ec68..db743fc9a049d716c931747ca7cb09180723980a 100644 (file)
 
         \startbuffer[from]
         (+) :: Word -> Word -> Word
 
         \startbuffer[from]
         (+) :: Word -> Word -> Word
-        (+) = GHC.Num.(+) @Word $dNum
+        (+) = GHC.Num.(+) @Word \$dNum
         ~
         (+) a b
         \stopbuffer
         \startbuffer[to]
         ~
         (+) a b
         \stopbuffer
         \startbuffer[to]
-        GHC.Num.(+) @ Alu.Word $dNum a b
+        GHC.Num.(+) @ Alu.Word \$dNum a b
         \stopbuffer
 
         \transexample{toplevelinline}{Top level binding inlining}{from}{to}
         \stopbuffer
 
         \transexample{toplevelinline}{Top level binding inlining}{from}{to}
         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
         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}
 
         Since both type and dictionary arguments are not representable,
         \refdef{representable}
         η-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
         η-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:
 
         example, the \lam{q} and \lam{r} variable will be propagated into the
         let expression and then into the case expression:
 
         expression shows an example:
 
         \startlambda
         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
 
 
         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
         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
 
         When faced with a user defined function, a body is available for that
         function. This means we could create a specialized version of the
         Applying this transformation to the example gives:
 
         \startlambda
         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
 
         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
         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
         \stoplambda
 
         This example also shows that the resulting normal form might not be as