From 58a5aa7ca5edc07ba1070f4f4ed384b42e36e8f3 Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Mon, 7 Dec 2009 15:19:48 +0100 Subject: [PATCH] =?utf8?q?Use=20=CE=B7/=CE=B2-expansion=20instead=20of=20?= =?utf8?q?=CE=B7/=CE=B2-abstraction.?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- Chapters/Normalization.tex | 26 +++++++++++++------------- Outline | 1 - 2 files changed, 13 insertions(+), 14 deletions(-) diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 2768ba2..fd62fea 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 @@ -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 diff --git a/Outline b/Outline index 56fc5f0..3ab4e6e 100644 --- a/Outline +++ b/Outline @@ -60,5 +60,4 @@ TODO: Future work: Use Cλash TODO: Abstract TODO: Preface TODO: Footnote font has not lambda -TODO: eta-abstraction -> expansion TODO: Top level function -> top level binder -- 2.30.2