1
$\begingroup$

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)
$\endgroup$
1

1 Answer 1

Reset to default
2
$\begingroup$

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})})} $$

$\endgroup$
2
  • $\begingroup$ I see. So (λu.(λx.u)u) wouldn't be a redex then? $\endgroup$
    – John Roberts
    Apr 17, 2013 at 22:49
  • 1
    $\begingroup$ @JohnRoberts No, this term isn't a redex. But it contains redex $(\lambda x.u)u$ as its subterm. $\endgroup$
    – Petr
    Apr 18, 2013 at 6:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .