我在ghci中键入以下内容，认为会发生以下两种情况之一:1)解释器将挂起，在无限列表的每个成员中搜索与谓词的匹配；或2)通过幕后Haskell柔术，口译员会以某种方式弄清楚序列在4处终止并在此处停止。
[x | x <- [1..],5>x]
结果1是发生了什么。现在，结果2有很多要求。但是，既然人类可以证明序列在4处终止，那么是否有办法让解释器来做呢？可以用终止的方式重写它吗？实际上，是否有谓词可以从无限列表中进行有限理解？
最佳答案
但是，既然人类可以证明序列在4处终止，那么是否有办法让解释器来做呢？
在这种简单情况下，可以。但是，由于Haskell是图灵完备的，因此不存在通用的算法来确定某个>n的所有自然数n的表达式是真还是假，因此无法证明该表达式甚至代表所有自然数的终止程序。
即使您的表达式仅限于基本整数算术运算，在一般情况下其真相仍不可确定。
可以用终止的方式重写它吗？
正如Mog在评论中所写，它是takeWhile (< 5) [1..]。
关于haskell - 无限列表的有限理解，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/10336392/