1
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ $\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. $\endgroup$ – Derek Elkins left SE Aug 29 '17 at 7:03
  • $\begingroup$ I thought I could apply $y$ at the $\lambda z$ by doing $[y/z] z$ $\endgroup$ – Daniel Aug 29 '17 at 22:48
  • $\begingroup$ 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$). $\endgroup$ – Derek Elkins left SE Aug 29 '17 at 23:08
0
$\begingroup$

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$

$\endgroup$
  • $\begingroup$ 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$ ? $\endgroup$ – Daniel Aug 29 '17 at 5:19
  • $\begingroup$ Is there a condition missing from definition 3? $\endgroup$ – Graham Kemp Aug 29 '17 at 6:23
  • $\begingroup$ No, all conditions are listed and no information was omitted $\endgroup$ – Daniel Aug 29 '17 at 6:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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