From 1fc4b09400e7d602d794b3ce0c1a4c032047aa98 Mon Sep 17 00:00:00 2001
From: Matthijs Kooijman <matthijs@stdin.nl>
Date: Mon, 12 Oct 2009 13:15:45 +0200
Subject: [PATCH] =?utf8?q?Split=20"extended=20=CE=B2-reduction"=20into=20t?=
 =?utf8?q?wo=20transformations.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

---
 Chapters/Normalization.tex | 89 +++++++++++++++++++++++++-------------
 1 file changed, 60 insertions(+), 29 deletions(-)

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index fd0e2cb..7c6b469 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -784,21 +784,66 @@ foo = λa.λx.(case a of
 
 \transexample{η-abstraction}{from}{to}
 
-\subsection{Extended β-reduction}
+\subsection{β-reduction}
+β-reduction is a well known transformation from lambda calculus, where it is
+the main reduction step. It reduces applications of labmda abstractions,
+removing both the lambda abstraction and the application.
+
+In our transformation system, this step helps to remove unwanted lambda
+abstractions (basically all but the ones at the top level). Other
+transformations (application propagation, non-representable inlining) make
+sure that most lambda abstractions will eventually be reducable by
+β-reduction.
+
+TODO: Define substitution syntax
+
+\starttrans
+(λx.E) M
+-----------------
+E[M/x]
+\stoptrans
+
+% And an example
+\startbuffer[from]
+(λa. 2 * a) (2 * b)
+\stopbuffer
+
+\startbuffer[to]
+2 * (2 * b)
+\stopbuffer
+
+\transexample{β-reduction}{from}{to}
+
+\subsection{Application propagation}
 This transformation is meant to propagate application expressions downwards
-into expressions as far as possible. In lambda calculus, this reduction
-is known as β-reduction, but it is of course only defined for
-applications of lambda abstractions. We extend this reduction to also
-work for the rest of core (case and let expressions).
+into expressions as far as possible. This allows partial applications inside
+expressions to become fully applied and exposes new transformation
+possibilities for other transformations (like β-reduction).
 
-For let expressions:
 \starttrans
 let binds in E) M
 -----------------
 let binds in E M
 \stoptrans
 
-For case statements:
+% And an example
+\startbuffer[from]
+( let 
+    val = 1
+  in 
+    add val
+) 3
+\stopbuffer
+
+\startbuffer[to]
+let 
+  val = 1
+in 
+  add val 3
+\stopbuffer
+
+\transexample{Application propagation for a let expression}{from}{to}
+
 \starttrans
 (case x of
   p1 -> E1
@@ -811,35 +856,21 @@ case x of
   pn -> En M
 \stoptrans
 
-For lambda expressions:
-\starttrans
-(λx.E) M
------------------
-E[M/x]
-\stoptrans
-
 % And an example
 \startbuffer[from]
-( let a = (case x of 
-            True -> id
-            False -> neg
-          ) 1
-      b = (let y = 3 in add y) 2
-  in
-    (λz.add 1 z)
-) 3
+( case x of 
+    True -> id
+    False -> neg
+) 1
 \stopbuffer
 
 \startbuffer[to]
-let a = case x of 
-           True -> id 1
-           False -> neg 1
-    b = let y = 3 in add y 2
-in
-  add 1 3
+case x of 
+  True -> id 1
+  False -> neg 1
 \stopbuffer
 
-\transexample{Extended β-reduction}{from}{to}
+\transexample{Application propagation for a case expression}{from}{to}
 
 \subsection{Let derecursification}
 This transformation is meant to make lets non-recursive whenever possible.
-- 
2.30.2