有限理解无限列表

Question

我在ghci中输入以下内容,认为会发生以下两种情况之一:1)解释器会挂起,搜索无限列表中的每个成员以匹配谓词; 或者2)通过幕后的Haskell jujitsu,解释器会以某种方式弄清楚序列终止于4并停在那里.

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

结果1是发生了什么.现在,结果2有很多要求.但是既然人类可以证明序列终止于4,那么可能有办法让翻译来做吗？这可以以它终止的方式重写吗？事实上,有过一个谓语,这使得有限的理解出无限的名单？

Answer 1

但是既然人类可以证明序列终止于4,那么可能有办法让翻译来做吗？

在这个简单的例子中,是的.但是>n对于某些人来说n,不存在用于确定某个表达式对于所有自然数是真还是假的通用算法,因为Haskell是图灵完备的,因此不可能证明表达式甚至代表所有自然数的终止程序.

即使你的表达式仅限于基本的整数算术,在一般情况下它的真实性仍然是不可判定的.

这可以以它终止的方式重写吗？

正如Mog在评论中写道的那样takeWhile (< 5) [1..].

Answer 2

takewhile 如上所述,是您特定问题的正确解决方案.

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