\stopdesc
To understand this notation better, the step by step application of
- the η-abstraction transformation to a simple \small{ALU} will be
- shown. Consider η-abstraction, which is a common transformation from
+ the η-expansion transformation to a simple \small{ALU} will be
+ shown. Consider η-expansion, which is a common transformation from
labmda calculus, described using above notation as follows:
\starttrans
λx.E x \lam{E} is not a lambda abstraction.
\stoptrans
- η-abstraction is a well known transformation from lambda calculus. What
+ η-expansion is a well known transformation from lambda calculus. What
this transformation does, is take any expression that has a function type
and turn it into a lambda expression (giving an explicit name to the
argument). There are some extra conditions that ensure that this
transformation does not apply infinitely (which are not necessarily part
- of the conventional definition of η-abstraction).
+ of the conventional definition of η-expansion).
Consider the following function, in Core notation, which is a fairly obvious way to specify a
simple \small{ALU} (Note that it is not yet in normal form, but
\stoplambda
The other alternative is left as an exercise to the reader. The final
- function, after applying η-abstraction until it does no longer apply is:
+ function, after applying η-expansion until it does no longer apply is:
\startlambda
alu :: Bit -> Word -> Word -> Word
\in{section}[sec:normalization:transformation].
\subsection{General cleanup}
- These transformations are general cleanup transformations, that aim to
- make expressions simpler. These transformations usually clean up the
- mess left behind by other transformations or clean up expressions to
- expose new transformation opportunities for other transformations.
-
- Most of these transformations are standard optimizations in other
- compilers as well. However, in our compiler, most of these are not just
- optimizations, but they are required to get our program into intended
- normal form.
-
- \placeintermezzo{}{
- \defref{substitution notation}
- \startframedtext[width=8cm,background=box,frame=no]
- \startalignment[center]
- {\tfa Substitution notation}
- \stopalignment
- \blank[medium]
+ \placeintermezzo{}{
+ \defref{substitution notation}
+ \startframedtext[width=8cm,background=box,frame=no]
+ \startalignment[center]
+ {\tfa Substitution notation}
+ \stopalignment
+ \blank[medium]
+
+ In some of the transformations in this chapter, we need to perform
+ substitution on an expression. Substitution means replacing every
+ occurence of some expression (usually a variable reference) with
+ another expression.
+
+ There have been a lot of different notations used in literature for
+ specifying substitution. The notation that will be used in this report
+ is the following:
- In some of the transformations in this chapter, we need to perform
- substitution on an expression. Substitution means replacing every
- occurence of some expression (usually a variable reference) with
- another expression.
+ \startlambda
+ E[A=>B]
+ \stoplambda
- There have been a lot of different notations used in literature for
- specifying substitution. The notation that will be used in this report
- is the following:
+ This means expression \lam{E} with all occurences of \lam{A} replaced
+ with \lam{B}.
+ \stopframedtext
+ }
- \startlambda
- E[A=>B]
- \stoplambda
+ These transformations are general cleanup transformations, that aim to
+ make expressions simpler. These transformations usually clean up the
+ mess left behind by other transformations or clean up expressions to
+ expose new transformation opportunities for other transformations.
- This means expression \lam{E} with all occurences of \lam{A} replaced
- with \lam{B}.
- \stopframedtext
- }
+ Most of these transformations are standard optimizations in other
+ compilers as well. However, in our compiler, most of these are not just
+ optimizations, but they are required to get our program into intended
+ normal form.
\subsubsection[sec:normalization:beta]{β-reduction}
β-reduction is a well known transformation from lambda calculus, where it is
of the other value definitions in let bindings and making the final
return value a simple variable reference.
- \subsubsection[sec:normalization:eta]{η-abstraction}
+ \subsubsection[sec:normalization:eta]{η-expansion}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
β-reduction and non-representable binding inlining, all function-typed
False -> λy.id y) x
\stopbuffer
- \transexample{eta}{η-abstraction}{from}{to}
+ \transexample{eta}{η-expansion}{from}{to}
\subsubsection[sec:normalization:appprop]{Application propagation}
This transformation is meant to propagate application expressions downwards
Note that the return value is not simplified if its not
representable. Otherwise, this would cause a direct loop with
the inlining of unrepresentable bindings. If the return value is
- not representable because it has a function type, η-abstraction
+ not representable because it has a function type, η-expansion
should make sure that this transformation will eventually apply.
If the value is not representable for other reasons, the
function result itself is not representable, meaning this
\stopframedtext
}
+ \subsubsection{Scrutinee binder removal}
+ This transformation removes (or rather, makes wild) the binder to
+ which the scrutinee is bound after evaluation. This is done by
+ replacing the bndr with the scrutinee in all alternatives. To prevent
+ duplication of work, this transformation is only applied when the
+ scrutinee is already a simple variable reference (but the previous
+ transformation ensures this will eventually be the case). The
+ scrutinee binder itself is replaced by a wild binder (which is no
+ longer displayed).
+
+ Note that one could argue that this transformation can change the
+ meaning of the Core expression. In the regular Core semantics, a case
+ expression forces the evaluation of its scrutinee and can be used to
+ implement strict evaluation. However, in the generated \VHDL,
+ evaluation is always strict. So the semantics we assign to the Core
+ expression (which differ only at this particular point), this
+ transformation is completely valid.
+
+ \starttrans
+ case x of bndr
+ alts
+ ----------------- \lam{x} is a local variable reference
+ case x of
+ alts[bndr=>x]
+ \stoptrans
+
+ \startbuffer[from]
+ case x of y
+ True -> y
+ False -> not y
+ \stopbuffer
+
+ \startbuffer[to]
+ case x of
+ True -> x
+ False -> not x
+ \stopbuffer
+
+ \transexample{scrutbndrremove}{Scrutinee binder removal}{from}{to}
+
\subsubsection{Case normalization}
This transformation ensures that all case expressions get a form
that is allowed by the intended normal form. This means they
lambda abstraction.
To reduce all higher-order values to one of the above items, a number
- of transformations we have already seen are used. The η-abstraction
+ of transformations we have already seen are used. The η-expansion
transformation from \in{section}[sec:normalization:eta] ensures all
function arguments are introduced by lambda abstraction on the highest
level of a function. These lambda arguments are allowed because of
- \in{item}[item:toplambda] above. After η-abstraction, our example
+ \in{item}[item:toplambda] above. After η-expansion, our example
becomes a bit bigger:
\startlambda
) q
\stoplambda
- η-abstraction also introduces extra applications (the application of
+ η-expansion also introduces extra applications (the application of
the let expression to \lam{q} in the above example). These
applications can then propagated down by the application propagation
transformation (\in{section}[sec:normalization:appprop]). In our
representable type). Completely applied top level functions (like the
first alternative) are now no longer invalid (they fall under
\in{item}[item:completeapp] above). (Completely) applied lambda
- abstractions can be removed by β-abstraction. For our example,
- applying β-abstraction results in the following:
+ abstractions can be removed by β-expansion. For our example,
+ applying β-expansion results in the following:
\startlambda
λy.λq.let double = λx. x + x in