haskell - 如何使用 QuickCheck 来测试函数是否终止？

Question

我想使用 QuickCheck 来测试函数以确保它终止(没有无限递归、没有抛出异常等)。这就是我现在所做的:

f :: Int -> Int -> Int

prop_fTerminates :: Int -> Int -> Bool   -- say
prop_fTerminates x y = f x y `seq` True

有更好的(更具表现力和惯用的)方式吗？

Answer 1

这是halting problem 。没有算法能够告诉您函数是否终止。

特别是，如果您愿意等待足够长的时间，您可能能够得到积极的结果(即，如果函数确实终止，这个命题会告诉您)。但仅通过等待，您永远无法知道此函数未终止和此函数尚未终止之间的区别。

您可以实现类似此函数是否在时间 T 内终止之类的检查，这可能适合您的需求。

<小时/>

编辑 正如所写，您的函数无法满足您的要求。考虑一下

> let f = 1:f
> f `seq` True
True

原因是 seq 的计算结果仅为 weak head normal form 。相反，您可以使用 deepseq 来深入评估数据结构，

> import Control.DeepSeq (deepseq)
> f `deepseq` True
* never returns *