指称语义，证明不动点迭代产生最小不动点

Question

我正在研究 denotational semantics 上的 Haskell wikibook 部分，我有点坚持这个练习：

证明定点迭代得到的不动点开始 也是最小的一个，它比其他任何一个都小 固定点。 （提示： 是我们 cpo 的最小元素，而 g 是 单调）。

以下陈述定义了导致练习的概念的核心（我认为）：

其中 f 是阶乘函数，并且显示为 g 的不动点，假设 g 是连续的。

我想我基本上理解了显示 g(f) = f 的部分，但我真的不知道该怎么做这个练习。据我了解，阶乘函数 f 是最小固定点（至少基于 运算符），但我完全不清楚将函数与 进行比较意味着什么（直观地），更不用说除了示例中显示的最小固定点之外，我如何找到固定点。

我了解 比其他所有内容都少，并且我了解由于 g(x) 是单调的，如果我将其应用于两件事，其中一个小于另一个，结果仍将遵循此顺序.

我想我会从取一些函数 f' 并假设 开始证明。如果是这样的话，通过 g 的单调属性，我可以证明。如果我可以证明 g(f') = g(f) 或 f' = f 我认为证明是完整的，但我不知道如何证明这一点。

Answer 1

让x 成为序列bot, g(bot), g(g(bot)), ... 的sup/最小上界。让y 是g 的任意不动点（单调）。我们要证明x <= y。

通过对迭代次数的归纳，很容易看出序列中的每个元素都是<= y。事实上，它对bot 是微不足道的，如果z 是<= y，我们得到g(z) <= g(y) = y。

所以，y 是序列的上限。但是x 最少，所以x <= y。 QED。