haskell - “所有（==1）[1,1..]”没有终止的数学意义是什么？

Answer 1

价值

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

是序列的最小上界

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

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

这是使用 Haskell 的指称语义，并且不（直接）依赖于选择任何特定的评估策略。

Answer 2

在编程中，我们使用的不是经典逻辑，而是直觉（构造）逻辑。我们仍然可以将类型解释为定理，但我们并不关心这些定理的真实性；相反，我们讨论它们是否具有建设性的可证明性。即使all (== 1) [1, 1 ..]是true，我们也无法在 Haskell 中证明它，所以我们得到 ⊥ （这里是一个无限循环）。

在建设性逻辑中，我们没有排中律，因此也没有双重否定消除。Haskell 函数类型all (== 1) :: [Int] -> Bool不代表定理 [Int] → Bool，这将是一个全函数；它表示定理 [Int] → ¬¬Bool。如果all可以通过产生一个结果来证明该定理，那么该结果将是类型Bool; 否则，结果为底部。

Answer 3

我对可计算性的了解不足以正确回答这个问题，但我确实从语言设计的简单性中得到安慰。在这种情况下，我发现它简单而优雅，all不需要知道任何关于它给出的输入。可以说，人类对您给出的片段进行推理更容易。

当然，现在无限列表理解以某种方式告诉all它是一个无限列表会很好。但是……这就是它所说的“具有那种价值”。拥有更多关于重复序列的通用元数据对于优化目的会更成功，但我认为简单性会降低，并引入复杂性。