13

我试图找到一种正式的方式来考虑haskell中的空间复杂性。我发现这篇关于 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参数以某种方式防止树的节点被破坏,但我想知道确切的机制,或者至少是我可以使用的正式机制其他情况也是如此。

感谢您的关注。

4

1 回答 1

7

你可以使用 Adam Bakewell 的空间语义,

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

或者从STG 机器的 Coq 规范工作。

于 2011-04-05T15:37:02.623 回答