在阿格達

啓用尾調用優化我使用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和*被定義爲與阿格達的內部自然數的定義相兼容。

當我評估(pow 2 100000)我得到一個堆棧溢出錯誤。但是，考慮到遞歸調用是尾部調用，我希望agda解釋器將pow'優化爲循環。

如何啓用此優化？

來源

2013-09-21 vlopez

我相當確信你不能;也許你可能想編譯代碼。 – Vitus

「自然數的內部定義」主要適用於編譯時，而不適用於評估者。如果你在C-C C-n中運行'pow 2 100000'，你會得到一個單一的自然，它比宇宙中的原子佔用更多的內存。如果你想要這樣的東西可用於證明和解釋，使用標準庫中的'Data.Bin'。 – copumpkin

'pow 2 10000'確實很好地工作，所以當使用C-c C-n時它可能也使用了內建定義。 Data.Bin看起來很有趣;雖然我也得到了堆棧溢出。編譯與MAlonzo可以解決這個問題，但我真的很喜歡以交互模式工作。 – vlopez

此優化在當前版本的Agda中未實現。替代方法包括增加堆棧的大小，或者將遞歸重寫爲指數中的對數，而不是線性的。

我也被告知：

有正在進行的工作，深入改變Agda.TypeChecking.Reduce 模塊（等等），它希望將有超過內置土黃上遞歸產生積極影響以及。

Ticket關於問題跟蹤器。

來源

2013-09-27 16:24:44 vlopez

隨着發展的進展，這個答案應該有望在將來更新。 – vlopez

回答

相關問題