1
$\begingroup$

I am studying from Sorensen's book "Lectures on the Curry-Howard isomorphism" and it is there asked if there exists a combinator s.t. $M \rightarrow_w Μ$ (one step of weak reduction only), i.e. a combinator reducing to itself in only one step.

I think that there isn't and I want to know if my proof is incorrect.

I am using induction on the definition of the weak reduction.

Base: Let $M=KFG$, for some $F,G$. Then $M \rightarrow_w F$. But $F\neq M$. So it can't be the case. Let $M=SFGH$, for some $F,G,H$. Then $M \rightarrow_w FH(GH)$. But $M\neq FH(GH)$, otherwise $S=F=H$ and $SSGS \rightarrow_w SS(GS)\neq SSGS$. So it can't be the case.

Induction step: $M=A_1A_2$.

If $A_1\rightarrow_w A_1$, $A_1=M_2M_1M_3$ for some $M_2,M_3$, (probably "empty" combinators, without loss of generality) and $M_1$ such that $M_1=KFG\rightarrow_w F$ or $M_1=SFGH\rightarrow_w FH(GH)$. Then $M_2FM_3=A_1$ or $M_2FH(GH)M_3=A_1$ but that can't be the case because of the base step.

My intuition murmurs that something is going wrong; it could be that $M$ reduces to two different combinators in induction step or that $M_1$ can't be just $KFG$ or $SFGH$ or that I skipped something else.

So the question: is the proof correct? If not, what did I miss?

$\endgroup$
2
  • $\begingroup$ What about $\Omega = (λx.xx)(λx.xx)$? $\endgroup$ Commented Sep 25, 2023 at 16:43
  • $\begingroup$ @sparusaurata That is a lambda term. The problem is in combinatory logic. And SII(SII) doesn't reduce to itself in one step, but in five. Sorry for that. I put a wrong tag. $\endgroup$ Commented Sep 25, 2023 at 18:12

0

You must log in to answer this question.

Browse other questions tagged .