1

Let $M \equiv \lambda z.zy$

is $M$ in $\beta$-normal form?

I know that the $\beta\text{-}nf$ class is defined as following:

(1) all atoms are in $\beta\text{-}nf$

(2) $M_1 ,...,M_n ∈ β\text{-}nf ⇒ aM_1 ...M_n ∈ β\text{-}nf\quad$ for all atoms $a$

(3) $M ∈ β\text{-}nf ⇒ λx.M ∈ β\text{-}nf$

So, by construction, I guess $M$ belongs to $β\text{-}nf$ by doing:

i) initialize a term as $y$ and call it $A_1$ (thus, $A_1 \equiv y$). By (1), $A_1 ∈ β\text{-}nf$

ii) by (2), let $n=1$ and $M_1 \equiv A_1$, so $zA_1$ should belong to $β\text{-}nf$. Let's say $A_2 \equiv zA_1$

iii) by (3), $\lambda z.A_2$ should belong to $β\text{-}nf$ since $A_2$ also does. Let's say $A_3 \equiv \lambda z.A_2$

as $A_2 \equiv zA_1$ and $A_1 \equiv y$, $A_2 \equiv zy$, thus $A_3 \equiv \lambda z.zy$

$M$ is obviously the same than $A_3$, so I guess $M$ belongs to $β\text{-}nf$. Is this right or I missed something in the way?

Community
  • 1
Daniel
  • 732
  • 1
    $\beta$-normal form is usually defined as a lambda term for which no $\beta$-reductions apply. This is clearly the case for $M$. The $\beta$-$nf$ class you describe would normally be separately described and there would be a theorem stating that all irreducible lambda terms are in the $\beta$-$nf$ class. – Derek Elkins left SE Aug 29 '17 at 07:03
  • I thought I could apply $y$ at the $\lambda z$ by doing $[y/z] z$ – Daniel Aug 29 '17 at 22:48
  • If $\lambda z.zy$ means $(\lambda z.z)y$ then you would be correct, but it usually means $\lambda z.(zy)$ and this seems to be how you are interpreting it in your question (i.e. $A_2$). – Derek Elkins left SE Aug 29 '17 at 23:08

1 Answers1

0

Indeed.   There is no need to introduce the $A_\star$ symbols though.

  • Tokens $z$ and $y$ are atoms.

  • Via (1), since they are atoms, therefore $z$ and $y$, are in $\beta$-nf.

  • Via (2), since these atoms, $z$ and $y$, are in $\beta$-nf, therefore their product, $zy$, is too.

  • Via (3), since such a thing as $zy$ is in $\beta$-nf, therefore the lambda expression $\lambda z {.} zy$ is too.

  • Since $\bf M$ is that lambda expression, therefore $\bf M$ is in $\beta$-nf.

$\blacksquare$

Graham Kemp
  • 129,094
  • I was thinking that $\lambda z.zy$ wasn't $\beta$-normal because I thought $\lambda z.zy \rhd _{\beta} [y/z]z$, thus $\lambda z.zy \rhd _{\beta} y$. Why is this wrong? I guess that, by convention, $y$ is not applying to $\lambda z.z$ ? – Daniel Aug 29 '17 at 05:19
  • Is there a condition missing from definition 3? – Graham Kemp Aug 29 '17 at 06:23
  • No, all conditions are listed and no information was omitted – Daniel Aug 29 '17 at 06:29