# Fixed points of fixed-point combinator?

A fixed point f of a fixed-point combinator would be a function that has itself as a fixed point: f(f) = f. The only such function I could come up with is id, which by definition has the apparently stronger property that id(x) = x for all x. Equivalently, everything is a fixed point of id.

My question is: is this actually a stronger property (in untyped lambda calculus), or is id the only function with f(f) = f?

If by "$$=$$" you mean $$\beta$$-equality, then the answer is yes, $$MX=X$$ for all $$X$$ is a stronger property than $$MM=M$$.
For example, let $$A := \lambda a.aa(aa)$$ (to save parentheses, I am using the standard left-associative notation for application; in your notation, the above term would be $$\lambda a.a(a)(a(a))$$) and take $$M := AA.$$ We clearly have $$M\to MM$$ and therefore $$MM=M$$. On the other hand, for any normal form $$N$$, $$MN\neq N$$, because $$MN$$ does not normalize (in fact, $$M$$ does not have a head normal form).
• It's easy to see that $MM=M$ for $M$ normalizable implies that $NN\to^\ast N$ where $N$ is the normal form of $M$. I can't quickly come up with an example of normal term different from the identity which reduces to itself when applied to itself, but I'm not convinced it does not exist... I honestly don't know! Jul 24, 2021 at 6:12