反对直接递归终止的魔鬼代言人

魔鬼代言人是指为确定某一主张的有效性而对其提出反对意见的人，并非出于坚定的反对立场。我们关注一种反对程序终止的魔鬼代言人。他通过生成一个可导致原程序不终止的恶意程序来实现这一点。通过检查并运行该恶意程序，人们可以洞察导致不终止的潜在原因，并生成终止性的反例。我们使用并发编程语言约束处理规则（CHR）来介绍我们的方法。与其他声明式语言类似，不终止通过无界递归发生。给定一个自递归规则，我们从中自动生成一个或多个魔鬼规则。魔鬼规则的构造是直接的，不涉及猜测。魔鬼规则可以很简单。例如，对于单递归规则，它们是非递归的。我们证明，魔鬼规则在以下意义上是最大恶意的：对于任何包含该自递归规则的程序，以及该程序中通过该规则的任何无限计算，都存在一个仅使用该递归规则和魔鬼规则的相应无限计算。在这种情况下，恶意规则充当了不终止的有限见证。另一方面，如果魔鬼规则未表现出无限计算，则该递归规则是无条件终止的。我们还识别出通过对魔鬼规则进行静态分析即可判定递归规则终止或不终止的情况。