0
$\begingroup$

Given a CL term $E$, can there exist multiple non-equivalent fixed points for $E$?

I think: any fixed point of $E$ can be expressed as $Y(E)$, this expression cannot reduce to multiple non-equivalent forms, due to confluence. So, I think that any CL term can have only 1 fixed point.

Is my logic correct? All ideas regarding this problem are welcome.

Edit:

Realized just now, the identity combinator is a CL term with multiple non-equivalent fixed points. But then, if we consider the term $Y(I)$, this must have multiple non-equivalent forms, corresponding to the multiple fixed points of $I$. But how is that justifiable under confluence?

Edit 2:

$Y(I)$ is nothing but the omega combinator. I think I have got it now. Even when a CL term has multiple fixed points, applying that CL term to Y gives us only one possible fixed point. Is that correct?

$\endgroup$

1 Answer 1

2
$\begingroup$

This may be useful to construct (partial) answers to your question: In general, there are infinitely many non-β-equivalent fixed-point combinators in λ-calculus. Consider $$ \delta := λy.λx.x(yx) =_β \mathsf{SI}, $$ then the terms $Y_n$ defined by $$ Y_0 := Y \qquad Y_{n+1} := Y_n \delta $$ are fixed points combinators, and $Y_i \neq_β Y_j$.

This is called the Böhm-van der Mey sequence. What I know about it comes from Barendregt and Manzonetto (2022), who cite Klop (2007).

$\endgroup$
1
  • $\begingroup$ Thanks for your help. $\endgroup$
    – Soham Saha
    Feb 27 at 11:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .