recursion - agda 中递归函数调用的终止检查

Question

下面的代码在 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.

我试过使用 coduction，设置选项--termination-depth=4- 没有帮助。{-# NO_TERMINATION_CHECK #-}在块内插入会有所mutual帮助，但它看起来像作弊。

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

Answer 1

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 后端会生成不会因aand终止的代码b，因为 JavaScript 是经过严格评估的。

Agda 的终止检查器检查强规范化程序的子集：那些只有结构递归的程序。它查看函数定义中与模式匹配的构造函数的数量和顺序，以确定递归调用是否使用“较小”的参数。a并且b没有任何参数，因此终止检查器会将来自ato a(via b) 的嵌套调用视为与其自身相同的“大小” a。