如何在 Haskell 中推理空间复杂度

Question

我正在尝试找到一种正式的方式来考虑 haskell 中的空间复杂性。我发现this article 是关于 Graph Reduction (GR) 技术的，这在我看来是一种可行的方法。但我在某些情况下应用它时遇到问题。考虑以下示例：

假设我们有一棵二叉树：

data Tree = Node [Tree] | Leaf [Int]

makeTree :: Int -> Tree
makeTree 0 = Leaf [0..99]
makeTree n = Node [ makeTree (n - 1)
                  , makeTree (n - 1) ]

还有两个遍历树的函数，一个 (count1) 可以很好地流式传输，另一个 (count2) 可以一次在内存中创建整个树；根据分析器。

count1 :: Tree -> Int
count1 (Node xs) = 1 + sum (map count1 xs)
count1 (Leaf xs) = length xs

-- The r parameter should point to the root node to act as a retainer.
count2 :: Tree -> Tree -> Int
count2 r (Node xs) = 1 + sum (map (count2 r) xs)
count2 r (Leaf xs) = length xs

我想我理解它在 count1 的情况下是如何工作的，以下是我认为在图形缩减方面发生的情况：

count1 $ makeTree 2
=> 1 + sum $ map count1 xs
=> 1 + sum $ count1 x1 : map count1 xs
=> 1 + count1 x1                                + (sum $ map count1 xs)
=> 1 + (1 + sum $ map count1 x1)                + (sum $ map count1 xs)
=> 1 + (1 + sum $ (count1 x11) : map count1 x1) + (sum $ map count1 xs)
=> 1 + (1 + count1 x11 + sum $ map count1 x1)   + (sum $ map count1 xs)
=> 1 + (1 + count1 x11 + sum $ map count1 x1)   + (sum $ map count1 xs)
=> 1 + (1 + 100 + sum $ map count1 x1)          + (sum $ map count1 xs)
=> 1 + (1 + 100 + count x12)                    + (sum $ map count1 xs)
=> 1 + (1 + 100 + 100)                          + (sum $ map count1 xs)
=> 202                                          + (sum $ map count1 xs)
=> ...

我认为从序列中可以清楚地看出它在恒定空间中运行，但是在 count2 的情况下会发生什么变化？

我了解其他语言的智能指针，所以我隐约明白 count2 函数中的额外 r 参数不知何故 可以防止树的节点被破坏了，但我想知道确切的机制，或者至少是一种我可以在其他情况下使用的正式机制。

感谢收看。

Answer 1

您可以使用 Adam Bakewell 的空间语义，

• A Space Semantics for Core Haskell，2000 年。

Haskell 目前缺乏标准的操作语义。我们认为应该提供这样的语义来支持对程序的操作属性进行推理，以确保实现保证某些空间和时间行为，并帮助确定空间故障的来源。我们为 Core Haskell 程序的顺序评估提出了一个小步确定性语义，并表明它是渐近空间和时间使用的准确模型。语义是图形符号的形式化，因此它提供了有用的心理模型以及精确的数学符号。我们讨论了它对教育、规划和实施的影响。基本语义通过一元 IO 机制进行了扩展，以便包含实现控制下的所有空间。

或者在the Coq specification of the STG machine工作。