作者:COMEX黄金2502897957 | 来源:互联网 | 2022-12-08 17:26
在像Haskell这样的非全部惰性语言中,最小固定点与最大固定点如何重合。完整的部分订单的连续性与此有何关系?
1> Li-yao Xia..:
在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
。)
因此,相反,术语“最大固定点”也可能是“最终定律”的同义词。有些直觉会延续下去(“固定点”通常可以通过迭代来解决),有些则不能(在集合论的意义上不是“最大”)。