From 222070c846ebc49b0b569386fe906edb617bda0b Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Mon, 30 Nov 2009 23:22:14 +0100 Subject: [PATCH] Restructure some of the normalization chapter. --- Chapters/Normalization.tex | 188 +++++++++++++++++++++++-------------- Outline | 1 + 2 files changed, 118 insertions(+), 71 deletions(-) diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 3a7196d..55e0057 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -801,6 +801,7 @@ 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. @@ -1383,7 +1384,7 @@ \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 @@ -1431,64 +1432,7 @@ 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} @@ -1632,20 +1576,58 @@ \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 @@ -1673,7 +1655,9 @@ 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 @@ -1714,6 +1698,68 @@ \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 533ca69..35ccc7d 100644 --- 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} -- 2.30.2