Lambda Calculus using $\beta$-reductions

Question

Use $\beta$ reductions to compute the final answer for the following $\lambda$ terms. Use a "fake" reduction step for "+" operator. Identify each redex for $\beta$-reduction steps. Does the order in which you apply these $\beta$-reduction steps make a difference in the final answer?

1. (($\lambda$x.(($\lambda$z.(($\lambda$x.(z x)) 3)) ($\lambda$y.(+ x y)))) 1)

2. (($\lambda$z. (($\lambda$y.z) (($\lambda$x.(x x))($\lambda$x.(x x))))) 5)

My solution for #1 was as follows:

(($\lambda$z.(($\lambda$x.(z x)) 3)) ($\lambda$y.(+ 1 y)))

(($\lambda$x.(($\lambda$y.(+ 1 y))x))3)

(($\lambda$x.(($\lambda$y.(+ 1 y)) x)) 3)

(($\lambda$y.(+ 1 y)) 3)

(+ 1 3)

4

However I couldn't get anything for #2, could someone please show me the process.

Also my interpretation is that the order does affect the answer, but I have no reasoning for it.

• MJD: The Church-Rosser theorem says that if two sequences of reductions each reach a normal form, then it must be the same normal form; this is what justifies references to "the" normal form of a redex.

Answer 1

Your reduction of (1) is correct, except that you have $((λx.((λy.(+ 1 y))x))3)$ in there twice for some reason.

For 2, let's first abbreviate the subexpression $(λx.(x x))(λx.(x x))$ to $\omega$ as is often done. Then (2) is: $$((λz. ((λy.z) \omega)) 5)$$

$\omega$ is notorious because it is the simplest example of a $\lambda$-term with no normal form; it $\beta$-reduces in one step to $\omega,ドル and so an attempt to reduce it to normal form never terminates. However, we can still reduce the entire term as follows. First apply $(\lambda z. \ldots)$ to the argument 5, obtaining: $$((λy.5) \omega)$$

And again apply $(λy.5)$ to $\omega$ obtaining $5ドル$$

This is the normal form for the original expression. Since an attempt to reduce $\omega$ never terminates, the reduction order does make a difference. Notice that in obtaining the normal form, in each case we reduced the leftmost redex without first attempting to reduce its argument. This is called ‘normal-order’ reduction, and is guaranteed to produce the normal form of the expression, if it has one.

[ You didn't ask about this, but I found the redundant parentheses in your expressions extremely confusing, and I suggest that in the future you try to use fewer of them. ]