我在 ghci 中输入了以下内容，认为会发生以下两种情况之一： 1）解释器会挂起，搜索无限列表的每个成员以匹配谓词；或 2）通过幕后的 Haskell 柔术，解释器会以某种方式找出序列在 4 处终止并停在那里。
[x | x <- [1..],5>x]
结果 1 就是发生了什么。现在，结果 2 要求很高。但是既然人类可以证明序列在 4 处终止，那么有没有办法让解释器来做呢？是否可以将其重写为终止？事实上，有没有一个谓词可以从无限列表中产生有限的理解？
问问题
3205 次
3 回答
25
但是既然人类可以证明序列在 4 处终止，那么有没有办法让解释器来做呢？
在这个简单的情况下，是的。但是不存在一个通用算法来确定一个表达式>n对于 some的所有自然数是真还是假n，因为 Haskell 是图灵完备的，所以不可能证明一个表达式甚至代表所有自然数的终止程序。
即使您的表达式仅限于基本整数算术，它的真实性在一般情况下仍然无法确定。
是否可以将其重写为终止？
正如 Mog 在评论中所写，它是takeWhile (< 5) [1..].
于 2012-04-26T15:25:26.503 回答
8
takewhile如上所述，是针对您的特定问题的正确解决方案。
但是，这只是因为在您的情况下，所有可接受的参数都在所有不可接受的参数之前，并且一般列表理解不遵守该约束。当然可以向解释器添加符号推理，以便它可以证明没有其他元素是可接受的，然后终止。（事实上，Haskell 中复杂的类型系统在实现这种推理时非常有用。）但是将它添加到标准[|]运算符中没有意义，因为检测器必须在所有被评估的列表推导上运行，并且除了更多的计算费用外，通常不会做出任何贡献。
于 2012-04-26T15:29:09.487 回答
2
“但既然人类可以证明序列在 4 处终止，那么有没有办法让解释器来做呢？”
好问题。困难的不是证明它在 4 处终止，而是它可能在 4 处终止的想法，然后是这种情况确实如此的洞察力。
于 2012-04-26T21:58:30.153 回答