<p>If by &quot;<span class="math-container">$=$</span>&quot; you mean <span class="math-container">$\beta$</span>-equality, then the answer is yes, <span class="math-container">$MX=X$</span> for all <span class="math-container">$X$</span> is a stronger property than <span class="math-container">$MM=M$</span>.</p>
<p>For example, let
<span class="math-container">$$A := \lambda a.aa(aa)$$</span>
(to save parentheses, I am using the standard left-associative notation for application; in your notation, the above term would be <span class="math-container">$\lambda a.a(a)(a(a))$</span>) and take
<span class="math-container">$$M := AA.$$</span>
We clearly have <span class="math-container">$M\to MM$</span> and therefore <span class="math-container">$MM=M$</span>.  On the other hand, for any normal form <span class="math-container">$N$</span>, <span class="math-container">$MN\neq N$</span>, because <span class="math-container">$MN$</span> does not normalize (in fact, <span class="math-container">$M$</span> does not have a head normal form).</p>

CC BY-SA 4.0
2021-07-22T22:24:34.507Z
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.
GeoffChurch
CC BY-SA 4.0
2021-07-24T06:12:40.970Z
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!
Damiano Mazza
CC BY-SA 4.0
2021-07-10T20:46:37.873Z
2021-07-10T20:46:37.873Z
Damiano Mazza
<p>A fixed point <code>f</code> of a fixed-point combinator would be a function that has itself as a fixed point: <code>f(f) = f</code>. The only such function I could come up with is <code>id</code>, which by definition has the <em>apparently</em> stronger property that <code>id(x) = x</code> for <em>all</em> <code>x</code>. Equivalently, everything is a fixed point of <code>id</code>.</p>
<p>My question is: is this actually a stronger property (in untyped lambda calculus), or is <code>id</code> the only function with <code>f(f) = f</code>?</p>

<lambda-calculus><fixed-points>
Fixed points of fixed-point combinator?
GeoffChurch
# Fixed points of fixed-point combinator?

(Asked by: username_0 on 2021-07-09)

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`?

**Tags:** lambda-calculus, fixed-points


---

## 1 answers

### Answer by username_1 on 2021-07-10. Score: 5 | Accepted answer

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

> **Comments:**
> **username_0**: 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.  
> **username_1**: 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!  

---

