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.