什么是“全部（== 1）[1,1 ..]”的数学意义？没有终止？ [英] What is the mathematical significance of "all (==1) [1,1..]" not terminating?

问题描述

直觉上，我期望 all（== 1）[1,1 ..] 的数学答案是 True 因为列表中只包含1的所有元素都等于1.但是我明白计算上是为了检查每个元素实际上等于1而评估无限列表的过程将永远不会终止，因此表达式将计算为底部或⊥。

我发现这个结果与直觉相反并且有点不安。我认为名单是一个无限的名单在数学上和计算上混淆了这个问题，我很想听到在这方面有一定洞察力和经验的人。

>我的问题是，这是数学上最正确的答案？ ⊥或 True ？
为了解答为什么一个答案比另一个答案更为正确，我们也非常感谢。

编辑：这可能间接与咖喱霍华德同构（程序是证明和类型是定理）和哥德尔的不完备定理。如果我没有记错的话，其中一个不完全性定理可以被概括为：足够强大的形式系统（如数学或编程语言）不能证明所有可以表达的真实陈述系统

解决方案

值

  all（== 1）[1,1 ..] 
  

（1）（⊥）
全部（== 1）（1：1）（$） ⊥）
全部（== 1）（1：1：⊥）
...

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

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

Intuitively, I would expect the "mathematical" answer to all (==1) [1,1..] to be True because all of the elements in a list that only contains 1s are equal to 1. However I understand that "computationally", the process of evaluating the infinite list in order to check that each element does in fact equal 1 will never terminate, therefore the expression instead "evaluates" to bottom or ⊥.

I find this result counter-intuitive and a little unnerving. I think the fact that the list is an infinite one confuses the issue both mathematically and computationally, and I would love to hear from anyone who has some insight and experience in this area

My question is, which is the most mathematically correct answer? ⊥ or True? Some elaboration as to why one answer is more correct than the other would also be much appreciated.

edit: This might indirectly have something to do with the Curry-Howard isomorphism (Programs are proofs and types are theorems) and Gödel's incompleteness theorems. If I remember correctly, one of the incompleteness theorems can be (incredibly roughly) summarised as saying that "sufficiently powerful formal systems (like mathematics or a programming language) cannot prove all true statements that can be expressed in the system"

解决方案

The value

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

is the least upper bound of the sequence

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

and all terms of this sequence are ⊥, so the least upper bound is also ⊥. (All Haskell functions are continuous: preserve least upper bounds.)

This is using the denotational semantics for Haskell and doesn't depend (directly) on choosing any particular evaluation strategy.

这篇关于什么是“全部（== 1）[1,1 ..]”的数学意义？没有终止？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！