From: Matthijs Kooijman Date: Wed, 2 Dec 2009 14:50:42 +0000 (+0100) Subject: Add an intermezzo about substitution. X-Git-Tag: final-thesis~118 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=68e92ccd2b456b9ce81b0617417bc8abdaff6fa3;p=matthijs%2Fmaster-project%2Freport.git Add an intermezzo about substitution. This is the first attempt at an intermezzo, which is not quite ideal yet, but it works for now. --- diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 78b7a1d..03f3792 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -641,8 +641,6 @@ In the following sections, we will be using a number of functions and notations, which we will define here. - \todo{Define substitution (notation)} - \subsubsection{Concepts} A \emph{global variable} is any variable (binder) that is bound at the top level of a program, or an external module. A \emph{local variable} is any @@ -799,8 +797,33 @@ optimizations, but they are required to get our program into intended normal form. + \placeintermezzo{}{ + \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: + + \startlambda + E[A=>B] + \stoplambda + + This means expression \lam{E} with all occurences of \lam{A} replaced + with \lam{B}. + \stopframedtext + } + + \defref{beta-reduction} \subsubsection[sec:normalization:beta]{β-reduction} - \defref{beta-reduction} β-reduction is a well known transformation from lambda calculus, where it is the main reduction step. It reduces applications of lambda abstractions, removing both the lambda abstraction and the application. diff --git a/Utils/Lambda.tex b/Utils/Lambda.tex index f08d75e..319b424 100644 --- a/Utils/Lambda.tex +++ b/Utils/Lambda.tex @@ -124,4 +124,18 @@ draw b; \definefloat[example][examples] \setupcaption[example][location=top] % Put captions on top +% Margin magic taken from +% http://www.pragma-ade.com/general/manuals/details.pdf By setting negative +% margin distances, we put our float inside the outer margin. I think we set +% both left and right margin distance, because we don't know what will be the +% outer margin (and it will probably only use the distance of the margin it's +% actually aligning against). +% We also set an offset, to prevent protruding text (overfull hboxes) from +% jamming into the intermezzo. Also, some extra space is easier on the eye +% (However, the intermezzo is moved to the right by this offset, instead of +% moving the text to left. We can't increase the offset by much...) +\setupfloat[intermezzo][offset=.3cm,leftmargindistance=-\leftmarginwidth, rightmargindistance=-\rightmarginwidth, default={outer}] +\setupcaption[intermezzo][location=top,number=no] % Put captions on top + +\setupheads[aligntitle=float] % vim: set sw=2 sts=2 expandtab: