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.
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
-----------------
\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
\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