∀ 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 中有描述。 .
关于coq - 形式化时间和空间复杂性要求，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/23220253/