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
projects / matthijs / master-project / report.git / blobdiff