1. Applicative Order¶

How many \(\beta\)-redexes are in \((\lambda x.m \; (\lambda x.(x \; x) \; \lambda x.(x \; x)))\)? You should be able to find two. Depending on which one you choose to reduce first, you may find that you end up with \(m\) as your "answer" or that you end up with the same expression that you started with, that is, the \(\beta\)-reduction equivalent of an infinite loop.

We have seen that evaluation of expressions in the \(\lambda\) calculus is essentially \(\beta\)-reduction, which can be defined simply in terms of substitution: \((\lambda p.b \; a) \equiv subst(a,p,b)\)

But there is an additional consideration involved: \(a\) and \(b\) in the preceding \(\beta\)-redex can each contain \(\beta\)-redexes themselves. We then need to recursively reduce them, which raises the following questions:

1. Which redex should we reduce first, the top-level redex, or a nested one?
2. Does it matter which one we do first? What are the consequences of these two strategies?
3. Do different reduction strategies lead to different results?

A key to partially answering the second and third questions above is the Church-Rosser Theorem, which we will merely state and not prove. According to the Church-Rosser theorem, if two different reduction strategies both lead to an answer, then they will lead to the same answer.

So the answers to the second and third questions are no with the following caveat: any reduction strategy that leads to an answer will give the same answer. The key here is whether or not the strategy leads to an answer, and the Church-Rosser theorem neither guarantees termination nor does it guarantee that an answer will be found if it exists. In instances where the strategy leads to an answer that cannot be further reduced, we say that the expression is in beta-normal form (or \(\beta\)-normal form).

The strategy that JavaScript uses in the substitution model of computation is called applicative order reduction. With this strategy, to evaluate an expression of the form f(arg1,arg2,arg3,...), we:

1. Evaluate each of the sub-expressions from left to right, including f if it requires evaluation. (How could it require evaluation?)
2. Apply the leftmost result, which should be a function, to the rest of the evaluated sub-expressions.

The applicative order strategy is characterized by proceeding left-to-right, evaluating the innermost sub-expressions first. That is, we only perform an application when each of the sub-expressions has been reduced and there are no redexes remaining except the topmost application. Consider:

\((\lambda x.((x \; y) \; (y \; x)) \; (\lambda w.(w \; w) \; z))\)

Applicative order evaluation will first reduce \((\lambda w.(w \; w) \; z)\), getting \((z \; z)\). This result will then be substituted in for \(x\) in \(((x \; y) \; (y \; x))\), yielding \((((z \; z) \; y) \; (y \; (z \; z)))\) as the final answer.

Although applicative order reduction finds its answer to the preceding problem in two reductions, when it is used for the first example we considered in this section, that is,

\((\lambda x.m \; (\lambda x.(x \; x) \; \lambda x.(x \; x)))\)

we end up in the infinite loop we referred to earlier.

2. Normal Order¶

Normal order reduction reduces the leftmost \(\beta\)-redex first before reducing the sub-expressions inside of it and those that follow it. While applicative order proceeds by evaluating the sub-expressions and then applying the function, normal order evaluation proceeds by applying the function first and then evaluating the sub-expressions. In other words, normal order reduction always seeks the leftmost outermost reduction whereas applicative order always seeks the leftmost innermost reduction.

Because normal order reduction delays its evaluation of the arguments to a function, it correctly gets \(m\) when applied to the example \((\lambda\)x.m (\(\lambda x.(x \; x) \; \lambda x.(x \; x)))\) on which applicative order looped infinitely.

Now, when applied to \((\lambda x.((x \; y) \; (y \; x)) \; (\lambda w.(w \; w) \; z))\), normal order will substitute \((\lambda w.(w \; w) \; z)\) for both occurrences of \(x\) in \(((x \; y) \; (y \; x))\). It will then have to evaluate \((\lambda w.(w \; w) \; z)\) twice before getting the final answer \((((z \; z) \; y) \; (y \; (z \; z)))\).

If you are still not certain of the exact difference between applicative and normal order, use the following visualization to watch them go through their respective steps on a variety of randomized \(\lambda\) expressions. Once you feel confident that you can always predict what the next step of the visualization will be, you are ready to tackle the practice problems that follow.

3. Beta-Reduction Order (1)¶

This problem focuses on the first step (i.e., \(\beta\)-reduction) in the evaluation of a \(\lambda\) expression with the two evaluation strategies that we discussed. To get credit for this randomized exercise, you must solve it correctly three times in a row.

4. Beta-Reduction Order (2)¶

In this problem, you have to study the complete evaluation of a \(\lambda\) expression with the two evaluation strategies that we discussed. To get credit for this randomized exercise, you must solve it correctly three times in a row.

5. Applicative Order Proficiency Exercise¶

In this problem, you have to perform a full evaluation of a randomly selected \(\lambda\) expression, that is, perform as many \(\beta\)-reductions as it takes until a \(\beta\)-normal form is reached. For this problem, you must use the applicative-order reduction strategy. To get credit for this problem, you only need to solve one problem instance correctly. However, each problem instance contains several steps that you must perform correctly (in this case, each step is a \(\beta\)-reduction). Read and follow the directions carefully. Note that the correct answer (called the model answer) is available. However, if you look it up, you will not get credit for the current problem instance. To get another chance for credit, start a new problem instance by clicking the Reset button.

6. Normal Order Proficiency Exercise¶

In this problem, you have to perform a full evaluation of a randomly selected \(\lambda\) expression, that is, perform as many \(\beta\)-reductions as it takes until a \(\beta\)-normal form is reached. For this problem, you must use the normal-order reduction strategy. To get credit for this problem, you only need to solve one problem instance correctly. However, each problem instance contains several steps that you must perform correctly (in this case, each step is a \(\beta\)-reduction). Read and follow the directions carefully. Note that the correct answer (called the model answer) is available. However, if you look it up, you will not get credit for the current problem instance. To get another chance for credit, start a new problem instance by clicking the Reset button.