以下代码在 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
block 中插入 {-# NO_TERMINATION_CHECK #-}
会有所帮助,但它看起来像是作弊。
是否有一种干净的方法让 Agda 编译代码? Agda 的终止检查器是否有一些基本限制?
最佳答案
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's termination checker检查强规范化程序的子集:那些只有结构递归的程序。它查看函数定义中模式匹配的构造函数的数量和顺序,以确定递归调用是否使用“较小”参数。 a
和 b
没有任何参数,因此终止检查器会看到从 a
到 a
的嵌套调用(通过 b
)与 a
本身具有相同的“大小”。
关于recursion - agda 中递归函数调用的终止检查,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/30688558/