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

Question

我正在尝试找到一种正式方式来思考 haskell 中的空间复杂性。我找到了this article关于图缩减(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 currently lacks a standard operational semantics. We argue that such a semantics should be provided to enable reasoning about operational properties of programs, to ensure that implementations guarantee certain space and time behaviour and to help determine the source of space faults. We present a small-step deterministic semantics for the sequential evaluation of Core Haskell programs and show that it is an accurate model of asymptotic space and time usage. The semantics is a formalisation of a graphical notation so it provides a useful mental model as well as a precise mathematical notation. We discuss its implications for education, programming and implementation. The basic semantics is extended with a monadic IO mechanism so that all the space under the control of an implementation is included.

或者从 the Coq specification of the STG machine 开始工作.