最小固定点，最大固定点答案

【问题标题】：Least fix point, greatest fix point最小固定点，最大固定点
【发布时间】：2019-01-11 23:32:29
【问题描述】：

在像 Haskell 这样的惰性非全语言中，最小固定点为何与最大固定点重合。完全偏序的连续性与此有什么关系？

【问题讨论】：

您能详细说明一下吗？您是在谈论术语级别（例如递归函数）还是类型级别（递归类型）的固定点？另请注意，在具有底部的 CPO 中，每个连续函数都有一个最小不动点，但不能有最大不动点（id @Bool 只有最小 = 底部）。（此外，如果稍微概括一下，这可能在 CS.SE 而不是 SO 的范围内更大——即使 Haskell 社区在 SO 上的范围很广，而在 CS.SE 上社区并没有那么大。）
在类型级别，函子的固定点。我发现在各个地方都提到了这一点，在 schoolofhaskell.com/user/edwardk/moore/for-less 或 cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf 中，但我无法拍照

【解决方案1】：

在CPO（我们将类型解释为）中，任何递增链都有一个最小上限。

这是一个示例，应该可以直观地理解为什么在 CPO 领域中，最小不动点和最大不动点重合。考虑以下仿函数，为了简洁而滥用列表符号：

data ListF a x = [] | a : x

它最大的不动点是 Haskell 列表的类型（可能是无限的，也可能是部分的）。它的最小不动点呢？其中必须包含以下元素（省略Fix 构造函数）：

0 : _|_
0 : 1 : _|_
0 : 1 : 2 : _|_
...

并且它们形成了一个递增链，因此必须有一个最小上界，它必须是自然整数的无限列表0 : 1 : 2 : ...。所以ListF的最小不动点包含了无限的列表，因此与最大不动点重合。

正如 cmets 中所指出的，最大不动点由类型 [] 给出的说法可能需要澄清。例如，由大序数索引的列表中的某些 CPO "BigList" 会不会产生更大的固定点？

首先可以证明[] 满足最终ListF-coalgebra 的定义。那么，最终余代数的一个性质是它们对于同构是唯一的。因此，由较大序数索引的列表将导致非同构 CPO，因此不能成为最终代数。

我可以停在那里，但等一下，BigList 不还是ListF 的更大固定点吗？我的结论是将问题归结为错误的术语，正式我们应该只讨论“最终的余代数”，而不是“最大的不动点”。

根据您如何定义 CPO 中函子的“不动点”以及 CPO 之间的（预）序概念，您可能会发现 BigList 是 ListF 的不动点，它大于@ 987654335@，当你到达“最大不动点”时，你会遇到集合论悖论，最终对于 Haskell 实践者来说，以形式化“最大不动点”的方式没有任何价值，因为你实际上想要好的最终代数的性质。

（我很想知道一种将不包括BigList 的“定点”定义为一个的直接方法。）

因此，“最大不动点”一词也可能是“最终代数”的同义词。有些直觉会延续（“固定点”通常可以通过迭代来接近），有些则不会（它不是集合论意义上的“最大”）。

【讨论】：

我对这个答案不满意——这个话题很重要，需要适当的证明。例如，即使在上面的列表示例中，为什么最终的代数除了上面提到的列表之外，还不能包含一些“更长”的序列？这里的更长，我的意思是更大的序数。结果可能取决于手头的类别，或对函子的一些假设——除非进行痛苦的形式化（IMO），否则很难看到。
您链接到的 Wikipedia CPO 页面打开时会说三个是称为 CPO 的三个不同定义。如果你说你在说哪一个，它可能会改善答案。
@Ben 该链接是由其他人添加的，所有定义都暗示了我预先声明的属性，这也是我在回答中所需要的，所以告诉它似乎没有帮助除了这种或那种风味的CPO。但这正是 omega-cpo 的定义（第三个），文章中提到前两个是严格的更精细的概念。
@chi 检查[] 是一个最终的余代数并不那么痛苦，它在同构之前是唯一的。我刚刚编辑了我的答案以扩展这一点。
谢谢。如果采用基数 [] 确实是最终的代数，并且从“大列表”到[] 的独特态射是第一个欧米茄元素的截断。