The*_*kle 10 math computer-science haskell data-structures infinite-recursion
直觉上,我希望"数学"答案all (==1) [1,1..]是True因为列表中只包含1的所有元素都等于1.但我理解"计算上",评估无限列表以检查事实上,每个元素实际上等于1将永远不会终止,因此表达式将"评估"到底部或?.
我发现这个结果反直觉而且有点令人不安.我认为列表无限的这个事实在数学上和计算上都会混淆这个问题,我很乐意听到在这个领域有一些见解和经验的人
我的问题是,哪个是数学上最正确的答案？?还是True？关于为什么一个答案比另一个答案更正确的一些详细说明也将受到高度赞赏.
编辑:这可能间接地与库里 - 霍华德同构(程序是证明和类型是定理)和哥德尔的不完备性定理有关.如果我没记错的话,其中一个不完备性定理可以(非常粗略地)总结为"足够强大的形式系统(如数学或编程语言)无法证明所有可以在系统中表达的真实陈述"
Rei*_*ton 23
价值
all (==1) [1,1..]
是序列的最小上限
all (==1) (?)
all (==1) (1 : ?)
all (==1) (1 : 1 : ?)
...
并且该序列的所有项都是⊥,所以最小上界也是⊥.(所有Haskell函数都是连续的:保留最小上限.)
这是使用Haskell 的指称语义,并不(直接)依赖于选择任何特定的评估策略.