Анализ прекращения - Termination analysis

void f(int n) {
   while (n > 1)
      if (n % 2 == 0)
          n = n / 2;
      else
          n = 3 * n + 1;
}
По состоянию на 2021 год все еще неизвестно
, завершается ли эта C- программа
для каждого ввода;
см. гипотезу Коллатца .

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

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

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

Доказательство расторжения

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

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

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

Пример

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

i := 0
loop until i = SIZE_OF_DATA
    process_data(data[i])) // process the data chunk at position i
    i := i + 1 // move to the next chunk of data to be processed

Если значение SIZE_OF_DATA неотрицательное, фиксированное и конечное, цикл в конечном итоге завершится, при условии, что process_data также завершится.

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

i := 1
loop until i = 0
    i := i + 1

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

i := 1
loop until i = UNKNOWN
    i := i + 1

Здесь условие цикла определяется с использованием некоторого значения UNKNOWN, где значение UNKNOWN неизвестно (например, определяется вводом пользователя при выполнении программы). Здесь анализ завершения должен учитывать все возможные значения UNKNOWN и выяснять, что в возможном случае UNKNOWN = 0 (как в исходном примере) завершение не может быть показано.

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

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

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

function factorial (argument as natural number)
    if argument = 0 or argument = 1
        return 1
    otherwise
        return argument * factorial(argument - 1)

Зависимые типы

Завершающая проверка очень важна в языках программирования с зависимой типизацией и в системах доказательства теорем, таких как Coq и Agda . Эти системы используют изоморфизм Карри-Ховарда между программами и доказательствами. Доказательства над индуктивно определенными типами данных традиционно описывались с использованием принципов индукции. Однако позже было обнаружено, что описание программы с помощью рекурсивно определенной функции с сопоставлением с образцом является более естественным способом доказательства, чем прямое использование принципов индукции. К сожалению, разрешение неограниченных определений приводит к логической несогласованности в теориях типов. Вот почему Agda и Coq имеют встроенные средства проверки завершения.

Типоразмеры

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

Текущее исследование

Есть несколько исследовательских групп, которые работают над новыми методами, которые могут показать (не) прекращение. Многие исследователи включают эти методы в программы, которые пытаются анализировать поведение завершения автоматически (без вмешательства человека). Постоянный аспект исследования - позволить использовать существующие методы для анализа поведения завершения программ, написанных на языках программирования «реального мира». Для декларативных языков, таких как Haskell , Mercury и Prolog , существует множество результатов (в основном из-за сильной математической основы этих языков). Исследовательское сообщество также работает над новыми методами анализа поведения завершения программ, написанных на императивных языках, таких как C и Java.

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

Смотрите также

Рекомендации

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

Системные описания инструментов автоматического анализа завершения включают:

Внешние ссылки