时间戳

首页 > 解决方案 > 最小固定点，最大固定点

haskell - 最小固定点，最大固定点

问题描述

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

标签： haskellfixpoint-combinators

解决方案

在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。）

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

推荐阅读