Что такое рекурсия
Это дом, который построил Джек.
Рекурсия — важный элемент в математике и программировании. С её помощью можно упаковывать большие и сложные конструкции в маленькие и простые, а потом разворачивать обратно, когда нужно. Давайте выясним, как она устроена.
Дом, который построил Джек
Чтобы было понятнее, что такое рекурсия, возьмём стихотворение Самуила Маршака «Дом, который построил Джек»:
Вот дом,
Который построил Джек.
А это пшеница,
Которая в тёмном чулане хранится
В доме,
Который построил Джек.
А это весёлая птица-синица,
Которая часто ворует пшеницу,
Которая в тёмном чулане хранится
В доме,
Который построил Джек.
Вот кот,
Который пугает и ловит синицу,
Которая часто ворует пшеницу,
Которая в тёмном чулане хранится
В доме,
Который построил Джек.
Вот пёс без хвоста,
Который за шиворот треплет кота,
Который пугает и ловит синицу,
Которая часто ворует пшеницу,
Которая в тёмном чулане хранится
В доме,
Который построил Джек. …
Смотрите, что в нём интересного: каждая часть стихотворения состоит из нового начала и точного повторения того, что уже было до этого. Сначала у нас был только дом, который построил Джек — это нулевой уровень рекурсии, или вложенности.
Вот дом,
Который построил Джек.
Обозначим его за [0] и дальше будем увеличивать это число для каждого уровня. Следите за уровнями.
А это пшеница,
Которая в тёмном чулане хранится [0]
Чтобы получить полноценное продолжение, нам нужно взять предыдущий уровень и подставить его сюда:
А это пшеница,
Которая в тёмном чулане хранится
В доме,
Который построил Джек.
А это весёлая птица-синица,
Которая часто ворует пшеницу,
[1]
Если мы будем разворачивать стих, то на первом проходе получим такое:
А это весёлая птица-синица,
Которая часто ворует пшеницу,
Которая в тёмном чулане хранится
[0]
А на втором у нас уже появится полноценный стих:
А это весёлая птица-синица,
Которая часто ворует пшеницу,
Которая в тёмном чулане хранится
В доме,
Который построил Джек.
👉 Общее правило такое: когда есть рекурсия, её последовательно разворачивают на каждом шаге, пока не дойдут до нулевого уровня. Как только дошли — всё готово, рекурсия сделала своё дело. До этого момента она вызывает сама себя с новыми параметрами.
Рекурсия в программировании
Допустим, нам нужно посчитать сумму всех чисел от 1 до какого-то числа. Можно это сделать в цикле, а можно сделать универсальную функцию с рекурсией. Ей будет достаточно указать на входе число, до которого нужно всё посчитать, а она сама сделает всё остальное.
Сначала запишем это на JavaScript, а потом разберёмся с тем, как работает эта магия:
Затем мы организуем нулевой уровень — тот, где рекурсия начинается: if (x == 1)
А дальше идёт самое интересное — если мы не дошли до единицы, то мы берём значение x и складываем его с результатом этой же функции, но от предыдущего значения. Если мы, например, считаем rec(10), то эта команда сделает так:
Попробуйте сами вставить код в консоль и посмотрите на результат.
Особенности рекурсии
Так как рекурсия — это программа, которая вызывает саму себя, то при неправильном подходе рекурсия может использовать очень много памяти и машинных ресурсов. Чем глубже уровень рекурсии — тем больше ресурсов ей нужно.
Иногда программист увлекается рекурсией и забывает прописать выход из неё. В результате рекурсия бесконечно углубляется саму в себя, забирает в себя все ресурсы и программа падает. Говорят, что так образуются чёрные дыры, в которых всё исчезает.
Бывают моменты, когда рекурсия — это единственный способ выполнить нужную задачу. Например, при парсинге HTML-кода или для построения дерева зависимостей.
Что дальше
Теперь, когда мы достаточно знаем про рекурсию, то сможем сделать интересный новый проект. Например, чтобы наша программа сама решала судоку любой степени сложности или рисовала классные лабиринты.
Рекурсия. Беглый взгляд
Ниже речь пойдёт о старушке рекурсии, которую неплохо бы представлять, понимать и применять.
Примечание: Данная небольшая статья написана для беглого ознакомления с рекурсией, некоторыми примерами её применения и опасностями.
Определение
Для начала стоит сказать, что рекурсия относится не только к программированию. Рекурсия — это общее понятие, которое может быть присуще чему угодно и встречаться в повседневной жизни, но больше всего она распространена в информатике и математике. Для программистов же умение применять рекурсию — большой плюс в коллекцию полезных навыков.
Самая большая глупость — это делать то же самое и надеяться на другой результат.
Под рекурсией понимают процесс повторения элементов самоподобным образом. Объект обладает рекурсией, если он является частью самого себя.
Частным случаем рекурсии является хвостовая рекурсия. Если любой рекурсивный вызов является последней операцией перед возвратом из функции, то это оно.
Некоторые примеры
Рекурсию надо бы понять, а определение для этого подходит хуже, чем наглядные примеры. Для лучшего понимания, конечно, всё же следует прочитать определение, посмотреть на пример, снова прочитать определение и снова посмотреть на пример… Повторять, пока не придёт осознание.
Отличный пример вы можете найти тут.
Самое известное программисту применение рекурсии — задачи на вычисление чисел Фибоначчи или факториала. Давайте покажем, как это реализовать на языке C:
Тут же стоит отметить, что декларативная парадигма, в частности парадигма логического программирования, намного лучше позволяет понять рекурсию, так как там это обычное дело.
Fork-бомба
Примечание: Рекурсивное создание процессов крайне быстро (из-за экспоненциального роста их количества) заполняет таблицу процессов, что достаточно опасно для системы.
Reboot кнопкой после такого делать немного не приятно.
Для математика первой ассоциацией, скорее всего, будет фрактал. Фракталы прекрасны и приятно для глаза показывают свойства самоподобия.
Самые известные фракталы:
Ну и в повседневной жизни классическим примером являются два зеркала, поставленных друг напротив друга.
Углубимся глубже
Проста ли рекурсия? Однозначно нет. На вид кажется, что всё просто, однако рекурсия таит в себе опасности (А иногда она просто не понятна).
Вернёмся к примеру с вычислением чисел Фибоначчи. Сразу заметим, что возвращаемым результатом функции является вызов этой же функции, а если быть точнее, то сумма результатов вызова двух функций (именно поэтому рекурсия не хвостовая). Становится понятно, что второй вызов не произойдёт, пока не завершится первый (в котором также будет вызов двух функций). Тут же пытливый ум заметит, что из рекурсивной функции должен существовать «нормальный» выход, без самовызова, иначе мы познакомимся с переполнением стека вызовов — это один из ключевых моментов, который стоит держать в голове при работе с функциями вызывающими сами себя.
Заметим, что дерево вызовов получится большим, но максимальное количество вызовов в стеке будет заметно меньше (N-1 при N > 2, соответственно).
Рекурсивные алгоритмы довольно-таки часто встречаются при работе с деревьями, сортировками и задачами на графах. Так что, чтобы лучше вникнуть нужна практика и для этого не плохо подходит вышеупомянутое (в частности, бинарные или общие деревья. Их реализация не так сложна, а опыт работы с рекурсией получится не плохой).
Помимо этого хотелось бы упомянуть Ханойские башни, которые также отлично подойдут для ознакомления с рекурсивными задачами. На Хабре также был отличный разбор этой игры.
Для полноты картины обязательно надо упомянуть о борьбе с рекурсией.
Повышается производительность. Но это не значит, что с ней просто необходимо бороться, ведь применение рекурсии очевиднее, проще и приятнее, чем итерационные варианты.
Под силу ли побороть любую рекурсию?
Однозначно да. Любой рекурсивный алгоритм можно переписать без использования рекурсии, а хвостовую рекурсию же очень легко перевести на итерацию (чем и занимаются некоторые компиляторы для оптимизации). Это также относится и к итерационным алгоритмам.
Самый известный способ — это использование стека. Здесь подробнее, для интересующихся.
Заключение
Спасибо за прочтение статьи. Надеюсь, что большинство не знакомых с рекурсией получили базовое представление о ней, а от знающих людей, конечно, хочется услышать дополнения и замечания в комментариях. Не бойтесь рекурсии и не переполняйте стек!
UPD: Добавлен корректный пример хвостовой рекурсии.
Функциональное программирование с точки зрения EcmaScript. Рекурсия и её виды
Сегодня мы продолжим наши изыскания на тему функционального программирования в разрезе EcmaScript, на спецификации которого основан JavaScript. В предыдущих статьях цикла были рассмотрены следующие темы:
Рекурсия
Реку́рсия — определение, описание, изображение какого-либо объекта или процесса внутри самого этого объекта или процесса, то есть ситуация, когда объект является частью самого себя. Термин «рекурсия» используется в различных специальных областях знаний — от лингвистики до логики, но наиболее применение находит в математике и информатике.
Применительно к программированию под рекурсией подразумевают процессы, которые вызывают сами себя в своём теле. Рекурсивная функция имеет несколько обязательных составляющих:
Выделим характерные составляющие рекурсивной функции. Терминальное условие
и правило движения по рекурсии
Важно осознавать, что рекурсия это не какая-то специфическая фича JS, а техника очень распространённая в программировании.
Рекурсивный и итеративный процессы
Рекурсию можно организовать двумя способами: через рекурсивный процесс или через итеративный.
Рекурсивный процесс мы с вами уже видели:
Итеративное решение задачи о факториале выглядело бы так:
Оба этих варианта это рекурсия. В обоих решениях есть характерные для рекурсии черты: терминальное условие и правило движения по рекурсии. Давайте разберём их отличия.
Рекурсивный процесс на каждом шаге запоминает действие. которое надо сделать. Дойдя до термального условия, он выполняет все запомненные действия в обратном порядке. Поясним на примере. Когда рекурсивный процесс считает факториал 6, то ему нужно запомнить 5 чисел чтобы посчитать их в самом конце, когда уже никуда не деться и рекурсивно двигаться вглубь больше нельзя. Когда мы находимся в очередном вызове функции, то где-то снаружи этого вызова в памяти хранятся эти запомненные числа.
Выглядит это примерно так:
Как видите, основная идея рекурсивного процесса — откладывание вычисления до конца.
Такой процесс порождает изменяемое во времени состояние, которое хранится «где-то» снаружи текущего вызова функции.
Думаю, вы помните, что в первой статье из цикла о Функциональном программировании мы говорили о важности имутабельности и отсутствия состояния. Наличие состояния порождает много проблем, с которыми не всегда легко справится.
Итеративный процесс отличается от рекурсивного фиксированным количеством состояний. На каждом своём шаге итеративный процесс считает всё, что может посчитать, поэтому каждый шаг рекурсии существует независимо от предыдущего.
Думаю, очевидно, что итеративный процесс потребляет меньше памяти. Следовательно, всегда при создании рекурсии следует использовать его. Единственное исключение: если мы не можем посчитать значение до достижения термального условия.
Древовидная рекурсия
Многие считают, что деревья и работа с ними это что-то очень заумное, сложное и не понятное простым смертным. На самом деле это не так. Любая иерархическая структура может быть представлена в виде дерева. Даже человеческое мышление подобно дереву.
Чтобы лучше понять древовидную рекурсию разберём простой и популярный пример — числа Фибоначчи.
Чи́сла Фибона́ччи — элементы числовой последовательности 0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181, 6765, 10946, 17711, … (последовательность A000045 в OEIS), в которой первые два числа равны либо 1 и 1, либо 0 и 1, а каждое последующее число равно сумме двух предыдущих чисел. Названы в честь средневекового математика Леонардо Пизанского (известного как Фибоначчи).
Математически довольно просто сформулировать описание (а ведь декларативное программирование и есть описание) данной последовательности:
Теперь давайте перейдём от математики к логическим рассуждениям(нам ведь нужно программную логику написать). Для вычисления fib(5) нам придётся вычислить fib(4) и fib(3). Для вычисления fib(4) нам придётся вычислить fib(3) и fib(2). Для вычисления fib(3) нам придётся вычислить fib(2) и так до тех пор пока мы не дойдём до известных значений (1) и (2) в нашей математической модели.
На какие мысли нас должны навести наши рассуждения? Очевидно, мы должны использовать рекурсию. Термальное условие можно сформулировать как n
Как учить рекурсию разработчикам программного обеспечения
Пришло время переосмыслить обучение рекурсии с помощью реальных кейсов вместо элегантных математических уравнений
Для программистов, особенно программистов-самоучек, первое знакомство с миром «рекурсии» в основном связано с математикой. При упоминании рекурсии программисты сразу вспоминают некоторые из наших любимых слов на F – нет, не те самые слова на F, а:
Фибоначчи
Факториал
Рекурсивные версии функций Фибоначчи и факториала – одни из самых красивых фрагментов кода, которые можно увидеть. Эти краткие фрагменты при выполнении работы полагаются лишь на самих себя. Они воплощают в себе определение рекурсии – функции, которая вызывает себя (вызов самой себя – это рекурсия). Меня совсем не удивляет тот факт, что функции Фибоначчи и факториалы инкапсулируют тему рекурсии наподобие разнообразных руководств, которые показывает пример работы кода на основе счётчиков или TODO-листов. Фибоначчи и факториалы настолько же тривиальны, как счётчики или TODO-листы.
Возможно, вы слышали выражение, что «все итерационные алгоритмы можно выразить рекурсивно». Другими словами, функция, использующая цикл, может быть переписана для использования самой себя. Теперь, если любой итерационный алгоритм может быть написан рекурсивно, то же самое должно быть верно и для обратного.
Примечание: итерационный алгоритм или функция – это алгоритм, который использует цикл для выполнения работы.
Давайте вернёмся к рекурсивной функции Фибоначчи и вместо этого запишем её как итеративную функцию Фибоначчи:
Давайте возьмём рекурсивную функцию факториала и напишем её как итеративную функцию:
Оба подхода приводят к одному и тому же выводу. Если вы возьмёте одинаковые входные данные, то функции дадут один и тот же результат. Даже путь, по которому они прошли, возможно, один и тот же. Единственное различие заключается в метафорическом способе транспортировки, используемом на пути к получению результата.
Итак, если мы можем писать рекурсивные функции итеративно, зачем нам вообще нужно беспокоиться о рекурсии и какая от этого польза в программировании?
Основная причина, по которой мы используем рекурсию, – упрощение алгоритма до терминов, легко понятных большинству людей. Здесь важно отметить, что цель рекурсии (или, скорее, преимущество от рекурсии) состоит в том, чтобы сделать наш код более понятным. Однако важно знать, что рекурсия не является механизмом, который используется для оптимизации кода – скорее всего, это может иметь неблагоприятное влияние на производительность по сравнению с эквивалентной функцией, написанной итеративно.
Краткий вывод из этого: рекурсивные функции повышают читаемость кода для разработчиков, а итерационные функции оптимизируют производительность кода.
Во многих статьях и руководствах по рекурсии, которые я читал раньше, разочаровывает то, что они склоняются к осторожности и зацикливаются только на разговоре о таких функциях, как рекурсивные Фибоначчи или факториалы. Их рекурсивное написание не даёт разработчикам никаких реальных преимуществ. Это всё равно, что рассказать шутку без каких-либо предпосылок к ней.
Если преобразовать рекурсивные функции в итерационные, мы также получаем довольно неплохой код. Пожалуй, он так же легко читаем, как и его рекурсивные эквиваленты. Конечно, он может не иметь такого же уровня элегантности, но если он всё ещё читаем, я собираюсь пойти дальше и отдать предпочтение оптимизации кода, чем наоборот.
Поэтому кажется правдоподобным, что многие люди, впервые изучающие рекурсию, с трудом могут увидеть реальную пользу от её использования. Может быть, они просто видят в этом некую чрезмерную абстракцию. Так чем же полезна рекурсия? Или, ещё лучше, как мы можем сделать изучение рекурсии полезным?
Полезную рекурсию можно найти, когда мы на самом деле пытаемся написать код, напоминающий сценарий из реальной жизни.
Я могу сказать, что почти ни один разработчик где бы то ни было (за исключением написания кода на собеседования) не собирался реализовывать рекурсивную функцию Фибоначчи или факториальную функцию для своей работы, и, если бы это было нужно, он мог бы просто погуглить, так как есть миллион статей, объясняющих это.
Однако существует очень мало статей, демонстрирующих, как рекурсию можно использовать в реальных кейсах. Нам нужно меньше статей наподобие «Введение в рекурсию» и больше статей о том, как рекурсия может быть полезна в решении задач, с которыми вы столкнётесь на работе.
Итак, теперь, когда мы подошли к этой теме, давайте представим следующий кейс: ваш босс прислал вам структуру данных, состоящую из разных отделов, каждый из которых содержит E-mail всех, кто работает в этом отделе. Однако отдел может состоять из подразделений: объектов и массивов разного уровня. Ваш босс хочет, чтобы вы написали функцию, которая сможет отправлять электронное письмо на каждый из этих адресов электронной почты.
Вот структура данных:
И как же с этим справиться?
Из того, что мы видим, подразделения записаны в объект, в то время как массивы используются для хранения адресов электронной почты. Поэтому можно попытаться написать какую-то итеративную функцию, которая проходит по каждому отделу и проверяет, является ли он отделом (объектом) или списком адресов электронной почты (массивом). Если это массив, мы можем перебрать массив и отправить электронное письмо на каждый адрес. Если это объект, можно создать ещё один цикл для работы с этим отделом, используя ту же тактику «проверить, является ли это объектом или массивом». Насколько мы можем видеть, наша структура данных не имеет больше двух подуровней. Так что еще одна итерация должна удовлетворить все уровни и сделать то, что мы хотим.
Наш окончательный код может выглядеть примерно так:
Я проверил вывод этого кода, может быть, я даже написал для него небольшой модульный тест. Этот код неразборчивый, но он работает. Учитывая количество вложенных циклов, можно утверждать, что он крайне неэффективен. А кто-то на заднем плане может кричать: «Big O? Больше похоже на Big OMG, верно?»
Конечно, есть и другие способы решения этой задачи, но то, что у нас есть на данный момент, работает. В любом случае, это всего лишь небольшая функция, и там не так много адресов электронной почты, и, вероятно, она не будет использоваться часто, так что это не имеет значения. Давайте вернёмся к работе над более важными проектами, прежде чем босс найдёт для меня еще одну побочную задачу!
Через пять минут ваш босс возвращается и говорит, что он также хочет, чтобы функция работала, даже если новые отделы, подразделения и адреса электронной почты будут добавлены в эту структуру данных. Это меняет ситуацию, потому что теперь мне нужно учитывать возможность наличия подподподразделений, подподподподразделений и так далее.
Внезапно итерационная функция больше не удовлетворяет критериям.
Но, о чудо, мы можем использовать рекурсию!
Итак, наконец-то у нас есть функция, которая использует рекурсию в более-менее реальном кейсе. Давайте разберёмся, как это всё работает.
Эта функция имеет два преимущества по сравнению с нашим предыдущим итеративным аналогом:
Она соответствует дополнительным критериям, установленным нашим начальником. Пока функция продолжает следовать тому же шаблону, она может обрабатывать любые новые объекты или массивы, добавленные к ней, без необходимости изменять ни одной строчки кода;
Код легко читаем. У нас нет набора вложенных циклов, которые наш мозг должен попытаться отслеживать.
Также можно заметить, что наша функция на самом деле содержит итеративные и рекурсивные элементы. Нет причин, по которым алгоритм должен быть исключительно тем или иным. Совершенно нормально иметь что-то итеративное, например функцию forEach, содержащую рекурсивные вызовы самой себя.
Давайте на мгновение вернёмся ко второму пункту. Функцию будет легче читать, только если вы поймёте, как работает рекурсия вне рамок Фибоначчи, факториала и любых других подобных функций, которые можно найти в книге/курсе «To Crack The Coding Interview». Итак, давайте немного углубимся в то, что именно происходит внутри нашей рекурсивной функции.
Вот несколько структур, которые я написал, чтобы попытаться пояснить их в дальнейшем.
Поскольку мы снова рекурсивно вызвали нашу функцию, мы пока не переходим к третьему отделу, поскольку наша рекурсивная функция должна обрабатываться первой, то есть мы всё ещё обрабатываем второй отдел. Технический способ объяснить это заключается в том, что наш рекурсивный вызов добавляется в наш стек вызовов.
Третий отдел (третье подразделение) имеет аналогичную структуру со вторым отделом (второе подразделение), в то время как четвёртый отдел имеет еще два отдела, а эти два отдела также содержат очередные два отдела — а наша рекурсивная функция проходит по каждому из них. Я не приложил фрагмент кода для этого случая, поскольку считаю, что вы уже поняли, как работает рекурсия.
Заключение
Итак, мы рассмотрели пример рекурсии на практике. Надеюсь, это дало вам более глубокое понимание рекурсии, а также вы узнали один способ решения задач, требующих определённого цикла.
Однако я хотел бы еще раз подчеркнуть: если вы используете рекурсию, производительность кода может снизиться, хотя этого не должно быть. Рекурсия не должна внезапно стать вашим привычным инструментом вместо итерации. Выгода, которую вы добились в читаемости кода, может быть потеряна в его производительности. В конечном счёте это зависит от представленной вам задачи. Вы столкнётесь с некоторыми задачами в программировании, которые могут хорошо подойти для рекурсии, в то время как другие задачи могут лучше подойти для итераций. В некоторых случаях, например в задаче, с которой мы столкнулись ранее, лучше всего использовать оба подхода. А если вы уже давно выучили рекурсию и хотите новых знаний, например в области Data Science или Machine Learning — используйте промокод HABR, который дает +10% к скидке на обучение, указанной ниже на баннере.
Разбираемся в рекурсии
Про рекурсию ходит много шуток, и она традиционно считается одной из сложных для понимания тем в computer science, поэтому давайте сегодня немного о ней поговорим. А именно, давайте обсудим, как выражать доказуемо завершимые вычисления.
Зачем это надо? Рекурсия — один из краеугольных камней ФП, а некоторые из функциональных языков (например, Idris или Agda) обладают достаточно мощной системой типов, чтобы использовать их для проверки доказательств. А чтобы проверенным доказательствам на самом деле можно было доверять, было бы неплохо, чтобы логическая система, которую представляет система типов языка, была консистентна — то есть, если упрощать, чтобы в ней нельзя было доказать ложь.
Один из главных источников неконсистентности — незавершающиеся вычисления (для примера см. КДПВ), поэтому вышеупомянутые языки очень стараются дать возможность убедиться, что вычисления завершаются — соответствующая их часть даже имеет отдельное название, «termination checker». Но, увы, по фундаментальным причинам у любой такой проверки всегда будут ложноположительные или ложноотрицательные срабатывания, поэтому приходится идти на компромиссы. В доказательствах лучше перебдеть, чем недобдеть, поэтому всегда есть завершимые функции, которые этими языками отвергаются. Однако, эти функции можно переписать так, чтобы termination checker был доволен, если можно доказать, что рекурсивный вызов всегда в каком-то смысле «меньше».
Не так давно мне нужно было убедить Агду, что куча взаимно рекурсивных функций всегда завершается. Для этого пришлось почитать стандартную библиотеку и пораскрывать встречающиеся абстракции, чтобы понять, что же там на самом деле происходит. В процессе я делал заметки, а потом понял, что если добавить в эти заметки слова, то может получиться полезный кому-то ещё текст.
Немного вводных
Сначала определим одно слово, которое дальше будет часто встречаться. Фундированное отношение на множестве — это такое отношение, у которого нет бесконечных убывающих цепочек элементов. Стандартное определение немного отличается, но для наших множеств (заведомо счётных, с другими даже идеальные Тьюринг-полные компьютеры не умеют работать) разница невелика и без аксиомы выбора. В качестве синонима в конструктивных контекстах часто используется понятие «доступности» (или как на русский перевести «accessible» в этом контексте?), которым я тоже иногда буду пользоваться.
Кроме того, немного про Агду, на которой мы и будем всё это писать. Это язык из ML-семейства с похожим на хаскель синтаксисом и с поддержкой зависимых типов. Стоит упомянуть пару синтаксических особенностей, которые не встречаются, пожалуй, ни в одном другом языке:
Ещё я иногда буду писать слово «свидетель утверждения X», обозначая этим терм, имеющий тип, соответствующий утверждению X.
Расковыриваем НОД
Один из классических примеров, на котором ломаются стандартные termination checker’ы — алгоритм Евклида для нахождения наибольшего общего делителя двух чисел. При этом он достаточно прост для того, чтобы не тратить внимание на неважные детали, да и, оказывается, в стандартной библиотеке Агды он уже реализован. Нас интересует, в частности, вот эта функция:
Здесь и дальше я буду приводить код в виде скриншотов, так как Хабр не умеет в раскрашивание Агды (что объяснимо, без запросов к тайпчекеру там не разберёшься), да и весь нужный уникод не у всех есть.
Если мы пройдём по цепочке импортов, то увидим, что Acc определён так:
Кроме того, Acc параметризован:
В принципе, можно было бы сразу подставить тело этого определения, но давайте для полноты разберёмся с типами.
Пожалуй, смысл этих типов можно было бы понять из контекста, но давайте не будем жульничать и посмотрим на определения.
С RecStruct всё чуть сложнее:
В любом случае, если пристально посмотреть на это определение, то станет ясно, что RecStruct принимает тип A и возвращает какой-то другой тип — функцию из Pred A в себя же, а Pred A по большому счёту является функцией A → Set — как и положено всякому благочестивому предикату в теории типов.
Но как это вообще связано с завершимостью? Почему этого Acc достаточно, чтобы доказать, что что-то завершается?
Доступность и структурная рекурсия
Оказывается, что это наша старая добрая структурная рекурсия под прикрытием.
В структурной рекурсии всё в порядке, если, сильно упрощая, мы совершаем рекурсивный вызов на синтаксическом субтерме одного из наших термов-аргументов. Вот, например, привычный Фибоначчи:
В Фибоначчи используется один из самых простых типов данных в мире, тип натуральных чисел:
но такая же логика работает и для чего-нибудь более сложного. Например, для бинарных деревьев:
Рекурсивные вызовы на каждом из поддеревьев, естественно, вполне себе корректны и доказуемо завершимы:
А теперь время для ключевого трюка. Заметим, что определение Tree выше изоморфно такому:
Аналогично можно поступить и с натуральными числами, просто в этом случае функция будет принимать аргумент типа, содержащего всего одно значение:
Подход Tree’ и ℕ’ выглядит более тяжеловесно и неуклюже, чем привычный способ описания типов, но у него есть два преимущества. Во-первых, этот подход хорошо обобщается и куда более выразителен. Например, можно представить себе дерево со счётно бесконечным числом поддеревьев в каждом узле:
Или дерево, где в каждом узле конечное, но неизвестное заранее число поддеревьев:
Во-вторых, возвращаемые значения функций, «хранящихся» в конструкторах, считаются termination checker’ом структурно меньшими, так что мы спокойно можем делать рекурсивные вызовы на этих возвращаемых значениях (и метатеория языка гарантирует, что это на самом деле всё ещё консистентно). Например, можно написать что-то в духе подсчёта глубины «диагонали» дерева с бесконечным числом детей в каждом узле:
Визуализировать эту функцию уже не так просто, как написать, но написать можно, и termination checker вполне корректно будет считать её тотальной.
Если вернуться к нашим НОДам, то можно заметить, что Acc имеет примерно ту же форму, что и все эти забавные типы, описанные выше. В частности, конструктор Acc _ принимает функцию, которая по элементу y и свидетелю y возвращает другой Acc (конкретнее, значение типа Acc _ ). Теперь мы знаем, что termination checker считает этот Acc _ как структурно меньший, чем исходный Acc _ (кстати, даже несмотря на то, что его тип отличается). Поэтому мы можем передать это новое значение в рекурсивный вызов, и termination checker с удовольствием посчитает это корректной завершимой рекурсией, даже если ни один из прочих аргументов не стал структурно меньше.
В каком-то смысле Acc позволяет преобразовать «меньше-согласно-отношению» в «структурно-меньше», и нам, программистам, остаётся заполнить пробелы в этом преобразовании.
Примеры
Но как именно выглядит это преобразование?
Натуральные числа
Это доказательство — просто объект типа Acc _ для любого x :
После обычных для Агды пасов мы придём к чему-то вроде такого:
Если теперь перейти ко второй дырке, убрать dot pattern и дать имя первому аргументу, то получим что-то такое:
В дырке при этом будет такая цель и такой контекст:
Пары чисел
Что насчёт чего-нибудь более сложного, как, например, пар натуральных чисел с лексикографическим порядком?
Такой порядок можно определить, например, так:
Доказательство его фундированности предлагается читателю в качестве упражнения.
Ладно, шучу, мне просто лень описывать процесс разработки доказательства. Конечный результат будет выглядеть примерно так:
Контрпримеры
Итак, мы встретились с парой типов и отношений на них, а также доказали их вполне упорядоченность. Но что случится, если мы попытаемся доказать что-то про фундированность отношения, которое таковым не является? Где именно и что именно сломается? Доказывать, что какие-то вещи невыразимы, бывает сложно, но мы попытаемся хотя бы немножко приблизиться к интуитивному пониманию этой самой невыразимости. Да и лично я считаю, что контрпримеры так же важны для понимания, как и обычные, положительные примеры, так что давайте ломать!
Тривиальный тип
Пожалуй, самый простой пример — тип-синглтон с отношением, которое выполняется для любых двух элементов этого типа (тривиальным образом, так как у этого типа всего один элемент):
Давайте начнём писать доказательство фундированности:
Каков тип этой дырки?
Единственный способ создать значение типа Acc — через конструктор acc :
Какой тип дырки перед нами после этого?
Ходим кругами
Что насчёт чего-нибудь поинтереснее? Давайте поиграем в камень-ножницы-бумагу, также известные как числа Пеано без аксиомы ∀x. suc(x) ≠ 0 на трёхэлементном множестве:
Из-за конечности Obj представляется разумным попытаться доказать фундированность через case split по аргументу. Затем давайте рассмотрим произвольную ветку после сплита (я люблю метал, поэтому выберу rock ):
Бесконечные цепи уникальных элементов
Или, другими словами, пусть у нас есть такой свидетель. Тогда мы можем скормить ему 0, заем 1, затем 2, и так далее. Так как мы по факту имеем структурную рекурсию, то мы сможем написать незавершающееся вычисление, но, так как Агда консистентна, этого не может быть!
Или, в виде кода, кратко и ясно:
Наконец-то рекурсия
Как же используется доказательство фундированности? Посмотрим ещё раз на функцию вычисления НОД:
Заключение
После этого маленького экскурса у меня получилось написать что-то чуть менее тривиальное, с кучей взаимно рекурсивных функций, бегающих по взаимно рекурсивным деревьям вывода в системе типов, формализацией которой я сейчас занимаюсь. Надеюсь, что если тебе, дорогой читатель, понадобится доказуемо завершимая рекурсия, эти записи помогут тебе с ней разобраться. Тем более, что, на мой взгляд, чаще всего все доказательства завершимости сводятся к введению размера как прямого отображения на множество натуральных чисел, а там с фундированностью всё просто, и 640 килобайт Acc _ хватит всем.