Тотальность: как доказывается завершение

Пометка тотальная перед словом функция — обещание: функция завершается на любом входе. Компилятор проверяет это обещание при check, и файл с недоказанной тотальной функцией не проходит (код возврата 1). Функцию без пометки можно писать как угодно, но её нельзя позвать из проверки фактов (flang facts, глава «Факт-чекинг»).

Все примеры главы проверены на flang 0.7.29. Подробное руководство лежит в репозитории языка: docs/guide/totality.ru.md.

Идея

Значения flang — конечные деревья: список, запись, вариант, скаляр. Бесконечной цепочки «часть от части от части» не бывает. Значит, достаточно показать, что на каждом рекурсивном вызове что-то строго уменьшается и уменьшаться бесконечно не может. В 0.7.29 таких способов три.

Способ первый: часть значения

Хвост списка из образца голова и хвост, поле варианта из образца, поле записи, элемент коллекции в отобразить / отфильтровать / свёртка. Объявлять ничего не нужно — компилятор видит это сам:

модуль «Проба»

тотальная функция «Длина»
  принимает элементы: список числа
  возвращает число
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то 1 плюс «Длина» от хвоста

$ flang check len.flang
модуль «Проба»: функций 1, из них с доказанным завершением 1; типов 0
len.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

хвост пришёл из образца, значит он — часть элементов. Значение, которое строится заново (литерал списка, добавить … к …, арифметика, результат вызова), частью параметра не считается.

Строки обходятся так же: встроенная форма разложить … на символы превращает строку в список символов, и посимвольный проход становится рекурсией по хвосту:

модуль «Проба»

тотальная функция «Длина списка»
  принимает элементы: список строки
  возвращает число
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то 1 плюс «Длина списка» от хвоста

тотальная функция «Сколько букв»
  принимает текст: строка
  возвращает число
  пример «Три»
    дано текст равно "мир"
    ожидается 3
  «Длина списка» от (разложить текст на символы)

$ flang test letters.flang
letters.flang: примеров 1, прошло 1, не прошло 0

Способ второй: постоянный шаг с проверкой снизу

Число, которое уменьшается на постоянную, и ветвь, которая обрывает спуск. Нужны оба условия:

модуль «Проба»

тотальная функция «Обратный счёт»
  принимает н: число
  возвращает число
  если н не больше 0
    то 0
    иначе 1 плюс «Обратный счёт» от (н минус 1)

check эту функцию принимает. Стоит заменить не больше 0 на равен 0 — и файл не пройдёт: при н = -1 проверка не сработает никогда.

модуль «Проба»

тотальная функция «Обратный отсчёт»
  принимает н: число
  возвращает число
  если н равен 0
    то 0
    иначе «Обратный отсчёт» от (н минус 1)

$ flang check count0.flang
модуль «Проба»: функций 1, из них с доказанным завершением 0; типов 0
без доказанного завершения: «Обратный отсчёт»
FLANG_NOT_TOTAL в файле count0.flang, строка 8, столбец 11: тотальная функция «Обратный отсчёт»: рекурсивный вызов «Обратный отсчёт» не убывает — аргумент 1 («н» sub 1) уменьшает параметр «н», но снизу «н» ничем не ограничен: добавьте проверку вида «если н не больше 0». …
count0.flang: не проверено — замечаний 1

Сообщение называет функцию, аргумент, причину и способ починить.

Способ третий: объявленная мера убывает

Когда уменьшается не аргумент, а выражение от аргументов, его объявляют строкой убывает … сразу после возвращает. Пример — счёт вверх до предела, который без меры не проходит:

модуль «Проба»

тотальная функция «Счёт вверх»
  принимает н: число, предел: число
  возвращает число
  убывает предел минус н
  если н не меньше предел
    то н
    иначе «Счёт вверх» от (н плюс 1) и предел

Для каждого рекурсивного вызова компилятор даёт один из трёх ответов.

Доказано. Мера — параметр типа неотрицательное, и вызов передаёт его минус постоянную. Дно даёт тип, шаг точен, проверок во время работы не остаётся:

модуль «Проба»

тотальная функция «Через два»
  принимает н: неотрицательное
  возвращает число
  убывает н
  если н не больше 1
    то н
    иначе «Через два» от (н минус 2)

