AI 中文总结
本文通过构造不变量追踪变量出现，证明在弱等价下BMI组合逻辑中不存在不动点组合子，否定了斯穆里安1985年提出的问题。
AI 中文摘要
设 $B$ 为蓝鸟组合子，其归约规则为 $Bxyz \to_{w} x\left(yz\right)$；设 $M$ 为模仿鸟组合子，其归约规则为 $Mx \to_{w} xx$；设 $I$ 为恒等鸟组合子，其归约规则为 $Ix \to_{w} x$。对于固定的变量 $x$，我们构造了一个 $BMI$-项 $u$ 关于 $\to_{w}$ 的不变量 $\mathrm{Tr}_{x}\left(u\right)$。该不变量追踪 $u$ 的最左最内归约序列中 $x$ 的出现情况。然后我们证明，对于每个不含 $x$ 的 $BMI$-项 $Y$ 以及每个 $r\geq 1$，都有 $\mathrm{Tr}_{x}\left(Yx\right) \neq \mathrm{Tr}_{x}\left(x^{r}\left( Yx \right)\right)$。因此，在弱等价下，$BMI$-组合逻辑中不存在不动点组合子。这为斯穆里安于1985年提出的问题给出了否定答案。
英文摘要
Let $B$ be the bluebird combinator with reduction rule $Bxyz \to_{w} x\left(yz\right)$, let $M$ be the mockingbird combinator with reduction rule $Mx \to_{w} xx$, and let $I$ be the identity bird combinator with reduction rule $Ix \to_{w} x$. A fixed-point combinator, called a sage bird by Smullyan, is a closed term $Y$ such that, for a fresh variable $x$, $Yx$ is equivalent to $x\left(Yx\right)$ under these reduction rules. For a fixed variable $x$, we construct an invariant $\mathrm{Tr}_{x}\left(u\right)$ of a $BMI$-term $u$ with respect to $\to_{w}$. This invariant traces the occurrences of $x$ in the leftmost-innermost reduction sequence of $u$. We then prove that $\mathrm{Tr}_{x}\left(Yx\right) \neq \mathrm{Tr}_{x}\left(x^{r}\left( Yx \right)\right)$ for every $x$-free $BMI$-term $Y$ and every $r\geq 1$. Consequently, there exists no fixed-point combinator in $BMI$-combinatory logic. This provides a negative answer to the problem posed by Smullyan in 1985.
