to this form as the \emph{normal form} of the program. The formal
definition of this normal form is quite simple:
- \placedefinition{}{\startboxed A program is in \emph{normal form} if none of the
+ \placedefinition[force]{}{\startboxed A program is in \emph{normal form} if none of the
transformations from this chapter apply.\stopboxed}
Of course, this is an \quote{easy} definition of the normal form, since our
other expression.
\stopitemize
- \todo{Intermezzo: functions vs plain values}
-
- A very simple example of a program in normal form is given in
- \in{example}[ex:MulSum]. As you can see, all arguments to the function (which
- will become input ports in the generated \VHDL) are at the outer level.
- This means that the body of the inner lambda abstraction is never a
- function, but always a plain value.
-
- As the body of the inner lambda abstraction, we see a single (recursive)
- let expression, that binds two variables (\lam{mul} and \lam{sum}). These
- variables will be signals in the generated \VHDL, bound to the output port
- of the \lam{*} and \lam{+} components.
-
- The final line (the \quote{return value} of the function) selects the
- \lam{sum} signal to be the output port of the function. This \quote{return
- value} can always only be a variable reference, never a more complex
- expression.
-
- \todo{Add generated VHDL}
-
\startbuffer[MulSum]
alu :: Bit -> Word -> Word -> Word
alu = λa.λb.λc.
ncline(add)(sum);
\stopuseMPgraphic
- \placeexample[here][ex:MulSum]{Simple architecture consisting of a
+ \placeexample[][ex:MulSum]{Simple architecture consisting of a
multiplier and a subtractor.}
\startcombination[2*1]
{\typebufferlam{MulSum}}{Core description in normal form.}
{\boxedgraphic{MulSum}}{The architecture described by the normal form.}
\stopcombination
+ \todo{Intermezzo: functions vs plain values}
+
+ A very simple example of a program in normal form is given in
+ \in{example}[ex:MulSum]. As you can see, all arguments to the function (which
+ will become input ports in the generated \VHDL) are at the outer level.
+ This means that the body of the inner lambda abstraction is never a
+ function, but always a plain value.
+
+ As the body of the inner lambda abstraction, we see a single (recursive)
+ let expression, that binds two variables (\lam{mul} and \lam{sum}). These
+ variables will be signals in the generated \VHDL, bound to the output port
+ of the \lam{*} and \lam{+} components.
+
+ The final line (the \quote{return value} of the function) selects the
+ \lam{sum} signal to be the output port of the function. This \quote{return
+ value} can always only be a variable reference, never a more complex
+ expression.
+
+ \todo{Add generated VHDL}
+
\in{Example}[ex:MulSum] showed a function that just applied two
other functions (multiplication and addition), resulting in a simple
architecture with two components and some connections. There is of
ncline(mux)(res) "posA(out)";
\stopuseMPgraphic
- \placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
+ \placeexample[][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
\startcombination[2*1]
{\typebufferlam{AddSubAlu}}{Core description in normal form.}
{\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.}
\stopuseMPgraphic
\todo{Don't split registers in this image?}
- \placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a
+ \placeexample[][ex:NormalComplete]{Simple architecture consisting of an adder and a
subtractor.}
\startcombination[2*1]
{\typebufferlam{NormalComplete}}{Core description in normal form.}
\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
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
\stoptrans
\starttrans
- x = λv0 ... λvn.E
- ~ \lam{E} is representable
+ x = λv0 ... λvn.E \lam{E} is representable
+ ~ \lam{E} is not a lambda abstraction
E \lam{E} is not a let expression
--------------------------- \lam{E} is not a local variable reference
letrec x = E in x
\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
projects / matthijs / master-project / report.git / blobdiff