2
$\begingroup$

I'm trying to construct terms $M_1$, $M_2$ such that

  • $M_1$ has a normal form, but $M_1I$ doesn't.
  • $M_2$ doesn't have a normal form, but $M_2I$ does.

This is somewhat related to these two questions, $M$ doesn't have a normal form, but $MS$ has a normal form, and $MN$ has a normal form, where $M$ doesn't have a normal form but $N$ does.

I've been trying various constructions involving $K$ or $(SI)I\leadsto \omega $, but none of my attempts have worked. Do such term $M_1$, $M_2$ exist? If so, how to construct them?

J. W. Tanner
64.4k5 gold badges45 silver badges89 bronze badges
asked Jun 21 at 21:02
$\endgroup$

1 Answer 1

2
$\begingroup$

$$M_1=\lambda x.(x \Delta)\Delta$$ $$M_2=\lambda x.(x\ \mathrm{True})I(\Delta\Delta)$$ where $\Delta=\lambda y.yy$, with $\Delta\Delta$ non-normalizable,
and $K=\mathrm{True}=\lambda x y.x$

answered Jun 22 at 8:48
$\endgroup$
1
  • $\begingroup$ Pardon my ignorance, what is Δ here? And also true, is it λxy.x aka K? $\endgroup$ Commented Jun 25 at 16:23

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.