Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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)
share|cite|improve this question
up vote 1 down vote accepted

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

share|cite|improve this answer
I see. So (λu.(λx.u)u) wouldn't be a redex then? – John Roberts Apr 17 '13 at 22:49
@JohnRoberts No, this term isn't a redex. But it contains redex $(\lambda x.u)u$ as its subterm. – Petr Pudlák Apr 18 '13 at 6:00

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.