Навеяно темой Решение Problem K на Эрланг: дизайн

Автор: Gaperton
Дата: 06.11.07

В хаскелле вычисления ленивые, поэтому мемоизация делается сравнительно просто.
Например,

f 0 = .....
f n = .....(f k)....(f l)....(f m)..... -- где k,l,m < n

-- превращаем в бесконечный список заготовок
memo = [ f' n | n <- [0..] ]
f n = memo !! n
-- можно и другие структуры, с более эффективным доступом
-- например, кучу - т.е. список массивов экспоненциально возрастающей длины

f' 0 = .....
f' n = .....(f k)....(f l)....(f m).....

Если f n для какого-то n зацикливается, то, естественно, мы получим зависание — что в исходной формуле, что с мемоизацией.

Допустим, мы хотим как-то диагностировать зацикливание — чтобы получать не _|_, а какой-то определённый результат, например, банальное None.

Если бы memo было изменяемым — то нет ничего проще. Каждая ячейка принимает одно из трёх значений: ( ещё-не-вычисляли, начали-вычислять, результат ).
Обращение к ячейке со значением начали-вычислять — это и есть признак цикла.

Но в суровой реальности у нас выбор лишь между ещё-не-вычисляли и результатом.
Что делать?

Понятно, что есть решение: протащить в функцию список всех вызовов, и на каждом шаге проверять.

f 0 _ = return .....
f n ns =
    do
        let False = n `elem` ns -- в случае нестыковки стремительно выйдем
        let ns' = n:ns
        fk <- f k ns'
        fl <- f l ns'
        fm <- f m ns'
        return .....fk.....fl.....fm.....

А можно ли сделать то же самое, не занимаясь трассировкой вручную?

Здравствуйте, Кодт, Вы писали:

К>Допустим, мы хотим как-то диагностировать зацикливание — чтобы получать не _|_, а какой-то определённый результат, например, банальное None.

К>А можно ли сделать то же самое, не занимаясь трассировкой вручную?

топологическая сортировка, порверка ацикличности графа

Здравствуйте, BulatZiganshin, Вы писали:

К>>А можно ли сделать то же самое, не занимаясь трассировкой вручную?
BZ>топологическая сортировка, порверка ацикличности графа

Это в тех случаях, когда граф зависимостей легко построить.
А если просто дана рекурсивная формула — например, знаменитая проблема 3x+1 — тогда как?
Сам процесс построения графа даст ответ, зацикливается он или нет. До сортировки не дойдёт

Здравствуйте, Кодт, Вы писали:

BZ>>топологическая сортировка, порверка ацикличности графа

К>Это в тех случаях, когда граф зависимостей легко построить.
К>А если просто дана рекурсивная формула — например, знаменитая проблема 3x+1 — тогда как?
К>Сам процесс построения графа даст ответ, зацикливается он или нет. До сортировки не дойдёт

может, я чего-то не понимаю, но для excel это строится легко — если в формуле для ячейки a1 упоминаются a2 и a3, то в графе должны быть направленные vertices от a1 к a2 и a3

Здравствуйте, BulatZiganshin, Вы писали:

К>>Это в тех случаях, когда граф зависимостей легко построить.
К>>А если просто дана рекурсивная формула — например, знаменитая проблема 3x+1 — тогда как?
К>>Сам процесс построения графа даст ответ, зацикливается он или нет. До сортировки не дойдёт

BZ>может, я чего-то не понимаю, но для excel это строится легко — если в формуле для ячейки a1 упоминаются a2 и a3, то в графе должны быть направленные vertices от a1 к a2 и a3

А если во всех формулах написано =problem3x1(k) где k — номер текущей ячейки?
Забудь про эксель. Есть рекурсивная функция. Всё.
Неограниченную мемоизацию как строить — я уже показал, на ленивых списках или аналогичных им структурах.

Здравствуйте, Кодт, Вы писали:

К>А если во всех формулах написано =problem3x1(k) где k — номер текущей ячейки?
К>Забудь про эксель. Есть рекурсивная функция. Всё.

тогда это проблема останова тьюринговской машины, которая не имеет универсального решения

Здравствуйте, Кодт, Вы писали:

К>Если бы memo было изменяемым — то нет ничего проще. Каждая ячейка принимает одно из трёх значений: ( ещё-не-вычисляли, начали-вычислять, результат ).
К>Обращение к ячейке со значением начали-вычислять — это и есть признак цикла.

я говорил о решении этой проблемы. а ты похоже две вещи смешиваешь

Здравствуйте, BulatZiganshin, Вы писали:

BZ>тогда это проблема останова тьюринговской машины, которая не имеет универсального решения

Э... согласен.
Но у вычислителя могут быть средства диагностики возможного зацикливания: когда глубина рекурсии достигает пороговой величины, или когда аргумент убегает очень далеко.

С учётом этих ограничений, можно считать, что рекурсивная формула описывает некоторый конечный орграф.
Кстати, конечный ли? Если есть лишь ограничение на глубину рекурсии, то, подсовывая каждый раз новые аргументы из универсума, мы получим неограниченное множество графов либо граф с неограниченным количеством вершин.

Просто — что дешевле, диагностировать зацикливание по ходу вычислений, или построить граф, провести его анализ и только после этого выполнить вычисления в полном объёме?

Конечно же, в любом случае исходную функцию нужно преобразовывать.
Для трассировки вызовов — вплести туда Maybe (для результата) и State (для аргументов)
Для работы с графами — сделать версии, конструирующие граф и выполняющие собственно вычисления.

Здравствуйте, Кодт, Вы писали:

К>В хаскелле вычисления ленивые, поэтому мемоизация делается сравнительно просто.
К>Например,
К>[code]
К>f 0 = .....
К>f n = .....(f k)....(f l)....(f m)..... -- где k,l,m < n

А как при таком условии вообще что-то может зациклиться?
Или это условие верно не для всех n>0?

Здравствуйте, Кодт, Вы писали:

К>Просто — что дешевле, диагностировать зацикливание по ходу вычислений, или построить граф, провести его анализ и только после этого выполнить вычисления в полном объёме?

дешевле сделать поддержку ^Break

пойми, ты сейчас решаешь задачу анализа завершаемости обычной программы. почему таких средств нет в компиляторах? потому, что простые случаи, с которыми они смогут справиться, неинтересны

Кодт wrote:

> Э... согласен.
> Но у вычислителя могут быть средства диагностики *возможного*
> зацикливания: когда глубина рекурсии достигает пороговой величины, или
> когда аргумент убегает очень далеко.
C глубиной тоже мало что получится, ведь рекурсия ещё и широкой может быть. Скажем, тупой алгоритм чисел Фибоначчи при n=100 требует глубины всего лишь в 100, аргумент не слишком "страшный", зато требует 10^30 операций.

Здравствуйте, Кодт, Вы писали:

К>Просто — что дешевле, диагностировать зацикливание по ходу вычислений, или построить граф, провести его анализ и только после этого выполнить вычисления в полном объёме?

Возьмём f n = ... (f k) ... (f l) ... (f m) ...
Если l зависит от (f k) или m от (f k) или (f l), то разделить построение графа и вычисление функции нельзя.
Так что в таком случае только рантайм проверка или математическое доказательство.

Здравствуйте, Кодт, Вы писали:

К>Но в суровой реальности у нас выбор лишь между ещё-не-вычисляли и результатом.
К>Что делать?

К>Понятно, что есть решение: протащить в функцию список всех вызовов, и на каждом шаге проверять.
К>А можно ли сделать то же самое, не занимаясь трассировкой вручную?

Здесь можно применить continuation-composing style.
Если рекурсивные вызовы заменить на запросы, выполняемые внешним кодом, то проверку зацикленности можно вынести наружу.

data Result = Done Int | GetValue Int (Int -> Result)

f :: Int -> Result
f 0 = Done 1
f 1 = Done 1
f n
    | n /= 10  = GetValue (n-1) $ \v1 ->
                 GetValue (n-2) $ \v2 -> Done (v1+v2)
    | n==10    = GetValue n $ \v -> Done v

compute :: Int -> Maybe Int
compute n = compute' n []

compute' n active | n `elem` active = Nothing
compute' n active = loop (f n)
    where loop (Done v) = Just v
          loop (GetValue x k) = maybe Nothing (loop . k) (compute' x (n:active))

Чтобы код функции f смотрелся не так громоздко, можно использовать настоящие delimited continuations.

Здравствуйте, palm mute, Вы писали:

PM>Чтобы код функции f смотрелся не так громоздко, можно использовать настоящие delimited continuations.
Вот как это может выглядеть в языке с поддержкой delimited continuations. Вместо рекурсивных вызовов будем использовать функцию recurse, вместо явного обращения к функции f, которая может зациклиться, будем использовать (compute f x).
Сначала пара тестов:

(define (f1 x)
  (cond ((= x 3) (recurse 4))
        ((= x 4) (recurse 3))
        (else (* x 10))))

(define (almost-fib x)
  (cond ((= x 0) 1)
        ((= x 1) 1)
        ;; here's the loop
        ((= x 2) (recurse 3))
        ((= x 3) (recurse 4))
        ((= x 4) (recurse 2))
        ;; break the loop
        ((= x 5) 5)
        ((= x 6) 8)
        (else (+ (recurse (- x 1)) (recurse (- x 2))))))

Проверим, как это дело работает:

> (compute almost-fib 1)
1
> (compute almost-fib 2)
#f
> (compute almost-fib 5)
5
> (compute almost-fib 10)
55
> (compute f1 3)
#f
> (compute f1 4)
#f
> (compute f1 1)
10
> (compute f1 2)
20

Реализация (работает в последней версии MzScheme):

(require (lib "control.ss"))

(define-struct req-done [val])
(define-struct req-recurse [x k])

(define (recurse x)
  (shift k (make-req-recurse x k)))

(define (compute1 f x active)
  (define (loop req)
    (cond ((req-done? req) (req-done-val req))
          (else (let ((result (compute1 f (req-recurse-x req) (cons x active))))
                  (if result
                      (loop ((req-recurse-k req) result))
                      #f)))))
  (if (member x active)
      #f
      (loop (reset (make-req-done (f x))))))

(define (compute f x) (compute1 f x '()))

Здравствуйте, red75, Вы писали:

К>>Просто — что дешевле, диагностировать зацикливание по ходу вычислений, или построить граф, провести его анализ и только после этого выполнить вычисления в полном объёме?

R>Возьмём f n = ... (f k) ... (f l) ... (f m) ...
R>Если l зависит от (f k) или m от (f k) или (f l), то разделить построение графа и вычисление функции нельзя.
R>Так что в таком случае только рантайм проверка или математическое доказательство.

Вот поэтому я и спрашиваю: как в рантайме можно это проверить.
Есть решение с мутабельным кэшем.
Есть решение с трассировкой, не зависящее от кэша (хотя, конечно, кэш всегда пригодится).
Ещё варианты? Можно ли каким-то волшебным способом прикрутить сюда иммутабельный ленивый кэш?

Кстати говоря, ленивость внутри всё равно реализуется через мутабельность. Объект меняет своё состояние с невычисленного на вычисленное. Так что рантайм мог бы и промежуточное состояние ввести, попытка вычисления которого приводила бы к error. Ибо, какая разница, как получить _|_ — бесконечным висением, исчерпанием стека или сообщением о вылете?
Конечно, все виды зацикливания этим не покроешь, но некоторые покрыть можно.

Здравствуйте, Кодт, Вы писали:

R>>Так что в таком случае только рантайм проверка или математическое доказательство.

К>Вот поэтому я и спрашиваю: как в рантайме можно это проверить.
К>Есть решение с мутабельным кэшем.
К>Есть решение с трассировкой, не зависящее от кэша (хотя, конечно, кэш всегда пригодится).
К>Ещё варианты? Можно ли каким-то волшебным способом прикрутить сюда иммутабельный ленивый кэш?

Ну ещё можно протаскивать состояние вычисления внутри параметра функции. Но это тоже громоздко.

NewType NoCyc a=NC a [a]
instance Eq NoCyc where
(NC a _) == (NC b _) = a==b 
...
instance Ord NoCyc where
...
instance ... -- в общем все нужные классы

f (NC num _) = memo !! num

f' (NC num ns) = not (num `elem` ns) | ... f(l) ... where l=n/2 ... where n=(NC num num:ns)
                 true | error "cycle"

А волшебным способом никак. f n зависит только от n.


К>Кстати говоря, ленивость внутри всё равно реализуется через мутабельность. Объект меняет своё состояние с невычисленного на вычисленное. Так что рантайм мог бы и промежуточное состояние ввести, попытка вычисления которого приводила бы к error. Ибо, какая разница, как получить _|_ — бесконечным висением, исчерпанием стека или сообщением о вылете?
К>Конечно, все виды зацикливания этим не покроешь, но некоторые покрыть можно.

Ну не факт, что каждый вызов функции с одинаковым аргументом возвращает "указатель" на один и тот-же объект. Это предполагает внутреннюю мемоизацию.

Здравствуйте, red75, Вы писали:

R>Ну ещё можно протаскивать состояние вычисления внутри параметра функции. Но это тоже громоздко.
Собственно, это и есть трассировка.

R>NewType NoCyc a=NC a [a]
R>instance Eq NoCyc where
R>(NC a _) == (NC b _) = a==b 
R>...
R>instance Ord NoCyc where
R>...
R>instance ... -- в общем все нужные классы

R>f (NC num _) = memo !! num

R>f' (NC num ns) = not (num `elem` ns) | ... f(l) ... where l=n/2 ... where n=(NC num num:ns)
R>                 true | error "cycle"

Этот код — почти то же самое, что у меня с монадами. Только у тебя конкретная монада Id использована: return=id, fail=error

К>>Кстати говоря, ленивость внутри всё равно реализуется через мутабельность. Объект меняет своё состояние с невычисленного на вычисленное. Так что рантайм мог бы и промежуточное состояние ввести, попытка вычисления которого приводила бы к error. Ибо, какая разница, как получить _|_ — бесконечным висением, исчерпанием стека или сообщением о вылете?
К>>Конечно, все виды зацикливания этим не покроешь, но некоторые покрыть можно.

R>Ну не факт, что каждый вызов функции с одинаковым аргументом возвращает "указатель" на один и тот-же объект. Это предполагает внутреннюю мемоизацию.

Однако, каждый вызов доступа к одному и тому же элементу одной и той же структуры — хоть и не гарантирует равенство адресов, но было бы очень странно, если бы это было не так.
Это может быть несправедливо для GADT, где конструкторы и акцессоры — "настоящие" функции (устроенные внутри как бог на душу положит). Но для обычных типов-то...

Здравствуйте, Кодт, Вы писали:

К>Этот код — почти то же самое, что у меня с монадами. Только у тебя конкретная монада Id использована: return=id, fail=error

Это я привёл для случая когда требуется минимальная модификация кода и функциональная частота. А что ты хочешь получить в итоге? Эффективность по скорости? По памяти? Функциональную чистоту? Универсальность? Легкость сопровождения?

R>>Ну не факт, что каждый вызов функции с одинаковым аргументом возвращает "указатель" на один и тот-же объект. Это предполагает внутреннюю мемоизацию.

К>Однако, каждый вызов доступа к одному и тому же элементу одной и той же структуры — хоть и не гарантирует равенство адресов, но было бы очень странно, если бы это было не так.
К>Это может быть несправедливо для GADT, где конструкторы и акцессоры — "настоящие" функции (устроенные внутри как бог на душу положит). Но для обычных типов-то...

Ммм... пожалуй, да. Не вижу причин по которым это невозможно. Разве что memo представлено как функция. Надо исходники компилятора смотреть. Или авторов спрашивать.

Здравствуйте, Кодт, Вы писали:

К>Это может быть несправедливо для GADT, где конструкторы и акцессоры — "настоящие" функции (устроенные внутри как бог на душу положит). Но для обычных типов-то...

А что с GADT не так?

Здравствуйте, lomeo, Вы писали:

К>>Это может быть несправедливо для GADT, где конструкторы и акцессоры — "настоящие" функции (устроенные внутри как бог на душу положит). Но для обычных типов-то...
L>А что с GADT не так?

data Foo where S :: String -> Foo
s :: Foo -> String

hello = S "hello"
h1 = s hello
h2 = s hello

Можешь дать гарантии, что h1 и h2 отсылаются к одном и тому же конструктору ( : ), а не к двум эквивалентным?
Ведь, например, функции могут быть реализованы так

encode :: String -> ByteString
decode :: ByteString -> String
-- мы-то знаем, что (decode.encode)==id, но знает ли компилятор?

data Foo = S' ByteString
makeFoo str = S' $ encode str
takeStr foo@(S' str) = decode str

hello = makeFoo "hello" -- единственный экземпляр, тут вариантов нет
h1 = takeStr hello
h2 = takeStr hello -- без внутренней мемоизации получим копию, а не ту же строку