有限理解无限列表 [英] Finite comprehension of an infinite list

问题描述

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

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

结果1发生了什么。现在，结果2有很多要求。但是由于人类可以证明序列终止于4，所以可能有办法让译员去做？这可以重写，它会终止吗？事实上，是否有一个谓词使得有限的理解超出了无限列表？

解决方案

但是由于一个人可以证明序列终止于4，所以可能有办法让解释器做到这一点吗？

在这个简单的例子中，是的。但是，对于某些 n > n 而言是真还是假因为Haskell是图灵完备的，所以不可能证明表达式甚至代表所有自然数的终止程序。

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

这可以重写成它会终止吗？

由于Mog在评论中写道，它是 takeWhile（< 5）[1 ..] code>。


I typed the following into ghci, thinking that one of two things would happen: 1) The interpreter would hang, searching every member of an infinite list for matches to a predicate; or 2) through behind-the-curtains Haskell jujitsu, the interpreter would somehow figure out that the sequence terminates at 4 and stop there.

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

Outcome 1 was what happened. Now, outcome 2 was a lot to ask for. But since a human can prove that the sequence terminates at 4, might there be a way to get the interpreter to do it? Could this be rewritten in such a way that it does terminate? In fact, is there ever a predicate which makes a finite comprehension out of an infinite list?

解决方案

But since a human can prove that the sequence terminates at 4, might there be a way to get the interpreter to do it?

In this simple case, yes. But there cannot exist a general algorithm to determine if an expression is true or false for all natural numbers >n for some n, because Haskell is Turing-complete, so it's impossible to prove that an expression even represents a terminating program for all natural numbers.

Even if your expression were limited to basic integer arithmetic, its truth would still be undecidable in the general case.

Could this be rewritten in such a way that it does terminate?

As Mog wrote in the comment, it's takeWhile (< 5) [1..].

这篇关于有限理解无限列表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！