如何使用 QuickCheck 测试函数是否终止？答案

【问题标题】：How do I use QuickCheck to test if a function terminates?如何使用 QuickCheck 测试函数是否终止？
【发布时间】：2016-08-31 15:19:24
【问题描述】：

我想使用 QuickCheck 来测试一个函数以确保它终止（没有无限递归，没有抛出异常等）。这就是我目前所做的：

f :: Int -> Int -> Int

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

有没有更好（更具表现力和惯用语）的方式？

【问题讨论】：

【解决方案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 *

【讨论】：

我不想证明函数终止（这是停止问题），我只是想确保我在实现中没有犯任何错误这将导致无限递归。我想以明确表达我意图的方式编写我的测试。
查看我的编辑，这解释了为什么seq 在这里不合适。
好吧，f 返回一个Int，所以 WHNF 和 NF 是一样的，对吧？但在一般情况下，你绝对是对的。
你是对的，一般来说是不可判定的，但是有很多方法可以证明许多函数的终止。许多定理证明器和软件验证系统都必须这样做。对于函数式语言，一个常见的想法是在输入项上定义一个明确定义的顺序，然后通过归纳表明递归调用的参数按该顺序减少。然后函数必须终止。当然，这些系统并不适用于所有功能，但它可以经常使用。
是的，如果您只返回Int，那么您无需担心seq 与deepseq。

【解决方案2】：

我可能不会打扰，我只是测试其输出的其他属性。

以任何方式检查f x y 输出的任何属性都将至少进行与prop_fTerminates 一样多的终止检查，那么为什么要浪费时间加倍检查呢？

如果由于某种原因“f x y terminates”是您可以测试的关于 f 的唯一属性，那么您所得到的似乎是合理的。

【讨论】：