在像 Haskell 这样的惰性非全语言中，最小固定点如何与最大固定点重合。完全部分订单的连续性与此有什么关系？
问问题
765 次
1 回答
6
在CPO（我们将类型解释为）中，任何递增链都有一个最小上限。
这是一个应该传达直觉的示例，为什么在 CPO 领域中，最小不动点和最大不动点重合。考虑以下仿函数，为了简洁而滥用列表符号：
data ListF a x = [] | a : x
它最大的固定点是 Haskell 列表的类型（可能是无限的，也可能是部分的）。它的最小不动点呢？必须包含以下元素（Fix省略构造函数）：
0 : _|_
0 : 1 : _|_
0 : 1 : 2 : _|_
...
并且它们形成一个递增链，所以必须有一个最小上界，它必须是自然整数的无限列表0 : 1 : 2 : ...。所以 的最小不动点ListF包含无限列表，因此与最大不动点重合。
正如评论中所指出的，最大不动点由类型给出的说法[]可能需要澄清。例如，BigList由大序数索引的列表中的某些 CPO " " 会不会产生更大的固定点？
可以首先证明[]满足最终ListF-余代数的定义。那么，最终余代数的一个性质是它们对于同构是唯一的。因此，由较大序数索引的列表将导致非同构 CPO，因此它不能是最终的代数。
我可以停在那里，但等等，不是BigList还有一个更大的固定点ListF吗？我的结论是将问题归结为错误的术语，正式我们应该只讨论“最终的余代数”，而不是“最大的固定点”。
根据您如何定义 CPO 中函子的“不动点”以及 CPO 之间的（预）序概念，您可能会发现它BigList是 的一个不动点ListF，它大于[]，您会遇到集合论悖论当达到“最大不动点”时，最终对于 Haskell 实践者来说，以形式化“最大不动点”的方式没有任何价值，因为您实际上想要最终代数的良好属性。
（我很想知道一种直接定义排除的“定点”的方法BigList。）
因此，相反，术语“最大不动点”也可能是“最终代数”的同义词。一些直觉延续（“固定点”通常可以通过迭代来接近），有些则没有（它不是集合论意义上的“最大”）。
于 2018-08-04T12:31:08.740 回答