void f ( int n ) { while ( n > 1 ) if ( n % 2 == 0 ) n = n / 2 ; иначе n = 3 * n + 1 ; } |
По состоянию на 2021 год все еще неизвестно , завершается ли эта C- программа для каждого ввода; см. гипотезу Коллатца . |
В информатике , анализ завершения является программа анализ , который пытается определить , является ли оценка данной программы остановок для каждого входа. Это означает определение того, вычисляет ли программа ввода общую функцию.
Это тесно связано с проблемой остановки , которая заключается в том, чтобы определить, останавливается ли данная программа для данного ввода и что является неразрешимым . Анализ завершения даже сложнее, чем проблема остановки: анализ завершения в модели машин Тьюринга как модели программ, реализующих вычислимые функции, будет иметь цель решить, является ли данная машина Тьюринга полной машиной Тьюринга , и эта проблема является на уровнеиз арифметической иерархии , и , таким образом , является строго более трудным , чем проблемы остановки.
Теперь, поскольку вопрос о том, является ли вычислимая функция тотальной, не является полуразрешимым , [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.
Из-за неразрешимости проблемы остановки исследования в этой области не могут достичь полноты. Всегда можно придумать новые методы, которые находят новые (сложные) причины прекращения.
Смотрите также
- Анализ сложности - проблема оценки времени, необходимого для завершения
- Вариант петли
- Полное функциональное программирование - парадигма программирования, которая ограничивает диапазон программ теми, которые доказуемо завершаются.
- Рекурсия Вальтера
Рекомендации
- Перейти ↑ Rogers, Jr., Hartley (1988). Теория рекурсивных функций и эффективной вычислимости . Кембридж (Массачусетс), Лондон (Англия): MIT Press. п. 476. ISBN. 0-262-68052-1.
- ^ Инструменты на termination-portal.org
- ^ Giesl, J. и Swiderski, S. и Schneider-Kamp, P. и Thiemann, R. Pfenning, F. (ed.). Автоматический завершающий анализ для Haskell: от переписывания терминов к языкам программирования (приглашенная лекция) (постскриптум) . Изменение сроков и заявки, 17-е межд. Конф., РТА-06. LNCS. 4098 . С. 297–312. (ссылка: springerlink.com ).CS1 maint: использует параметр авторов ( ссылка )
- ^ Параметры компилятора для анализа завершения в Mercury
- ^ http://verify.rwth-aachen.de/giesl/papers/lopstr07-distribute.pdf
Исследовательские работы по автоматическому анализу завершения программ включают:
- Кристоф Вальтер (1988). "Аргумент-ограниченные алгоритмы как основа для автоматизированных доказательств завершения". Proc. 9-я конференция по автоматическому отчислению . LNAI. 310 . Springer. С. 602–621.
- Кристоф Вальтер (1991). «О доказательстве завершения алгоритмов машиной» (PDF) . Искусственный интеллект . 70 (1).
- Си, Хунвэй (1998). «На пути к автоматическому доказательству прекращения посредством замораживания » (PDF) . В Тобиасе Нипкове (ред.). Методы перезаписи и приложения , 9-е межд. Конф., РТА-98 . LNCS. 1379 . Springer. С. 271–285.
- Юрген Гисль; Кристоф Вальтер; Юрген Браубургер (1998). «Завершающий анализ функциональных программ». У В. Бибеля; П. Шмитт (ред.). Автоматическое вычитание - основа для приложений (постскриптум) . 3 . Дордрехт: Kluwer Academic Publishers. С. 135–164.
- Кристоф Вальтер (2000). «Критерии прекращения действия». В С. Hölldobler (ред.). Интеллект и вычислительная логика (постскриптум) . Дордрехт: Kluwer Academic Publishers. С. 361–386.
- Кристоф Вальтер; Стефан Швейцер (2005). «Автоматический анализ завершения для не полностью определенных программ» (PDF) . У Франца Баадера; Андрей Воронков (ред.). Proc. 11-е межд. Конф. по логике программирования, искусственного интеллекта и рассуждений (LPAR) . LNAI. 3452 . Springer. С. 332–346.
- Адам Копровски; Йоханнес Вальдманн (2008). «Арктическое прекращение ... ниже нуля». У Андрея Воронкова (ред.). Методы перезаписи и приложения, 19-я Международная конференция. Конф., РТА-08 (PDF) . Конспект лекций по информатике. 5117 . Springer. С. 202–216. ISBN 978-3-540-70588-8.
Системные описания инструментов автоматического анализа завершения включают:
- Гизл, Дж. (1995). «Генерация полиномиальных порядков для доказательств завершения (описание системы)». В Сян, Цзе (ред.). Методы перезаписи и приложения, 6-е Междунар. Конф., РТА-95 (постскриптум) . LNCS. 914 . Springer. С. 426–431.
- Ohlebusch, E .; Claves, C .; Марше, К. (2000). «TALP: Инструмент для окончательного анализа логических программ (описание системы)». В Bachmair, Лео (ред.). Методы перезаписи и приложения, 11-е Int. Конф., РТА-00 (сжатый постскриптум) . LNCS. 1833 . Springer. С. 270–273.
- Hirokawa, N .; Миддельдорп, А. (2003). «Tsukuba Termination Tool (системное описание)». В Nieuwenhuis, R. (ed.). Методы перезаписи и приложения, 14-я Int. Конф., РТА-03 (PDF) . LNCS. 2706 . Springer. С. 311–320.
- Giesl, J .; Thiemann, R .; Schneider-Kamp, P .; Фальке, С. (2004). «Автоматизированные доказательства расторжения с AProVE (описание системы)». В van Oostrom, V. (ed.). Методы перезаписи и приложения, 15-е Int. Конф., РТА-04 (PDF) . LNCS. 3091 . Springer. С. 210–220. ISBN 3-540-22153-0.
- Hirokawa, N .; Мидделдорп, А. (2005). «Тирольский инструмент прекращения (описание системы)». В Giesl, J. (ред.). Изменение сроков и заявки, 16-е межд. Конф., РТА-05 . LNCS. 3467 . Springer. С. 175–184. ISBN 978-3-540-25596-3.
- Копровский, А. (2006). «TPA: прекращение действия подтверждено автоматически (описание системы)». В Пфеннинге, Ф. (ред.). Изменение сроков и заявки, 17-е межд. Конф., РТА-06 . LNCS. 4098 . Springer. С. 257–266.
- Marché, C .; Зантема, Х. (2007). «Прекращение конкурса (описание системы)». В Баадере, Ф. (ред.). Изменение сроков и заявки, 18-е межд. Конф., РТА-07 (PDF) . LNCS. 4533 . Springer. С. 303–313.
Внешние ссылки
- Завершающий анализ функциональных программ высшего порядка
- Список рассылки инструментов прерывания
- Прекращение конкурса - см. Marché, Zantema (2007) для описания
- Портал прекращения действия