如何判断一个列表是不是是无限的？

Posted 2023-02-23

【中文标题】如何判断一个列表是不是是无限的？

【英文标题】：How to tell if a list is infinite?如何判断一个列表是否是无限的？

【发布时间】：2011-11-14 08:43:51

【问题描述】：

有没有办法判断 Haskell 中的列表是否无限？原因是我不想将length之类的函数应用到无限列表中。

【问题讨论】：

关于您在 cmets 中的问题“不要无限结构使我的程序非常脆弱”：是和否。您不妨换一种说法：依赖于有限结构的算法使您的程序非常容易受到攻击。但实际上，如果分开处理，两者都是完全可以的。错误通常很容易通过简单测试程序检测：在这样的程序中，结构要么非常小（如 3 个元素 => 程序应该很快完成）或无限大。

【参考方案1】：

还可以通过设计分离有限列表和无限列表，并为它们使用不同的类型。

不幸的是，Haskell（与 Agda 不同）不允许您强制数据结构始终是有限的，您可以使用 total functional programming 的技术来确保这一点。

您可以将无限列表（AKA 流）声明为

data Stream a = Stream a (Stream a)

它没有任何方法可以终止一个序列（它基本上是一个没有[] 的列表）。

【参考方案2】：

我们不需要解决停止问题就可以安全地调用“长度”。我们只需要保守一点；接受所有有有限性证明的东西，拒绝所有没有的东西（包括许多有限列表）。这正是类型系统的用途，因此我们使用以下类型（t 是我们的元素类型，我们忽略它）：

terminatingLength :: (Finite a) => a t -> Int
terminatingLength = length . toList

Finite 类将只包含有限列表，因此类型检查器将确保我们有一个有限参数。 Finite 的成员资格将是我们有限性的证明。 “toList”函数只是将有限值转换为常规 Haskell 列表：

class Finite a where
  toList :: a t -> [t]

现在我们的实例是什么？我们知道空列表是有限的，所以我们创建了一个数据类型来表示它们：

-- Type-level version of "[]"
data Nil a = Nil
instance Finite Nil where
  toList Nil = []

如果我们将一个元素“cons”到一个有限列表上，我们会得到一个有限列表（例如，如果“xs”是有限的，那么“x:xs”就是有限的）：

-- Type-level version of ":"
data Cons v a = Cons a (v a)

-- A finite tail implies a finite Cons
instance (Finite a) => Finite (Cons a) where
  toList (Cons h t) = h : toList t -- Simple tail recursion

任何调用 terminatingLength 函数的人现在都必须证明他们的列表是有限的，否则他们的代码将无法编译。这并没有消除停机问题，但我们已将其转移到编译时而不是运行时。编译器在尝试确定 Finite 成员资格时可能会挂起，但这比在给定一些意外数据时让生产程序挂起要好。

请注意：Haskell 的“ad-hoc”多态性允许在代码的其他点声明几乎任意的 Finite 实例，并且 terminatingLength 将接受这些作为有限性证明，即使它们不是。不过，这还不错。如果有人试图绕过您代码的安全机制，他们会得到应得的错误；)

【讨论】：

要了解这背后的灵感，请看 Conor McBride 的“Faking It: Simulating Dependent Types in Haskell”

【参考方案3】：

将length 应用于未知列表通常不是一个好主意，这实际上是由于列表无限，而且在概念上是因为通常事实证明您实际上并不关心长度。

你在评论中说：

我是 Haskell 的新手，所以现在，无限结构不是让我的程序非常脆弱吗？

不是真的。虽然我们中的一些人希望有更好的方法来区分必然有限和必然无限的数据，但当您创建、处理和检查 惰性结构增量。计算长度显然不是增量的，而是检查长度是否高于或低于某个截止值是，而且通常这就是你想做的全部！

一个小例子是测试非空列表。 isNonEmpty xs == length xs > 0 是一个糟糕的实现，因为它检查了无限数量的元素，而只检查一个就足够了！比较一下：

isNonEmpty [] = False
isNonEmpty (_:_) = True

这不仅可以安全地应用于无限列表，而且在有限列表上效率也更高——它只需要恒定的时间，而不是与列表长度呈线性关系的时间。也是how the standard library function null is implemented。

为了将这一点概括为相对于截断点的长度测试，您显然需要检查与要比较的长度一样多的列表。我们可以做到这一点，仅此而已，使用标准库函数drop：

longerThan :: Int -> [a] -> Bool
longerThan n xs = isNonEmpty $ drop n xs

