There may be a choice of two or more applications in an expression.
For example, the following expression can be reduced by two different paths:
( λx . λy . ( add y ( ( λz . ( mul x z ) ) 3 ) ) ) 7 5
⇒β ( λy . ( add y ( ( λz . ( mul 7 z ) ) 3 ) ) ) 5
⇒β ( add 5 ( ( λz . ( mul 7 z ) ) 3 ) )
⇒β ( add 5 ( mul 7 3 ) ) = ( add 5 21 ) = 26
( λx . λy . ( add y ( ( λz . ( mul x z ) ) 3 ) ) ) 7 5
⇒β ( λx . λy . ( add y ( mul x 3 ) ) ) 7 5
⇒β ( λy . ( add y ( mul 7 3 ) ) ) 5
= ( λy . ( add y 21 ) ) 5
⇒β ( add 5 21 ) = 26
The strategy for determining which application to carry out next is called an evaluation rule.
There are two rules commonly used:
- Strict evaluation or call by value:
It requires the evaluation of an actual parameter before it is passed to, or substituted in, a function.
It corresponds to passing parameters by value in a language such as Pascal.
- Normal-order evaluation or call by name:
It specifies that the left-most, outer-most application of an expression be carried out at each step.
An actual parameter is not evaluated before being passed to a function.
It corresponds to passing parameters by name, as in Algol-60.
For example, the expression terminates by using normal-order evaluation:
( λx . 7 ) ( ( λx . x x ) ( λy . y y ) ) ⇒β 7
The expression does not terminates by using strict evaluation:
( λx . 7 ) ( ( λx . x x ) ( λy . y y ) )
⇒β ( λx . 7 ) ( ( λy . y y ) ( λy . y y ) )
⇒β …