coq - 形式化时间和空间复杂性要求

Question

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

Answer 1

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

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