9c9
< \setlength{\headheight}{0cm}
---
> \setlength{\headheight}{1cm}
81c81
< Each language has a syntax for specifying functions.  In lambda
---
> Each language has a syntax to specifying functions.  In lambda
85,89c85,87
< argument to the function.  The $\lambda$-term itself is a value,
< sometimes called a {\em nameless function,\/} and we are just using
< the symbol $f$ to refer to it.  When we apply the function to an
< (actual) argument, like in $(f~4)$, we replace each $x$ in the body of
< the function with $4$, which results in $4*4$, or $(*~4~4)$: this
---
> argument to the function.  When we apply the function to an (actual)
> argument, like in $(f~4)$, we replace each $x$ in the body of the
> function with $4$, which results in $4*4$, or $(*~4~4)$: this
91,93c89,91
< $*$.  The evaluation continues until we reach a {\em ``normal
<   form,''\/} such as $16$, which can't be evaluated any further.
< Sounds simple enough, but there are some complications.
---
> $*$.  The evaluation continues until we reach a {\em ``normal form,''\/} such
> as $16$, which can't be evaluated any further.  Sounds simple enough,
> but there are some complications.
95,96c93,94
< Actually, in Python you can also just write \verb+'f=lambda x:x*x'+,
< but even in languages that do not support lambda
---
> Actually, in Python you can also write \verb+'f=lambda x:x*x'+ to have
> the same effect, but even in languages that do not support lambda
100c98
< int f(int x) 
---
> int f(int x)
207c205
< Observe that by the syntactic conventions, this term should be
---
> Observer that by the syntactic conventions, this term should be
217c215
< Now we can more formally define how to apply a function in the form of a $\lambda$-abstraction to
---
> Now we can more formally define how to apply a function as a $\lambda$-abstraction to
219c217
< $M$, let $M[N/x]$ represents the term obtained by replacing {\em all free
---
> $M$, let $M[N/x]$ represent the term obtained by replacing {\em all free
293,294c291,292
< Yes, this is {\em a term that applies its argument to itself and is itself applied to itself, and
< such a term reduces to itself.\/} Got it?  Don't even try to understand it
---
> Yes, a term that applies its argument to itself is applied to itself, and
> such a term reduces to itself. Got it?  Don't even try to understand it
656c654
< if we used directed acyclic graphs {\em (DAGs)\/} instead of {\em trees\/} to
---
> if used a directed acyclic graph {\em (DAG)\/} instead of {\em tree\/} to
661,662c659,660
< to a function.  Furthermore, the code must carry the environment under which
< it's defined in order to be executed correctly: it's called a {\em closure.\/}
---
> to a function.  Furthermore, the code must carry whatever information it needs
> in order to be executed correctly.
674c672
< of $a$, and it is clearly not how we want if-else to behave.  Thus, from
---
> of $a$, and it this is clearly not how we want if-else to behave.  Thus, from
682c680
< the terms that cannot be evaluated eagerly, inside vacuous 
---
> the terms that cannot be evaluated eagerly, inside dummy
701,702c699,700
< We will need these versions of the combinators in our implementation of
< pure lambda calculus in real programming languages, such as Python and Perl.
---
> We will use these versions of the combinators in our implementation of
> pure lambda calculus in Scheme, Python and Perl.
737d734
< 
904,908c901
< and logic.  That is, if $\rightarrow$ can be read as {\em implies\/} then
< the type of every combinator must be a propositional {\em tautology\/}
< because the rules of typing are isomorphic to the rules of logic (this is
< called the {\em Curry-Howard Isomorphism\/}).
< The following is a sample type derivation using the rules:
---
> and logic.  The following is a sample type derivation using the rules:
916,918d908
<       You can verify that the derived type is a tautology by constructing a truth
<       table.
<       
920a911
> 
927,929c918
<   3+1 is an expression of type int, and 4, the normal form, is also an int.
<   So type checking can be done before, during, or after beta-reduction. If
<   it's done before reduction, it's called {\em static typing.\/}
---
>   3+1 is an integer, and 4, the normal form, is also an integer.
932,937c921,924
< such as $\lambda x.(x~x)$, is not typable (does not have a type).  To
< encode a programming language that allows for recursion and
< repetition, the fixed pointer operator, with property $FIX~M = M~(FIX
< ~M)$, must be imported as an extra constant.  If we are to give $FIX$
< a type, it would have to be $(a\rightarrow a)\rightarrow a$.  This is
< a {\em not a tautology,\/} so no pure lambda term can have this type.
---
> such as $\lambda x.(x~x)$, is not typable (does not have a type).  To encode a programming
> language that allows for recursion and repetition, the fixed pointer
> operator, with property $FIX~M = M~(FIX ~M)$, must be imported as an extra
> constant.
939d925
< \end{document}
945a932
> \end{document}
958,984d944
< 
< \section{Static Single Assignment Form}
< 
< The lambda calculus is {\em stateless,\/} which means that the same
< term will always reduce to the same normal form.  But what if we allowed
< {\em destructive assignment\/} in our language: the infamous 
< $x=x+1$?  Certainly computing this expression twice will have a
< different effect than computing it once.  Such an opertion is not
< stateless.  However, this does not necessarily mean that every program
< that contains such assignments are not {\em admissible\/} in lambda
< calculus.  In fact, many modern compilers will first translate a program
< into an intermediate language called {\em Static Single
<   Assignment Form\/} (SSA).  A new variable is introduced for each
< destructive assignment, so $x=x+1$ is translated into something
< like $x_2=x+1$. Loops containing such statements are translated
< into {\em tail\/} recursive functions where $x$ is an argument.  The
< popular {\em LLVM\/} intermediate language is based on SSA. 
< The first C program on page 2, which contains a destructive assignment
< $y=y+x$, is equivalent to the following pure lambda term:
< $$
< f= \lambda x. (\lambda y_2.y_2+x) ((\lambda y.(\lambda x.y+x)~2)~1)
< $$
< The destructive assignment to $y$ has been replaced by a {\em single\/}
< binding to the variable $y_2$.  We see that $(f~4)$ reduces to
< $(\lambda y_2.y_2+4) ((\lambda y.(\lambda x.y+x)~2)~1) ~\Rightarrow~$
< $(\lambda y_2.y_2+4) ((\lambda y.y+2)~1) ~\Rightarrow~$
< $(\lambda y_2.y_2+4) (1+2) ~\Longrightarrow~ 7$.