The meaning of lambda terms is given by computation rules.
The basic rule,
called * beta reduction *,
is that reduces to
; for example,
reduces to .
The strategy for computing applications is involves reducing
**f** until it has the form ,
then computing .
This method of computing with noncanonical forms is called
* head reduction * or * lazy evaluation *, and
it is not the only possible way to compute.
For example, we might reduce **f** to and then continue
to perform reductions in the body **b**.
Such steps might constitute computational optimizations of functions.
Another possibility is to reduce **a** first until it reaches canonical
form before performing the beta reductions.
This corresponds to call--by--value computation
in a programming language.

In Nuprl we use lazy evaluation, although for the simple calculus of typed lambda terms it is immaterial how we reduce. Any reduction sequence will terminate---this is the strong normalization result [Tait 67,Stenlund 72]---and any sequence results in the same value according to the Church--Rosser theorem [Church 51,Stenlund 72]. Of course, the number of steps taken to reach this form may vary considerably depending on the order of reduction.

Thu Sep 14 08:45:18 EDT 1995