X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=55e00577e393dc0c3933ecb708ad4c394d95ca5c;hp=ca84ed171760e6af2a40cf3f418025a4d13c15bc;hb=222070c846ebc49b0b569386fe906edb617bda0b;hpb=a117295a33890774410292246ae8d21bd2505cf8 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index ca84ed1..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. @@ -957,15 +958,17 @@ arguments used here are described in \in{Section}[section:prototype:polymorphism]. - Without this transformation, there would be a (+) entity in the - architecture which would just add its inputs. This generates a lot of - overhead in the VHDL, which is particularly annoying when browsing the - generated RTL schematic (especially since + is not allowed in VHDL - architecture names\footnote{Technically, it is allowed to use - non-alphanumerics when using extended identifiers, but it seems that - none of the tooling likes extended identifiers in filenames, so it - effectively doesn't work}, so the entity would be called - \quote{w7aA7f} or something similarly unreadable and autogenerated). + Without this transformation, there would be a \lam{(+)} entity + in the \VHDL which would just add its inputs. This generates a + lot of overhead in the \VHDL, which is particularly annoying + when browsing the generated RTL schematic (especially since most + non-alphanumerics, like all characters in \lam{(+)}, are not + allowed in \VHDL architecture names\footnote{Technically, it is + allowed to use non-alphanumerics when using extended + identifiers, but it seems that none of the tooling likes + extended identifiers in filenames, so it effectively doesn't + work.}, so the entity would be called \quote{w7aA7f} or + something similarly unreadable and autogenerated). \subsection{Program structure} These transformations are aimed at normalizing the overall structure @@ -1381,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 @@ -1429,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} @@ -1630,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 @@ -1671,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 @@ -1712,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