∀ a b ∈ ℕ, b ≠ 0 → ∃ ! q r ∈ ℕ, a = q × b + r ∧ r < b是使用依赖类型的标准示例。如何扩展这种类型，使其也表达时间和空间复杂性要求？

最佳答案

Nils Anders Danielsson 在 Agda 中使用 monad 来跟踪时间复杂度:与正在研究的复杂性“相关”的子计算通过使它们中的每一个花费“一个时间刻度”来明确标记为此类。这些子计算然后通过跟踪单子(monad)类型索引中的刻度总和来单子(monad)组合。

详细信息在他的论文 Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures 中有描述。 .

https://stackoverflow.com/questions/23220253/