Parentheses placement and identifying redexes in a lambda expression

Question

I'm struggling to understand how to identify redexes in a lambda expression. I've been given the following expression and asked to identify all redexes

(.(.))(.)

I understand that -terms are left associative. So I believe I would place my parentheses as follows

(((.((.)))(.)))

I see that (.(.))(.) is a redex as it follows a (.)' pattern and I believe (.) is also a redex. Is there a third that spans the entire expression?

Would the reduction look something like this?

(((.((0.0)))(1.1))2)

(((0.0)(1.1))2)

((1.1)2)

2

Answer 1

Yes, in the $\lambda$-term \begin{align} (\lambda x. (\lambda x_0.x_0) x)(\lambda x_1. x_1) x \end{align} there are exactly two redexes: $(\lambda x. (\lambda x_0.x_0) x)(\lambda x_1. x_1)$ and $(\lambda x_0.x_0) x$.

Your reduction is correct, it starts by reducing the redex $(\lambda x. (\lambda x_0.x_0) x)(\lambda x_1. x_1)$.

Note that another reduction is possible, starting by reducing the redex $(\lambda x_0.x_0) x$: \begin{align} &(\lambda x. (\lambda x_0.x_0) x)(\lambda x_1. x_1) x_2 \\ &(\lambda x. x)(\lambda x_1. x_1) x_2 \\ &(\lambda x_1. x_1) x_2 \\ &x_2 \end{align} Coincidentally, the two reductions are extensionally the same (the same $\lambda$-terms), even though they are obtained intensionally in a different way, by reducing different redexes.