Подтвердить что ты не робот

Как рассуждать о сложности пространства в Haskell

Я пытаюсь найти формальный способ думать о сложности пространства в 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?

Я понимаю интеллектуальные указатели на других языках, поэтому я смутно понимаю, что дополнительный параметр r в функции count2 как-то удерживает узлы дерева от разрушения, но я хотел бы знать точный механизм или по крайней мере, формальный, который я мог бы использовать и в других случаях.

Спасибо, что посмотрели.

4b9b3361

Ответ 1

Вы можете использовать семантику пространства Адама Баквелла,

В настоящее время в Haskell отсутствует стандартная операционная семантика. Мы утверждаем, что такая семантика должна предоставляться для обоснования эксплуатационных свойств программ, чтобы гарантировать, что реализации гарантируют определенное пространственное и временное поведение и помогают определить источник космических ошибок. Мы представляем малоэтажную детерминированную семантику для последовательной оценки программ Core Haskell и показываем, что она является точной моделью асимптотического пространства и использования времени. Семантика - это формализация графической нотации, поэтому она дает полезную ментальную модель, а также точную математическую нотацию. Мы обсуждаем его последствия для образования, программирования и реализации. Основная семантика расширена с помощью монадического механизма ввода-вывода, так что все пространство под управлением реализации включено.

Или работайте из спецификации Coq машины STG.