1

How do I beta reduce these equations. My attempts are below the questions.

  1. (λy.zy)a

= λy[y:=a].zy

= λa.za

  1. (λz . zz)(λy . yy)

= λz[z:=λy . yy].z z

= (λy . yy)(λy . yy)

= (λy[y:=λy . yy].yy)

= (λy . yy)y

= λy[y:=y]y

  1. (λx.x)(λx.x)

= (λx[x:=λx.x].x)

= λx.x

  1. (λx.xy)(λx.xx)

= (λx[x:=λx.xx].xy)

= (λx.xx)y

= λx[x:=y].xx

= yy

Are my solutions correct?

llamaro25
  • 289
  • This is hard to read. – NoChance Aug 25 '19 at 12:12
  • 1
    Just a note on notation: The way you use the part in square brackets is unusual -- normally, $P[x:Q]$ means "in $P$, replace $x$ by $Q$"; but when reducing a redex, it's not the lambda-abstraction part ($\lambda x.$) in which the substitution happens, but the term bound by the lambda-abstraction ($M$): $(\lambda x.M)N \to_\beta M[x:N]$ -- so e.g. $(\lambda y.zy)a \to_\beta (zy)[y:=a]$, not $\lambda y[y:=a].zy$ -- the substitution of $a$ for $y$ happens on $zy$, not on $\lambda y$, which is eliminated, – Natalie Clarius Aug 25 '19 at 21:23
  • @lemontree oh, I see. I just copied the format in my lecture slides. I will consult my lecturer about it. thanks! – llamaro25 Aug 26 '19 at 09:04

1 Answers1

2
  1. After substituting $[y:=a]$, the leading $\lambda$ should be resolved (omitted), so we get $za$.
  2. Let $s:=\lambda y. yy$. After the first step, when you arrived to $ss$, I can't follow you. When applying the $\beta$-reduction to $ss$, we get back $ss$ again.
  3. and 4. are correct.
Berci
  • 90,745