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

Question

我试图找到一种正式方式来思考 haskell 中的空间复杂性。我发现这篇文章关于图缩减（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 机制进行扩展，以便包含实现控制下的所有空间。

或者根据STG 机器的 Coq 规范进行工作。