3
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

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).

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks so much for the elegant counter-example. Do you know if the same would hold when only considering normalizing terms? I think it's an important restriction because a normalizing term is meaningful as a function and we could see how it differs semantically from the identity. $\endgroup$
    – GeoffChurch
    Jul 22, 2021 at 22:24
  • 1
    $\begingroup$ 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! $\endgroup$
    – Damiano Mazza
    Jul 24, 2021 at 6:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.