功能程序中的终止检查

Question

是否存在可以在类型检查器中指定某个计算是否可以保证终止的函数式语言？或者,你能在Haskell中做到这一点吗？

关于Haskell,在这个答案中,海报上写道

通常的思考方式是每个Haskell类型都被"解除" - 它包含⊥.也就是说,Bool对应{?, True, False}而不仅仅是{True, False}.这表示Haskell程序不能保证终止并且可以有例外.

另一方面,关于阿格达的这篇论文表明了这一点

正确的Agda程序是通过类型检查和终止检查的程序

即,所有Agda程序都将终止,并且Bool在Agda中完全对应{True, False}.

因此,例如,在Haskell中,您可以拥有类型的值IO a,这告诉类型检查器需要IO来计算相关值.你有一个类型Lifted a断言有问题的计算可能不会终止吗？也就是说,您允许非终止,但在类型系统中将其分开.(显然,就像在Agda中一样,你只能将值分成"绝对终止"和"可能不会终止")如果没有,是否有语言可以做到这一点？

Answer 1

你当然可以。然而它并不完美。根据定义，一些终止的计算必须驻留在Lifted. 这称为停机问题。

现在，在您放弃这个想法之前，这听起来并没有那么糟糕。Coq、Agda 和许多其他工具都可以很好地使用启发式方法来检查终止。

这实际上很重要的语言是 Coq 和 Agda 等你试图证明定理的语言。例如，假设我们有类型

 Definition falsy := exists n, n > 0 /\ 0 > n.
 -- Read this as, 
 --   "The type of a proof that for some number n, n > 0 and n < 0"

在 Coq 语法中。/\意味着和。现在要在 Coq 或 Agda 中证明这样的属性，我们必须编写类似的内容

Definition out_proof : falsy = ____.
-- Read this as
--   "A proof that there exists a number n < 0 and n > 0"

哪里____有证明对于某些数字n，n > 0和0 > n。现在这非常困难，因为这falsy是错误的。显然不存在既小于又大于 0 的数字。

然而，如果我们允许无限递归的非终止，

 Definition bottom_proof : falsy = bottom_proof.

这种类型检查，但是明显不一致！我们刚刚证明了一些错误！因此，定理证明助手强制执行某种形式的终止检查，否则它们就毫无价值。

如果你想务实一点，你可以使用这个提升的类型来基本上告诉类型检查器，“退出，我知道这可能不会终止，但我同意”。这对于编写现实世界的东西很有帮助，比如网络服务器或任何你可能希望它“永远”运行的东西。

从本质上讲，您提出了语言的分歧，一方面，您拥有可以安全地证明事物的“经过验证的代码”，另一方面，您拥有可以永远循环的“不安全代码”。与 的比较你是对的IO。这与 Haskell 的副作用划分思想完全相同。

编辑：核心递归数据

您提到了 corecursive 数据，但这并不是您想要的。这个想法是，你确实会永远循环，但你会“高效地”这样做。本质上，对于递归，检查终止的最简单方法是始终使用严格小于当前项的项进行递归。

Fixpoint factorial n := match n with
  | 0 => 1
  | S n' => n * factorial n'

使用 corecursion，您的结果项必须比您的输入“更大”。

Cofixpoint stream := Cons 1 stream

这又不允许

 Cofixpoint stream := stream