\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