$ flang check dn.flang --proof
…
чем несётся обещание «тотальная»:
  «Через два»  доказано точным шагом: аргумент 1 («н») объявлен натуральным и убывает на 2; …

Отказ. Вызов, который меру уменьшить не может (н плюс 1, само н, умножение на число не меньше единицы), отвергается уже при check.

Проверка при запуске. Всё остальное компилятор принимает на слово автора и вставляет проверку меры в код. «Счёт вверх» выше — такой случай. Ещё один, с неудачно выбранной мерой, проходит check:

модуль «Проба»

тотальная функция «Сближение»
  принимает низ: число, верх: число
  возвращает число
  убывает верх минус низ
  если верх не больше низ
    то низ
    иначе «Сближение» от (низ плюс 2) и верх

$ flang run meas.flang --function "Сближение" --args '{"низ": 0, "верх": 5}'
FLANG_MEASURE: тотальная функция «Сближение»: мера на вызове «Сближение» — «верх» минус «низ» — ушла ниже нуля. …

От 0 до 5 шагом два мера идёт 5, 3, 1, −1 — и запуск останавливается с кодом 1, а не уходит в бесконечность. С "верх": 4 та же функция возвращает 4. Сколько таких мест в программе, показывает итог check --proof: там отдельной строкой посчитаны проверки, оставленные на время работы.

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

Один убывающий аргумент на весь цикл

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

модуль «Проба»

тотальная функция «А»
  принимает а: список числа, б: список числа
  возвращает число
  разбор а
    случай пусто
      то 0
    случай голова и хвост
      то «Б» от хвост и (добавить голова к б)

тотальная функция «Б»
  принимает а: список числа, б: список числа
  возвращает число
  разбор б
    случай пусто
      то 0
    случай голова и хвост
      то «А» от (добавить голова к а) и хвост

$ flang check ab.flang
…
FLANG_NOT_TOTAL в файле ab.flang, строка 10, столбец 10: в цикле «А» → «Б» нет аргумента, который убывает на каждом вызове: «А» → «Б» убывает по аргументу 1 (параметр «а»); «Б» → «А» убывает по аргументу 2 (параметр «б»). Нужен один и тот же убывающий аргумент на всех рёбрах цикла

Каждый вызов где-то убывает, но то, что отнято у одного списка, добавляется к другому, и пара по кругу не уменьшается. Правило «каждый вызов убывает хоть где-нибудь» было бы неверным.

По той же причине не проходит функция Аккермана: один вызов уменьшает м, другой — н, а лексикографического порядка анализ не знает. Её можно записать с мерой убывает, но тогда завершение проверяется при запуске, а не доказывается.

Что анализ отвергает

• Счёт вверх без меры: н плюс 1 увеличивает аргумент, а неизменный предел частью значения не является.
• Шаг без проверки снизу (равен 0 вместо не больше 0).
• Разные убывающие аргументы на разных вызовах одного цикла.
• Убывание через результат другой функции: результат вызова — новое значение, а не часть аргумента.

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

Зачем это нужно

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

$ flang facts fc1.flang --claims '["«Цифр в числе» от 5 равно 1"]'
{"ok":false,"results":[{"claim":"«Цифр в числе» от 5 равно 1","holds":false,"why":"функция «Цифр в числе» не помечена как «тотальная»; факт-чекинг допускает только тотальные функции — иначе ответ может не наступить",…,"status":"refused"}]}

Здесь fc1.flang — обычная функция «Цифр в числе», которая зовёт себя от собственного результата.

Сколько это стоит

Счёт объявлений по файлам на дереве выпуска 0.7.29 (коммит dc76a0b):

Пересчитать: cat <каталог>/*.flang | grep -cE '^(тотальная )?функция «', то же с '^тотальная функция «' и с '^ убывает '.

Библиотека и решения задач почти целиком тотальны. Компилятор — меньше: он не обещает остановку на любом входе и имеет право упереться в предел шагов (--step-limit). Тотальность здесь — не оценка кода, а обязательство перед тем, кто функцию вызывает.

Цена видна в самом коде: чтобы остаться в классе, иногда пишут не так, как думают, а так, как примет анализ, — свёртку по заранее известному списку вместо цикла «пока есть символы», меру вместо счётчика. Зато отказ предсказуем и объяснён в сообщении.

Дальше — глава «Стандартная библиотека».