Restructure some of the normalization chapter.
authorMatthijs Kooijman <matthijs@stdin.nl>
Mon, 30 Nov 2009 22:22:14 +0000 (23:22 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Mon, 30 Nov 2009 22:23:45 +0000 (23:23 +0100)
Chapters/Normalization.tex
Outline

index 3a7196d44c26ab92338c2e71a29e56097cc5223a..55e00577e393dc0c3933ecb708ad4c394d95ca5c 100644 (file)
        normal form.
 
       \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.
 
         \transexample{argextract}{Argument extraction}{from}{to}
       
-      \subsubsection{Function extraction}
+      \subsubsection[sec:normalization:funextract]{Function extraction}
         \todo{Move to section about builtin functions}
         This transform deals with function-typed arguments to builtin
         functions.  Since builtin functions cannot be specialized to remove
 
         Note that \lam{x0} and {x1} will still need normalization after this.
 
-      \subsubsection{Argument propagation}
-        \todo{Rename this section to specialization and move it into a
-        separate section}
-
-        This transform deals with arguments to user-defined functions that are
-        not representable at runtime. This means these arguments cannot be
-        preserved in the final form and most be {\em propagated}.
-
-        Propagation means to create a specialized version of the called
-        function, with the propagated argument already filled in. As a simple
-        example, in the following program:
-
-        \startlambda
-        f = λa.λb.a + b
-        inc = λa.f a 1
-        \stoplambda
-
-        We could {\em propagate} the constant argument 1, with the following
-        result:
-
-        \startlambda
-        f' = λa.a + 1
-        inc = λa.f' a
-        \stoplambda
-
-        Special care must be taken when the to-be-propagated expression has any
-        free variables. If this is the case, the original argument should not be
-        removed completely, but replaced by all the free variables of the
-        expression. In this way, the original expression can still be evaluated
-        inside the new function. Also, this brings us closer to our goal: All
-        these free variables will be simple variable references.
-
-        To prevent us from propagating the same argument over and over, a simple
-        local variable reference is not propagated (since is has exactly one
-        free variable, itself, we would only replace that argument with itself).
-
-        This shows that any free local variables that are not runtime representable
-        cannot be brought into normal form by this transform. We rely on an
-        inlining transformation to replace such a variable with an expression we
-        can propagate again.
-
-        \starttrans
-        x = E
-        ~
-        x Y0 ... Yi ... Yn                               \lam{Yi} is not of a runtime representable type
-        ---------------------------------------------    \lam{Yi} is not a local variable reference
-        x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn            \lam{f0 ... fm} are all free local vars of \lam{Yi}
-        ~
-        x' = λy0 ... λyi-1. λf0 ... λfm. λyi+1 ... λyn .       
-              E y0 ... yi-1 Yi yi+1 ... yn   
-        \stoptrans
-
-        \todo{Describe what the formal specification means}
-        \todo{Note that we don't change the sepcialised function body, only
-        wrap it}
-
-        \todo{Example}
-
+      \todo{Fill the gap left by moving argument propagation away}
 
     \subsection{Case normalisation}
       \subsubsection{Scrutinee simplification}
 
         \transexample{caserem}{Case removal}{from}{to}
 
-  \todo{Move these two sections somewhere? Perhaps not?}
-  \subsection{Removing polymorphism}
-    Reference type-specialization (== argument propagation)
+    \subsection{Removing unrepresentable values}
+      The transformations in this section are aimed at making all the
+      values used in our expression representable. There are two main
+      transformations that are applied to \emph{all} unrepresentable let
+      bindings and function arguments, but these are really meant to
+      address three different kinds of unrepresentable values:
+      Polymorphic values, higher order values and literals. Each of these
+      will be detailed below, followed by the actual transformations.
+
+      \subsubsection{Removing Polymorphism}
+        As noted in \in{section}[sec:prototype:polymporphism],
+        polymorphism is made explicit in Core through type and
+        dictionary arguments. To remove the polymorphism from a
+        function, we can simply specialize the polymorphic function for
+        the particular type applied to it. The same goes for dictionary
+        arguments. To remove polymorphism from let bound values, we
+        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.
+
+        Since both type and dictionary arguments are not representable,
+        \refdef{representable}
+        the non-representable argument specialization and
+        non-representable let binding inlining transformations below
+        take care of exactly this.
 
-    Reference polymporphic binding inlining (== non-representable binding
-    inlining).
+        There is one case where polymorphism cannot be completely
+        removed: Builtin functions are still allowed to be polymorphic
+        (Since we have no function body that we could properly
+        specialize). However, the code that generates \VHDL for builtin
+        functions knows how to handle this, so this is not a problem.
 
-  \subsection{Defunctionalization}
-    These transformations remove most higher order expressions from our
-    program, making it completely first-order (the only exception here is for
-    arguments to builtin functions, since we can't specialize builtin
-    function. \todo{Talk more about this somewhere}
+      \subsubsection{Defunctionalization}
+        These transformations remove higher order expressions from our
+        program, making all values first-order.
 
-    Reference higher-order-specialization (== argument propagation)
+        \todo{Finish this section}
+        
+        There is one case where higher order values cannot be completely
+        removed: Builtin functions are still allowed to have higher
+        order arguments (Since we have no function body that we could
+        properly specialize). These are limited to (partial applications
+        of) top level functions, however, which is handled by the
+        top-level function extraction (see
+        \in{section}[sec:normalization:funextract]). However, the code
+        that generates \VHDL for builtin functions knows how to handle
+        these, so this is not a problem.
+
+      \subsubsection{Literals}
+        \todo{Fill this section}
 
       \subsubsection{Non-representable binding inlining}
         \todo{Move this section into a new section (together with
         non-representable types. \todo{Expand on this. This/these paragraph(s)
         should probably become a separate discussion somewhere else}
 
-        \todo{Can this duplicate work?}
+        \todo{Can this duplicate work? -- For polymorphism probably, for
+        higher order expressions only if they are inlined before they
+        are themselves normalized.}
 
         \starttrans
         letrec 
 
         \transexample{nonrepinline}{Nonrepresentable binding inlining}{from}{to}
 
+      \subsubsection{Argument propagation}
+        \todo{Rename this section to specialization}
+
+        This transform deals with arguments to user-defined functions that are
+        not representable at runtime. This means these arguments cannot be
+        preserved in the final form and most be {\em propagated}.
+
+        Propagation means to create a specialized version of the called
+        function, with the propagated argument already filled in. As a simple
+        example, in the following program:
+
+        \startlambda
+        f = λa.λb.a + b
+        inc = λa.f a 1
+        \stoplambda
+
+        We could {\em propagate} the constant argument 1, with the following
+        result:
+
+        \startlambda
+        f' = λa.a + 1
+        inc = λa.f' a
+        \stoplambda
+
+        Special care must be taken when the to-be-propagated expression has any
+        free variables. If this is the case, the original argument should not be
+        removed completely, but replaced by all the free variables of the
+        expression. In this way, the original expression can still be evaluated
+        inside the new function. Also, this brings us closer to our goal: All
+        these free variables will be simple variable references.
+
+        To prevent us from propagating the same argument over and over, a simple
+        local variable reference is not propagated (since is has exactly one
+        free variable, itself, we would only replace that argument with itself).
+
+        This shows that any free local variables that are not runtime representable
+        cannot be brought into normal form by this transform. We rely on an
+        inlining transformation to replace such a variable with an expression we
+        can propagate again.
+
+        \starttrans
+        x = E
+        ~
+        x Y0 ... Yi ... Yn                               \lam{Yi} is not of a runtime representable type
+        ---------------------------------------------    \lam{Yi} is not a local variable reference
+        x' y0 ... yi-1 f0 ...  fm Yi+1 ... Yn            \lam{f0 ... fm} are all free local vars of \lam{Yi}
+        ~
+        x' = λy0 ... λyi-1. λf0 ... λfm. λyi+1 ... λyn .       
+              E y0 ... yi-1 Yi yi+1 ... yn   
+        \stoptrans
+
+        \todo{Describe what the formal specification means}
+        \todo{Note that we don't change the sepcialised function body, only
+        wrap it}
+        \todo{This does not take care of updating the types of y0 ...
+        yn. The code uses the types of Y0 ... Yn for this, regardless of
+        whether the type arguments were properly propagated...}
+
+        \todo{Example}
+
+
+
 
   \section[sec:normalization:properties]{Provable properties}
     When looking at the system of transformations outlined above, there are a
diff --git a/Outline b/Outline
index 533ca69f7c15360dd22dbe288cb61423ce4e763b..35ccc7da1aa8c9ba0a918a295ff990b10aba6c6c 100644 (file)
--- a/Outline
+++ b/Outline
@@ -58,3 +58,4 @@ TODO: Variable vs binder
 TODO: simplification -> Normalisation?
 TODO: Use saturated (application) instead of complete (application)?
 TODO: core => Core
+TODO: \defref{beta-reduction} -> \defref{β-reduction}