EVALUATION
----------

So far we have assumed "normal order beta reduction". That is, in a function 
application (<function> <argument>) we have replaced all occurences or the
bound variable in <function> with the "unevaluated" <argument>. 

New Syntax
----------

 (<name> <argument>) == (<function> <argument>)

 Where == indicates the replacement of <name> by its associated <function>

 (<function> <argument>) => <expression>

 Where => means that in the function application, the bound variable in 
 <function> is replaced with the "unevaluated" <argument>.
 This is "normal order beta reduction". This is the same as "call-by-name".

 (<function> <argument>) -> <expression>

 Where -> means that in the function application, the bound variable in 
 <function> is replaced with the "evaluated" <argument>.
 This is "applicative order beta reduction". This is the same as 
 "call-by-value".


Normal Order Beta Reduction
---------------------------
Normal order beta reduction requires the evaluation of the leftmost redex in 
an expression. In a function application, evaluate the <function>, then 
substitute in unevaluated  <argument>. That is, the evaluation of the 
argument is delayed. Consider the (artificial/contrived) function below:

  silly = Ln.(((IF (iszero n)) n) (pred n))

  (silly ((add one) two))
    == (Ln.(((IF (iszero n)) n) (pred n)) ((add one) two))
    => (((IF (iszero ((add one) two))) 
          ((add one) two)) (pred ((add one) two)))

Ultimately, the expression ((add one) two) would be evaluated twice (not 
three times!). First, we would evaluate the leftmost redex (iszero ((add one) 
two)). This would deliver a result of Lx.Ly.y (second/false), and we would 
then evaluate the expression (pred ((add one) two)). Clearly, this is 
inefficient.


Applicative Order Beta Reduction
--------------------------------
Applicative order beta reduction requires the evaluation of both the 
function and the argument expression. This results in each argument being 
evaluated once only.

  (silly ((add one) two))
    == (Ln.(((IF (iszero n)) n) (pred n)) ((add one) two))
    -> (Ln.(((IF (iszero n)) n) (pred n)) three)
    -> (((IF (iszero three)) three) (pred three))