next up previous contents index
Next: Extending the Typed Up: The Typed Lambda Previous: A Formal System

Computation System

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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995