haskell - "all (==1) [1,1..]"没有终止的数学意义是什么？

Question

直觉上，我希望 all (==1) [1,1..] 的“数学”答案成为 True因为列表中仅包含 1 的所有元素都等于 1。但是我理解“计算上”，评估无限列表以检查每个元素实际上是否等于 1 的过程永远不会终止，因此表达式改为“评估”到底部或 ⊥ .

我发现这个结果违反直觉并且有点令人不安。我认为列表是无限的这一事实在数学和计算上都混淆了这个问题，我很想听听任何在这个领域有一些见解和经验的人

我的问题是，哪个是数学上最正确的答案？ ⊥或 True ?
关于为什么一个答案比另一个答案更正确的一些详细说明也将不胜感激。

编辑:这可能与 Curry-Howard isomorphism 间接有关。 (程序是证明，类型是定理)和 Gödel's incompleteness theorems .如果我没记错的话，其中一个不完备性定理可以(非常粗略地)概括为“足够强大的形式系统(如数学或编程语言)不能证明可以在系统中表达的所有真实陈述”

Answer 1

值(value)

all (==1) [1,1..]

是序列的最小上界

all (==1) (⊥)
all (==1) (1 : ⊥)
all (==1) (1 : 1 : ⊥)
...

并且这个序列的所有项都是⊥，所以最小上界也是⊥。 (所有 Haskell 函数都是连续的:保持最小上界。)

这是使用 denotational semantics对于 Haskell 并且不(直接)依赖于选择任何特定的评估策略。