Анализ завершения

Доказательство завершения — это разновидность математического доказательства, играющая важную роль в формальной верификации, поскольку тотальная корректность алгоритма зависит от его завершения.

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

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

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

i := 0
цикл пока i ≠ РАЗМЕР_ДАННЫХ
    process_data(data[i]) // обработать фрагмент данных с индексом i
    i := i + 1 // перейти к следующему фрагменту данных

Если значение РАЗМЕР_ДАННЫХ неотрицательно, фиксировано и конечно, цикл в конечном итоге завершится, при условии, что process_data также завершается.

Некоторые циклы можно показать как всегда завершающиеся или никогда не завершающиеся при ручном анализе. Например, следующий цикл теоретически никогда не завершится. Однако на реальной машине он может завершиться из-за арифметического переполнения: либо произойдёт исключение, либо счётчик перейдёт в отрицательное значение, что позволит выполнить условие завершения цикла.

i := 1
цикл пока i ≠ 0
    i := i + 1

В анализе завершения также может ставиться задача определить поведение программы относительно завершения в зависимости от неизвестного входного значения. Следующий пример иллюстрирует эту проблему.

i := 1
цикл пока i ≠ НЕИЗВЕСТНО
    i := i + 1

Условие выхода из цикла определяется некоторым значением НЕИЗВЕСТНО, которое заранее неизвестно (например, задаётся пользователем при запуске программы). В этом случае анализ завершения должен учитывать все возможные значения НЕИЗВЕСТНО и установить, что, например, при НЕИЗВЕСТНО = 0 (как в исходном примере) завершение цикла не может быть гарантировано.

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

На практике не удаётся доказать завершение (или незавершение) программы, поскольку любой алгоритм работает с конечным набором методов, способных извлекать релевантную информацию из программы. Один из методов может анализировать, как изменяются переменные относительно условия цикла (возможно, доказывая завершение для этого цикла), другие методы могут пытаться преобразовать вычисления программы в некоторую математическую конструкцию и анализировать её, получая информацию о завершении из свойств этой модели. Но поскольку каждый метод способен «видеть» только определённые причины (не)завершения, даже их комбинация не может охватить все возможные случаи.

Рекурсивные функции и циклы эквивалентны по выразительной мощности: любое выражение с циклами можно записать с помощью рекурсии, и наоборот. Поэтому завершение рекурсивных выражений также в общем случае неразрешимо. Большинство рекурсивных выражений, встречающихся на практике (то есть не патологические), можно доказать завершающимися различными способами, обычно исходя из определения самой функции. Например, аргумент функции в рекурсивном определении факториала ниже всегда уменьшается на 1; по свойству хорошей упорядоченности натуральных чисел аргумент в итоге достигнет 1, и рекурсия завершится.

функция факториал (аргумент как натуральное число)
    если аргумент = 0 или аргумент = 1
        вернуть 1
    иначе
        вернуть аргумент * факториал(аргумент - 1)

Проверка завершения имеет большое значение в языках программирования с зависимыми типами и в системах автоматического доказательства теорем, таких как Rocq и Agda. Эти системы используют изоморфизм Карри — Ховарда между программами и доказательствами. Доказательства над индуктивно определёнными типами данных традиционно строились с помощью индуктивных принципов. Однако позже было обнаружено, что описание программы через рекурсивную функцию с сопоставлением с образцом является более естественным способом доказательства, чем непосредственное использование индуктивных принципов. Разрешение незавершающихся определений приводит к логической противоречивости в теориях типов, поэтому в Agda и Rocq встроены средства проверки завершения.

Существует несколько исследовательских групп, разрабатывающих новые методы доказательства (не)завершения. Исследователи внедряют эти методы в программы^[2], которые пытаются анализировать поведение программ относительно завершения автоматически (то есть без участия человека). Одним из направлений исследований является адаптация существующих методов для анализа завершения программ, написанных на «реальных» языках программирования. Для декларативных языков, таких как Haskell , Mercury и Prolog, существует множество результатов^[3][4][5] (в основном благодаря сильной математической базе этих языков). Ведётся разработка новых методов анализа завершения программ, написанных на императивных языках, таких как C и Java.