Как рассуждать о космической сложности в Хаскеле - PullRequest
Новая
       55

Как рассуждать о космической сложности в Хаскеле

11 голосов
/ 05 апреля 2011

Я пытаюсь найти формальный способ думать о сложности пространства в 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 функция каким-то образом предотвращает разрушение узлов дерева, но я хотел бы знать точный механизм или хотя бы формальный механизм, который я мог бы использовать и в других случаях.

Спасибо за внимание.

1 Ответ

7 голосов
/ 05 апреля 2011

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

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

Или работа с Спецификация Coq станка STG .

...