I am self-studying Lambda calculus and have encountered a question where I need to identify all the redexes of the following expression: (λu.(λx.u)u)((λy.y)(λw.(λv.v)w)). Here are all the ones I've come up with, but I'm not sure if they are valid or if I'm missing any. Could somebody help?
1. (λx.(λy.y) (λw.(λv.v) w)) ((λy.y) (λw.(λv.v) w))
2. (λy.y) (λw.(λv.v) w)
3. λw.(λv.v) w
4. (λu.(λx.u) u) ((λy.y) (λv.v))
5. (λx.λv.v) (λv.v)
A redex of a term is its subterm of the form $(\lambda x.M)N$. Some of your expressions aren't redexes of the given expression, but of some different terms (which you probably computed by evaluating the original one).
Redexes of the original expressions are: $$ \underbrace{(\lambda u.\underbrace{(\lambda x.u)u})(\underbrace{(\lambda y.y)(\lambda w.\underbrace{(\lambda v.v)w})})} $$
In your list, the terms which appear are the following: $$ y,\quad A = λy·y,\quad v,\quad B = λv·v,\quad w,\quad C_w = B w,\\ D = λw·C_w,\quad E = A D,\quad F = λx·E,\quad G = F E,\quad u,\quad H_u = λx·u,\\ I_u = H_u u,\quad J = λu·I_u,\quad K = A B,\quad L = J K,\quad M = λx·B,\quad N = M B. $$ Your numbered expressions are, respectively, $G$, $E$, $D$, $L$ and $N$. The terms which are variables are: $$y,\quad x,\quad w,\quad u.$$ The terms which are lambda-abstractions are: $$ A = λy·y,\quad B = λv·v,\quad D = λw·C_w,\quad F = λx·E,\\ H_u = λx·u,\quad J = λu·I_u,\quad M = λx·B. $$ The terms which are applications are $$C_w = B w,\quad E = A D,\quad G = F E,\quad I_u = H_u u,\quad K = A B,\quad L = J K,\quad N = M B. $$
An application whose first subterm is a lambda abstraction is a redex. All of the applications listed are of this form and are, therefore, redexes. Under β-reduction: $$ C_w = (λv·v) w → w,\quad E = (λy·y) D → D,\quad G = (λx·E) E → E,\quad I_u = (λx·u) u → u,\\ K = (λy·y) B → B,\quad L = (λu·I_u) K → I_K,\quad N = (λx·B) B → B. $$ Thus, $$C_w → w,\quad G → E → D,\quad L → I_K → K → B,\quad N → B.$$
The lambda abstractions reduce underneath their respective lambdas to: $$D = λw·C_w → λw·w,\quad F = λx·E → λx·D,\quad J = λu·I_u → λu·u.$$ The others are all already in normal form. Thus, defining $O = λw·w$, we have: $$G → D → O,\quad E → D → O,\quad D → O,\quad L → I_K → K → B,\quad N → B.$$ Finally, under α-equivalence, $A ≡ B ≡ O$.
