我正在阅读 Richard Bird 的《用 Haskell 进行函数式思考》一书，遇到了关于无限列表归纳的链完成的概念。
它说:
A property P is called chain complete if whenever xs0, xs1,... is a sequence of partial lists with limit xs, and P(xsn) holds for all n, then P(xs) also holds.
作为链完整属性的一个例子，它说:
All equations e1 = e2, where e1 and e2 are Haskell expressions involving universally quantified free variables, are chain complete.
我很难理解这个例子如何适合链完成的属性。它还指出不等式 e1 =/= e2 不一定是链完整的。我如何根据这种链完整性来理解这些属性？
顺便说一句，这不一定是关于 Haskell 的问题，而是数学方面的问题。
最佳答案
这是一个例子。
假设您有一个递增的列表序列xs_1, xs_2, ...有限制 xs .
对于每个 k , 我们有 map id xs_k等于 xs_k .
通过链的完整性(AKA Scott 连续性)，我们得到 map id xs是 xs .
这为我们提供了一种方法来证明限制列表上的属性 xs ，这可能是无限的，通过仅在它们的近似值上验证它们 xs_k .
这里的直觉是，对于 xs成为一个限制列表，每个 xs_k必须等于 xs或者更短的前缀 x1:x2:...:xn:undefined .注意未定义的尾部，表示循环计算(例如无限递归)。因此，如果我们比较 f xs_k和 f xs ，我们发现后者必须至少与前者一样终止。这里的一般想法是，如果我们传递更多或定义的输入，我们将得到更多或定义的输出。在数学上，这个概念被 Scott 排序的单调性所捕获。
斯科特欧米茄连续性或链完整性更进一步。它告诉我们 f xs与序列f xs_k的极限完全相同.最终结果近似于 f 的结果在近似值上。粗略地说，可以通过使输入收敛来使输出收敛。
不平等在链式完整的方式中不起作用。确实，采取xs = [0..]作为一个无限列表和近似值 xs_k = 0:...:k:undefined .很明显xs_k不等于 xs , 对于每个 k .但是我们不接受这种不等式的限制，这将表明 xs不等于 xs .
最后，这里的主题相当广泛。如果您有兴趣，我建议您阅读有关指称语义的内容，例如阅读 Winskel 的书。
关于haskell - 链完整的概念是什么？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/45529201/