我将Emacs与结合使用agda-mode，并编写了此功能：
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'成循环。
如何启用此优化？
当前版本的Agda中未实现此优化。替代方法包括增加堆栈的大小，或将递归重写为指数的对数，而不是线性的。
我也被告知：
正在进行深入的工作以深深地更改Agda.TypeChecking.Reduce模块（以及其他模块），希望该模块也将对内置自然函数的递归产生积极影响。
问题跟踪器上的票证。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句