Agda 中递归函数调用的终止检查

Question

Agda 中递归函数调用的终止检查

3

以下Haskell代码是完全没有问题的：

dh :: Int -> Int -> (Int, Int)
dh d q = (2^d, q^d)
a = dh 2 (fst b)
b = dh 3 (fst a)

在Agda中类似的代码无法编译（终止检查失败）：

infixl 9 _^_
_^_ : ℕ → ℕ → ℕ
x ^ zero = 1
x ^ suc n = x * (x ^ n)

dh : ℕ -> ℕ -> ℕ × ℕ
dh d q = 2 ^ d , q ^ d

mutual
  a = dh 2 (proj₁ b)
  b = dh 3 (proj₁ a)

变量 a 的定义中使用了结构大小相同的 a，因此出现了循环。似乎终止检查器不会查看 dh 的定义。

我尝试使用协同归纳，设置选项 --termination-depth=4 —— 没有帮助。在 mutual 块内插入 {-# NO_TERMINATION_CHECK #-} 可以解决问题，但这看起来像是作弊。

有没有一种干净的方法让 Agda 编译代码？Agda 的终止检查器是否有一些根本性的限制？

- Vlad Semenov

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Steve Trout · Accepted Answer

Agda不像Haskell一样假设惰性求值。相反，Agda要求所有表达式都是强规范化的。这意味着无论您以何种顺序评估子表达式，都应该得到相同的答案。您提供的定义不是强规范化的，因为存在一种不终止的评估顺序：

a
-->
dh 2 (proj₁ b)
-->
dh 2 (proj₁ (dh 3 (proj₁ a))
-->
dh 2 (proj₁ (dh 3 (proj₁ (dh 2 (proj₁ b)))))

特别是，Agda的JavaScript后端会生成对于a和b不终止的代码，因为JavaScript是严格求值的。 Agda的终止检查器检查强规范化程序的子集：只有具有结构递归的程序。它查看在函数定义中匹配的构造函数模式的数量和顺序，以确定递归调用是否使用“较小”的参数。 a和b没有任何参数，因此终止检查器将从a到a（通过b）的嵌套调用视为与a本身相同的“大小”。