在∀M FM=F中F是否可发散？YY组合子相关等式是否成立？

Great questions about untyped lambda calculus and fixed points—let’s break them down clearly, focusing on the key distinction between different types of "equality" in this system.

1. Can F be divergent in the proposition ∀M FM = F? #

First, we need to clarify what = means here—this is make-or-break for the answer:

• If we’re talking about observational equivalence: Yes, a divergent F absolutely works. Observational equivalence means two terms behave identically in every context: either both diverge forever during reduction, or both reduce to the same normal form.
  For example, take F = YY (the Y combinator applied to itself, a classic divergent term). For any term M, YYM will also diverge: when you reduce YYM, it expands to (λx.M(xx))(λx.M(xx)), which immediately reduces to M((λx.M(xx))(λx.M(xx))) = M(YYM), creating an infinite loop. Since both YY and YYM never reach a normal form, they’re observationally equivalent—so FM = F holds for all M in this sense.
• If we’re talking about strict β-convertibility: No. β-convertibility requires terms can be rewritten into each other via β-reduction steps, and YYM can’t be transformed into YY through those steps. But in most fixed-point discussions, the equality here refers to observational equivalence, so divergent F is valid.

2. Can we assert ∀M YYM = YY because both sides diverge? #

Let’s start with the derivation you mentioned: since YF is a fixed point of F, F(YF) = YF. If we also have F(YF) = F, then YF = F—meaning F is a fixed point of Y itself, and YY is indeed one such fixed point (since Y(YY) = YY).

Now, to the core question:

• Observational equivalence: Yes! As we noted earlier, all divergent terms are observationally equivalent in untyped lambda calculus. Both YYM and YY loop infinitely during reduction, so replacing one with the other in any context won’t change the outcome (the context will either diverge too, or ignore the term entirely, in which case the divergent behavior doesn’t affect the result). So in this sense, YYM = YY holds for all M.
• β-convertibility: No. YYM’s reduction loop involves applying M repeatedly, while YY’s loop is self-contained without M. These are distinct syntactic paths, and you can’t rewrite YYM into YY using β-reduction alone.

内容的提问来源于stack exchange，提问作者Alex