2
$\begingroup$

I'm trying to understand more about $\lambda$-calculus through exercises so I'm stuck with this one:

Being:

  • $M$ a $\lambda$-term without normal form (we can't find a normal form, such as the term $(\lambda x. x x) (\lambda x. x x)$), and

  • $N$ a $\lambda$-term with a normal form.

Can we find an expression such as

$$(M N)$$

that has a normal form?

Thanks for the help.

$\endgroup$
1
$\begingroup$

Consider $(\lambda f.f\,A)(K B)$, where $A$ is any $\lambda$-term with no normal form (e.g., $(\lambda x. x x)(\lambda x. x x)$), $K$ is the $K$-combinator ($\lambda x .\lambda y. x$) and $B$ is any normal form $\lambda$-term, (e.g., $\lambda x.x$). Then $(\lambda f.f\,A)$ has no normal form, but if you choose the leftmost $\beta$-redex at each step you have:

$$ (\lambda f.f\,A)(K B) \rightsquigarrow K B A \rightsquigarrow B $$

So $B$ is a normal form for $(\lambda f.f\,A)(K B)$.

$\endgroup$
  • $\begingroup$ Now I see, thanks! $\endgroup$ – Pau Muñoz Apr 2 '18 at 20:45

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.