X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=cdd57bb9c52da6a0d885ae2cadf02d114f76f548;hp=3a7196d44c26ab92338c2e71a29e56097cc5223a;hb=0cd3f69b1d8fb7e18a7e0b2bccd86a96d7fd009b;hpb=9314a7202be9b207a4f8cfe4e1524a85d4bbd2dd diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 3a7196d..cdd57bb 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. @@ -811,6 +812,11 @@ sure that most lambda abstractions will eventually be reducable by β-reduction. + Note that β-reduction also works on type lambda abstractions and type + applications as well. This means the substitution below also works on + type variables, in the case that the binder is a type variable and teh + expression applied to is a type. + \starttrans (λx.E) M ----------------- @@ -828,6 +834,17 @@ \transexample{beta}{β-reduction}{from}{to} + \startbuffer[from] + (λt.λa::t. a) @Int + \stopbuffer + + \startbuffer[to] + (λa::Int. a) + \stopbuffer + + \transexample{beta-type}{β-reduction for type abstractions}{from}{to} + + \subsubsection{Empty let removal} This transformation is simple: It removes recursive lets that have no bindings (which usually occurs when unused let binding removal removes the last @@ -1383,7 +1400,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 +1448,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 +1592,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 +1671,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 +1714,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