Привет, Хабр.
Про рекурсию ходит много шуток, и она традиционно считается одной из сложных для понимания тем в computer science, поэтому давайте сегодня немного о ней поговорим. А именно, давайте обсудим, как выражать доказуемо завершимые вычисления.
Зачем это надо? Рекурсия — один из краеугольных камней ФП, а некоторые из функциональных языков (например, Idris или Agda) обладают достаточно мощной системой типов, чтобы использовать их для проверки доказательств. А чтобы проверенным доказательствам на самом деле можно было доверять, было бы неплохо, чтобы логическая система, которую представляет система типов языка, была консистентна — то есть, если упрощать, чтобы в ней нельзя было доказать ложь.
Один из главных источников неконсистентности — незавершающиеся вычисления (для примера см. КДПВ), поэтому вышеупомянутые языки очень стараются дать возможность убедиться, что вычисления завершаются — соответствующая их часть даже имеет отдельное название, «termination checker». Но, увы, по фундаментальным причинам у любой такой проверки всегда будут ложноположительные или ложноотрицательные срабатывания, поэтому приходится идти на компромиссы. В доказательствах лучше перебдеть, чем недобдеть, поэтому всегда есть завершимые функции, которые этими языками отвергаются. Однако, эти функции можно переписать так, чтобы termination checker был доволен, если можно доказать, что рекурсивный вызов всегда в каком-то смысле «меньше».
Не так давно мне нужно было убедить Агду, что куча взаимно рекурсивных функций всегда завершается. Для этого пришлось почитать стандартную библиотеку и пораскрывать встречающиеся абстракции, чтобы понять, что же там на самом деле происходит. В процессе я делал заметки, а потом понял, что если добавить в эти заметки слова, то может получиться полезный кому-то ещё текст.
