13

私は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) ]

ツリーをトラバースする2つの関数。1つ（count1）は適切にストリーミングし、もう1つ（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 には標準的な操作セマンティクスがありません。そのようなセマンティクスは、プログラムの操作上の特性に関する推論を可能にし、実装が特定の空間と時間の動作を保証することを保証し、空間障害の原因を特定するのに役立つように提供されるべきであると主張します。コア Haskell プログラムの逐次評価のためのスモール ステップ決定論的セマンティクスを提示し、それが漸近的な空間と時間の使用の正確なモデルであることを示します。セマンティクスはグラフィック表記法を形式化したものであるため、有用なメンタル モデルと正確な数学的表記法を提供します。教育、プログラミング、および実装への影響について説明します。基本的なセマンティクスは、実装の制御下にあるすべてのスペースが含まれるように、モナディック IO メカニズムで拡張されています。

または、STG マシンの Coq 仕様から作業します。

于 2011-04-05T15:37:02.623 に答える