X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=a1dec0a854efabd08ff58e32c07b2d3845dd99b4;hp=2768ba2c0a2c89e87e989471bd5d7a3c53ea5e4c;hb=313351372e8c609c2875902d9c9a2b89f7c97032;hpb=05ab912a6a0d53892521265750b313126ab442af diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 2768ba2..a1dec0a 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -473,8 +473,8 @@ \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 @@ -483,12 +483,12 @@ λ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 @@ -632,7 +632,7 @@ \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 @@ -820,41 +820,41 @@ \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 @@ -1099,7 +1099,7 @@ 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 @@ -1123,7 +1123,7 @@ 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 @@ -1284,7 +1284,7 @@ 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 @@ -1776,11 +1776,11 @@ 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 @@ -1791,7 +1791,7 @@ ) 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 @@ -1810,8 +1810,8 @@ 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