Почему рекурсивный `пусть` делает пространство эффективным?

Я нашел это утверждение, изучая функционально-реактивное программирование из "Заглушения космической утечки стрелой" Хай Лю и Пола Худака (стр. 5):

Suppose we wish to define a function that repeats its argument indefinitely:

    repeat x = x : repeat x

or, in lambdas:

    repeat = λx → x : repeat x

This requires O(n) space. But we can achieve O(1) space by writing instead:

    repeat = λx → let xs = x : xs
                  in xs

Разница здесь кажется небольшой, но она очень сильно влияет на эффективность использования пространства. Почему и как это происходит? Лучшее предположение, которое я сделал, это оценить их вручную:

    r = \x -> x: r x
    r 3

    -> 3: r 3 
    -> 3: 3: 3: ........
    -> [3,3,3,......]

Как и выше, для этих рекурсий нам нужно будет создать бесконечные новые выпады. Затем я пытаюсь оценить второй:

    r = \x -> let xs = x:xs in xs
    r 3

    -> let xs = 3:xs in xs
    -> xs, according to the definition above: 
    -> 3:xs, where xs = 3:xs
    -> 3:xs:xs, where xs = 3:xs

Во второй форме xs появляется и может быть разделен между всеми местами, где это происходит, поэтому я думаю, поэтому мы можем требовать только O(1) пространства, а не O(n), Но я не уверен, прав я или нет.

Кстати: ключевое слово "общий доступ" происходит со страницы 4 той же статьи:

Проблема в том, что стандартные правила оценки по требованию не могут распознать, что функция:

f = λdt → integralC (1 + dt) (f dt) 

такой же как:

f = λdt → let x = integralC (1 + dt) x in x

Первое определение приводит к повторению работы при рекурсивном вызове f, тогда как во втором случае вычисление является общим.

3 ответа

Решение

Проще всего разобраться с картинками:

  • Первая версия

    repeat x = x : repeat x
    

    создает цепочку (:) конструкторы, оканчивающиеся на thunk, который заменит себя на большее количество конструкторов по мере их необходимости. Таким образом, O(n) пространство.

    цепь

  • Вторая версия

    repeat x = let xs = x : xs in xs
    

    использования let "завязать узел", создав единый (:) конструктор, который ссылается на себя.

    цикл

Проще говоря, переменные являются общими, а функции приложений - нет. В

repeat x = x : repeat x

это совпадение (с точки зрения языка), что (со) рекурсивный вызов повторения с тем же аргументом. Таким образом, без дополнительной оптимизации (которая называется статическим преобразованием аргумента), функция будет вызываться снова и снова.

Но когда ты пишешь

repeat x = let xs = x : xs in xs

нет рекурсивных вызовов функций. Вы берете xи построить циклическое значение xs используй это. Все обмены явными.

Если вы хотите понять это более формально, вам необходимо ознакомиться с семантикой отложенной оценки, такой как "Естественная семантика для отложенной оценки".

Ваша интуиция о xs быть разделенным правильно Чтобы переформулировать авторский пример в терминах повторения, а не интеграла, когда вы пишете:

repeat x = x : repeat x

язык не признает, что repeat x справа совпадает со значением, полученным выражением x : repeat x, Тогда как если вы напишите

repeat x = let xs = x : xs in xs

вы явно создаете структуру, которая при оценке выглядит следующим образом:

{hd: x, tl:|}
^          |
 \________/
Другие вопросы по тегам