无限列表的有限理解答案

【问题标题】：Finite comprehension of an infinite list无限列表的有限理解
【发布时间】：2012-04-26 15:18:35
【问题描述】：

我在 ghci 中输入了以下内容，认为会发生以下两种情况之一： 1) 解释器会挂起，搜索无限列表的每个成员以匹配谓词；或 2) 通过幕后的 Haskell 柔术，解释器会以某种方式找出序列在 4 处终止并停在那里。

[x | x <- [1..],5>x]

结果 1 就是发生的事情。现在，结果 2 要求很高。但是既然人类可以证明序列在 4 处终止，那么有没有办法让解释器来做呢？是否可以将其重写为终止？事实上，曾经有一个谓词可以从无限列表中产生有限的理解吗？

【问题讨论】：

takeWhile (< 5) [1..]
@Mog：虽然我同意你的评论，但你在某种程度上改变了理解的含义，这不是作弊吗？
人类证明程序某事的能力并不总是自动程序可以模仿的：您可以推断某些特定程序可以终止，但通常这是不可能的计算（这是停止问题，无法确定）。而且你可以在列表推导中编写任何你想要的代码，所以我相信在一般情况下编译器将很难推理你的列表推导。
@gcbenison：takeWhile 不是灵丹妙药。它仅在所需的输出列表是输入列表的前缀时才有效。
但是，takeWhile (< 5) [1,2,3,5,4] 将只生成 [1,2,3]。

标签： haskell

【解决方案1】：

但是既然人类可以证明序列在 4 处终止，那么有没有办法让解释器来做呢？

在这个简单的情况下，是的。但是对于某些n，不存在一个通用算法来确定一个表达式对于所有自然数>n是真还是假，因为Haskell是图灵完备的，所以不可能证明一个表达式甚至代表一个终止程序所有自然数。

即使您的表达式仅限于基本的整数算术，它的真实性在一般情况下仍然无法确定。

是否可以将其重写为终止？

正如 Mog 在评论中所写，它是 takeWhile (< 5) [1..]。

【讨论】：

那么您是否同意@Kilian 的说法：“可以向解释器添加符号推理，以便它可以证明没有其他元素可以接受然后终止”？
@gcbenison：是和不是。是的，有可能。不，它不适用于一般情况，因此口译员在某些情况下只能猜测正确答案。要么必须彻底改变语言，要么将解释器变成定理证明器。
@larsmans “将解释器变成定理证明者”，无论如何都应该如此。 ;)
哇，这是我在 Stack Overflow 上看到的关于停止问题的第一个参考。
解决方案不错，但解释为什么[x | x <- [1..],5>x] 挂起会很有用。直到我读到this answer，我才意识到我是多么愚蠢。

【解决方案2】：

takewhile 是针对您的特定问题的正确解决方案，如上所述。

但是，这只是因为在您的情况下，所有可接受的参数都在所有不可接受的参数之前，并且一般列表理解不遵守该约束。当然可以向解释器添加符号推理，以便它可以证明没有其他元素是可接受的，然后终止。（事实上，Haskell 中复杂的类型系统在实现这种推理时非常有用。）但是将它添加到标准的 [|] 运算符中是没有意义的，因为检测器必须在 all 列出已评估的推导式，除了更多的计算费用外，通常不会做出任何贡献。

【讨论】：

【解决方案3】：

“但是由于人类可以证明序列在 4 处终止，因此可能有办法让口译员来做吗？”

好问题。困难的不是证明它在 4 处终止，而是它可能在 4 处终止的想法，然后是这种情况确实如此的洞察力。

【讨论】：