[Math] Lambda expression Evaluation

lambda-calculus

( (λf.λx.f(f(x)))(λy.y ^2 ) ) (5)

I tried finding out the order of evaluation for this lambda expression. How is this lambda expression evaluated?

Best Answer

λ-calculus doesn't define an "order of evaluation". Investigating the behavior of different orders of evaluation is one of the issues that the λ-calculus sheds light on.

For example, one can use the "applicative order" strategy used by most conventional programming languages, which is that to evaluate $(\lambda x.A) B$ one first evaluates $B$ to its normal form, and then inserts this normal form into $A$ in place of $x$. But if $B$ has no normal form, this procedure might not terminate, even if $\lambda x.A$ never looks at its argument because $x$ does not appear in $A$. One can use instead the "normal order" strategy, where one substitutes $B$ into $A$ immediately, without evaluating it. A theorem of Church and Rosser says that this is guaranteed to reduce the entire expression to a normal form, if it has one.

For your example, $( (λf.λx.f(f(x)))(λy.y ^2 ) ) (5)$, one can proceed by applicative order:

$$\begin{array}{c} ( (λf.λx.f(f(x)))(λy.y ^2 ) ) (5) \\ (λx.(λy.y ^2 )((λy.y ^2 )(x))) (5) \\ (λy.y ^2 )((λy.y ^2 ) 5) \\ (λy.y ^2 )(5 ^2 ) \\ (5 ^2 ) ^2 \\ \end{array} $$

Normal order begins the same, but proceeds differently once it reaches the $(λy.y ^2 )((λy.y ^2 ) 5)$ step: $$\begin{array}{c} ( (λf.λx.f(f(x)))(λy.y ^2 ) ) (5) \\ (λx.(λy.y ^2 )((λy.y ^2 )(x))) (5) \\ (λy.y ^2 )((λy.y ^2 ) 5) \\ ((λy.y ^2 ) 5) ^2 \\ (5 ^2 ) ^2 \\ \end{array} $$

The end result is the same, as the Church-Rosser theorem says it must be.

Related Question