给定一个长度n 和一个（可能是无限的）列表xs，如果存在xs 的第一个n 元素，则删除它们，然后检查结果是否为非空。因为如果n 大于列表的长度，drop 会生成空列表，所以这对所有正数n 都有效（唉，标准库中没有非负整数类型，例如自然数） .

---

这里的关键点是，在大多数情况下，最好将列表视为迭代流，而不是简单的数据结构。如果可能，您希望执行转换、累积​​、截断等操作，或者生成另一个列表作为输出，或者只检查已知有限数量的列表，而不是尝试一次性处理整个列表。

如果您使用这种方法，您的函数不仅可以在有限 和 无限列表上正常工作，而且它们还将从惰性和 GHC 的优化器中受益更多，并且可能运行得更快并且使用更少的内存。

【讨论】：

“计算长度显然不是增量的，但是检查长度是高于还是低于某个截止值是”——要清楚，if length xs < n then ... 是错误的做法那:)

【参考方案4】：

Halting Problem 首先被证明是无法解决的，方法是假设存在一个停止预言机，然后编写一个与预言机所说的相反的函数。让我们在这里重现：

isInfinite :: [a] -> Bool
isInfinite ls = - Magic! -

现在，我们要创建一个列表 impossibleList，它与 isInfinite 所说的相反。所以，如果impossibleList 是无限的，它实际上是[]，如果它不是无限的，它是something : impossibleList。

-- using a string here so you can watch it explode in ghci
impossibleList :: [String]
impossibleList =
    case isInfinite impossibleList of
        True -> []
        False -> "loop!" : impossibleList

在 ghci 中使用 isInfinite = const True 和 isInfinite = const False 亲自尝试一下。

【讨论】：

没有什么比对角化参数更能永远毁掉一切的了。我责怪康托尔开始了整个事情。

你不能用一个类似的“证明”来证明不可能检查一个列表是否为非空吗？只需将isInfinite 替换为isNonEmpty。但是isNonEmpty显然是可以实现的。

@C. A. McCann：这段代码没有表明“isInfinite 的任何实现都不能在所有列表上工作”，因为impossibleList 不是一个列表（它是⊥）。否则，您可以说它也表明 isNonEmpty 的任何可能实现都不能在所有列表上工作，正如我在之前的评论中所说的那样。

@C. A. McCann：这不仅没有说明isInfinite，也没有说明可判定性或停机问题。考虑f::Int32->Bool 形式的函数。由于可能的输入数量有限，因此它们都是可判定的。但是很容易使用与上述几乎相同的构造来“证明”任何非平凡的f 不能为所有值计算。例如，对于f x = x>0，使用impossibleValue = if (f impossibleValue) then 0 else 1

@C. A. McCann：前提是isInfinite 决定给定列表的无限性，即它为任何无限列表返回True，为任何有限列表返回False......如果你给它⊥它会做什么既非这里也非那里。我们只能通过传递一个有限列表并证明它不返回False（计算为True或⊥）或传递一个无限列表并证明它不返回True（计算为False或⊥）。给它 ⊥ 并显示它产生 ⊥ 仅表明 isInfinite 是严格的。

【参考方案5】：

isInfinite x = length x `seq` False

【讨论】：

我不明白，这个定义isInfinite [1,2,3]给出False，而isInfinite [1..]也给出False。

@alexraasch：不，那里的seq 确保它计算长度——如果列表是无限的，这当然永远不会完成。因此，如果列表是有限的（这是正确的），它要么给出False，要么它永远不会完成，因此根本不会回答。一个不存在的答案不能被称为不正确，不是吗？ :] 是的，这是一个笑话，如果这不是很明显的话。

【参考方案6】：

不，您最多只能估计。请参阅Halting Problem。

【讨论】：

好吧，这很可悲。没想到这是停机问题的一个实例。

好吧，它即将告诉您，您的程序是否会无限期地运行——这对于无限列表来说是正确的。也许其他人可以为您提供更好的答案。

好吧，您可以创建一个列表，返回头指向的图灵机中磁带上的当前元素。如果你能说出列表是否是有限的，你就可以解决停机问题。

@Alexander Raasch：没有甲骨文。您在 Haskell 中构建了一个图灵机模拟器，它提供了一个显示头部如何移动的列表。列表结束：程序完成。

@ShreevatsaR：采用任意通用递归函数，将其重写为展开操作，该操作生成在每个递归步骤中获取的连续值列表，并在达到基本情况时生成单例列表。如果原始函数终止，则列表将是有限的，但任意通用递归函数正是图灵机可计算的那些。因此，在任意列表上工作的isFinite 函数必然是一个停止预言。