Lazy or Normal Evaluation

Here are the inductively defined rules for lazy evaluation. To evaluate a term :

• if is an abstraction, then is the value itself.
• if is an application, i.e. , then evaluate ; if the result is an abstraction, i.e. , then evaluate .
• if is a variable, then abort.

We write its corresponding natural semantics: