在Agda中启用尾叫优化

Question

我在agda-mode中使用Emacs，并编写了以下函数：

pow : Nat → Nat → Nat
pow m n = pow' 1 m n
          where
            pow' : Nat → Nat → Nat → Nat
            pow' acc _ zero = acc
            pow' acc m (succ n) = pow' (m * acc) m n

Nat、succ和*被定义为与Agda关于自然数的内部定义相兼容。

在计算(pow 2 100000)时，会得到堆栈溢出错误。但是，考虑到递归调用是尾调用，我希望agda解释器将pow'优化为一个循环。

如何启用此优化？

Answer 1

这种优化没有在目前版本的Agda中实现。替代方法包括增加堆栈的大小，或将递归改写为指数中的对数，而不是线性。

我还被告知：

正在进行的工作是深入改变Agda.TypeChecking.Reduce模块(除其他外)，希望这将对对内置自然的递归产生积极的影响。

关于问题跟踪器的票证。