В информатике анализ завершения — это программный анализ , который пытается определить , останавливается ли оценка данной программы для каждого ввода. Это означает определить, вычисляет ли программа ввода общую функцию.
Она тесно связана с проблемой остановки , которая заключается в определении того, останавливается ли данная программа для заданного ввода и которая неразрешима . Анализ остановки еще сложнее, чем проблема остановки: анализ остановки в модели машин Тьюринга как модели программ, реализующих вычислимые функции, имел бы целью решить, является ли данная машина Тьюринга полной машиной Тьюринга , и эта проблема находится на уровне арифметической иерархии и, таким образом, строго сложнее, чем проблема остановки.
Теперь, поскольку вопрос о том, является ли вычислимая функция полной, не является полуразрешимым , [1] каждый анализатор завершения (то есть утвердительный ответ никогда не дается для незавершающейся программы) является неполным , то есть должен потерпеть неудачу в определении завершения для бесконечного числа завершающихся программ, либо работая вечно, либо останавливаясь с неопределенным ответом.
Доказательство завершения — это тип математического доказательства , который играет решающую роль в формальной проверке, поскольку от завершения зависит общая правильность алгоритма .
Простой, общий метод построения доказательств завершения включает в себя связывание меры с каждым шагом алгоритма. Мера берется из области хорошо обоснованного отношения , например, из порядковых чисел . Если мера «уменьшается» в соответствии с отношением на каждом возможном шаге алгоритма, он должен завершиться, поскольку нет бесконечных нисходящих цепей относительно хорошо обоснованного отношения.
Некоторые типы анализа прекращения могут автоматически генерировать или подразумевать наличие доказательства прекращения.
Примером конструкции языка программирования , которая может или не может завершиться, является цикл , поскольку они могут выполняться повторно. Циклы, реализованные с использованием переменной-счетчика , как правило, встречающейся в алгоритмах обработки данных , обычно завершаются, что демонстрируется в примере псевдокода ниже:
i := 0 цикл до тех пор, пока i = SIZE_OF_DATA process_data(data[i])) // обработать фрагмент данных в позиции i i := i + 1 // перейти к следующему фрагменту данных для обработки
Если значение SIZE_OF_DATA неотрицательное, фиксированное и конечное, цикл в конечном итоге завершится, если предположить, что process_data также завершится.
Некоторые циклы могут быть показаны как всегда завершающиеся или никогда не завершающиеся с помощью человеческого контроля. Например, следующий цикл, теоретически, никогда не остановится. Однако он может остановиться при выполнении на физической машине из-за арифметического переполнения : либо приводя к исключению , либо заставляя счетчик переходить к отрицательному значению и позволяя условию цикла быть выполненным.
i := 1 цикл , пока i = 0 я := я + 1
В анализе завершения можно также попытаться определить поведение завершения некоторой программы в зависимости от некоторого неизвестного ввода. Следующий пример иллюстрирует эту проблему.
i := 1 цикл , пока i = НЕИЗВЕСТНО я := я + 1
Здесь условие цикла определяется с использованием некоторого значения UNKNOWN, где значение UNKNOWN неизвестно (например, определяется вводом пользователя при выполнении программы). Здесь анализ завершения должен учитывать все возможные значения UNKNOWN и выяснить, что в возможном случае UNKNOWN = 0 (как в исходном примере) завершение не может быть показано.
Однако не существует общей процедуры для определения того, остановится ли выражение, включающее циклические инструкции, даже если люди должны выполнить проверку. Теоретическая причина этого — неразрешимость проблемы остановки: не может существовать алгоритма, который определяет, остановится ли любая заданная программа после конечного числа шагов вычисления.
На практике не удается показать завершение (или незавершение), потому что каждый алгоритм работает с конечным набором методов, способных извлечь соответствующую информацию из заданной программы. Метод может смотреть, как изменяются переменные относительно некоторого условия цикла (возможно, показывая завершение для этого цикла), другие методы могут попытаться преобразовать вычисление программы в некоторую математическую конструкцию и работать над ней, возможно, получая информацию о поведении завершения из некоторых свойств этой математической модели. Но поскольку каждый метод способен «видеть» только некоторые конкретные причины (не)завершения, даже с помощью комбинации таких методов невозможно охватить все возможные причины (не)завершения. [ необходима цитата ]
Рекурсивные функции и циклы эквивалентны по выражению; любое выражение, включающее циклы, может быть записано с использованием рекурсии, и наоборот. Таким образом, завершение рекурсивных выражений также неразрешимо в общем случае. Можно показать, что большинство рекурсивных выражений, встречающихся в общем употреблении (т. е. не патологических ), завершаются различными способами, обычно в зависимости от определения самого выражения. Например, аргумент функции в рекурсивном выражении для факториальной функции ниже всегда будет уменьшаться на 1; по свойству хорошего упорядочения натуральных чисел аргумент в конечном итоге достигнет 1, и рекурсия завершится.
функция факториал (аргумент как натуральное число) , если аргумент = 0 или аргумент = 1, возвращает 1, в противном случае возвращает аргумент * факториал(аргумент - 1)
Проверка завершения очень важна в языках программирования с независимой типизацией и системах доказательства теорем, таких как Coq и Agda . Эти системы используют изоморфизм Карри-Ховарда между программами и доказательствами. Доказательства над индуктивно определенными типами данных традиционно описывались с использованием принципов индукции. Однако позже было обнаружено, что описание программы с помощью рекурсивно определенной функции с сопоставлением с образцом является более естественным способом доказательства, чем прямое использование принципов индукции. К сожалению, разрешение нетерминируемых определений приводит к логической непоследовательности в теориях типов [ требуется ссылка ] , поэтому в Agda и Coq есть встроенные средства проверки завершения.
Одним из подходов к проверке завершения в языках программирования с зависимой типизацией являются типы размера. Основная идея заключается в аннотировании типов, по которым мы можем рекурсивно выполнять рекурсию, с помощью аннотаций размера и разрешении рекурсивных вызовов только для меньших аргументов. Типы размера реализованы в Agda как синтаксическое расширение.
Есть несколько исследовательских групп, которые работают над новыми методами, которые могут показать (не)завершение. Многие исследователи включают эти методы в программы [2] , которые пытаются автоматически анализировать поведение завершения (то есть без человеческого взаимодействия). Текущий аспект исследований заключается в том, чтобы позволить существующим методам использоваться для анализа поведения завершения программ, написанных на языках программирования «реального мира». Для декларативных языков, таких как Haskell , Mercury и Prolog , существует много результатов [3] [4] [5] (в основном из-за сильной математической основы этих языков). Исследовательское сообщество также работает над новыми методами анализа поведения завершения программ, написанных на императивных языках, таких как C и Java.
Научные работы по анализу автоматического завершения программ включают:
Описания систем автоматизированных инструментов анализа прекращения включают:
