0

I'm trying to beta-reduce the following: $$\lambda xy.y((\lambda xyz.xyz)(\lambda u.u)(\lambda u.uu))$$ Anyway I think that I didn't understand terms' scope.

Considering the application in the shape of $ (\lambda x.y)M $ and evaluating by leftmost outermost, at the first step, I have that my $ (\lambda x.y)M $ is:

  1. $ (\lambda xyz.xyz)(\lambda u.u), $ or
  2. $ (\lambda xyz.xyz)(\lambda u.u)(\lambda u.uu)$?

How should I choose M?

Thank you.

MoreOver
  • 101
  • 2
  • Are there no parentheses around the $\lambda xy.y$ part? Otherwise it's rather hard to be sure what is meant here. – MJD Oct 10 '14 at 17:20
  • No, I suppose they are hidden: before the first lambda and after the last parenthesis in the equation. – MoreOver Oct 10 '14 at 17:40

1 Answers1

0

Since the expression overall has the form $\def\L{\lambda}\L xy.yB$, any $\beta$-reduction will have to be inside the subexpression $B$, which is $(\L xyz.xyz)(\L u.u)(\L u.uu))$. There is a standard convention in $\L$-calculus in which $(a\,b\, c)$ is an abbreviation for $((a\,b)\, c)$, so the expression above should be considered short for $$(\color{darkblue}{((\L xyz.xyz)(\L u.u))}\;(\L u.uu)).$$

The only reducible subexpression is colored in dark blue. It has the form $(\L x.B)M$ where $M=\L u.u$, so you should have no trouble reducing it. (If you do, ask a question in the comments.)

After reducing the blue expression to a result $\color{darkblue}{R}$ you can further reduce $(\color{darkblue}{R} (\L u.uu))$.

MJD
  • 65,394
  • 39
  • 298
  • 580
  • Sorry, I've edited my question, I meant (\lambda x.y)M. Anyway to me it's still not clear why you chose answer 1. and not 2 (from my question). To be more precise, what I don't understand is why that one is "The only reducible expression". Are you saying that I should consider (λxyz.xyz)(λu.u)(λu.uu) like (a)(b)(c) and so it becomes ((a)(b))(c)? Thank you. – MoreOver Oct 10 '14 at 21:55
  • Are you aware that $\lambda xyz.B$ is a shorthand for $\lambda x.(\lambda y.(\lambda z.B))$? Or should I explain that in more detail? – MJD Oct 10 '14 at 21:58
  • Yes, I'm aware of this. My problem was with B, in the sense that I couldn't understand where to stop selecting it. Anyway if all come from (a)(b)(c) -> ((a)(b))(c), I've understand the reason. Thank you. – MoreOver Oct 10 '14 at 22:01
  • If you can expand it entirely, I'd appreciate it, anyway, thank you. – MoreOver Oct 11 '14 at 01:28
  • I'm concerned that by doing so we might be violating your school's academic honesty rules. – MJD Oct 11 '14 at 15:02
  • Can you confirm me if this is the right solution, please? Thank you. λxy.y((λxyz.xyz)(λu.u)(λu.uu)) -> λxy.y((λyz.(λu.u)yz)(λu.uu)) -> λxy.y((λz.(λu.u)(λu.uu)z)) -> λxy.y((λz.(λu.uu)z)) -> λxy.y(λz.zz) – MoreOver Oct 11 '14 at 20:41