\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
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 / commitdiff