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

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

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

Она тесно связана с проблемой остановки , которая заключается в том, чтобы определить, останавливается ли данная программа для данного ввода, и которая неразрешима . Анализ завершения еще более сложен, чем проблема остановки: анализ завершения в модели машин Тьюринга как модели программ, реализующих вычислимые функции, будет иметь целью решить, является ли данная машина Тьюринга полной машиной Тьюринга , и эта проблема на уровне $\Pi _{2}^{0}$ арифметической иерархии и, следовательно, является строго более сложной, чем проблема остановки.

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

Доказательство прекращения действия [ править ]

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

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

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

Пример [ править ]

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

я := 0 
  цикл  , пока я не = SIZE_OF_DATA 
      process_data(data[i]))  // обрабатываем фрагмент данных в позиции i 
      i := i + 1  // переход к следующему фрагменту данных для обработки

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

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

я := 1 
  цикл  до тех пор, пока я = 0 
      я := я + 1

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

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

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

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

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

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

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

Зависимые типы [ править ]

Проверка завершения очень важна в языках программирования с зависимой типизацией и системах доказательства теорем, таких как Coq и Agda . Эти системы используют изоморфизм Карри-Говарда между программами и доказательствами. Доказательства над индуктивно определенными типами данных традиционно описывались с использованием принципов индукции. Однако позже выяснилось, что описание программы с помощью рекурсивно определенной функции с сопоставлением с образцом является более естественным способом доказательства, чем непосредственное использование принципов индукции. К сожалению, разрешение бесконечных определений приводит к логической несогласованности в теориях типов. ^{[ нужна цитата ]}, поэтому Agda и Coq имеют встроенные средства проверки завершения.

Типы размеров [ править ]

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

Текущее исследование [ править ]

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

См. также [ править ]

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

Ссылки [ править ]

^ Роджерс-младший, Хартли (1988). Теория рекурсивных функций и эффективная вычислимость . Кембридж (Массачусетс), Лондон (Англия): MIT Press. п. 476. ИСБН 0-262-68052-1 .
^ Инструменты на сайте Termination-portal.org.
^ Гизл, Дж.; Свидерски, С.; Шнайдер-Камп, П.; Тиманн, Р. Пфеннинг, Ф. (ред.). Автоматизированный анализ завершения для Haskell: от переписывания терминов к языкам программирования (приглашенная лекция) (постскриптум) . Переписывание терминов и приложения, 17-й Int. конф., РТА-06. ЛНКС. Том. 4098. стр. 297–312. (ссылка: Springerlink.com ).
^ Параметры компилятора для анализа завершения в Mercury
^ http://verify.rwth-aachen.de/giesl/papers/lopstr07-distribute.pdf ^{[ пустой URL PDF ]}

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

Кристоф Вальтер (1988). «Алгоритмы, ограниченные аргументами, как основа автоматического доказательства завершения». Учеб. 9-я конференция по автоматизированному дедукции . ЛНАИ. Том. 310. Спрингер. стр. 602–621.
Кристоф Вальтер (1991). «О доказательстве машинного завершения алгоритмов» . Искусственный интеллект . 70 (1).
Си, Хунвэй (1998). «На пути к автоматизированному подтверждению прекращения действия путем замораживания » (PDF) . В Тобиасе Нипкове (ред.). Техники и приложения переписывания , 9-й Межд. конф., РТА-98 . ЛНКС. Том. 1379. Спрингер. стр. 271–285.
Юрген Гизль; Кристоф Вальтер; Юрген Браубургер (1998). «Анализ завершения функциональных программ». У В. Бибеля; П. Шмитт (ред.). Автоматизированный дедукция – основа для приложений (постскриптум) . Том. 3. Дордрехт: Академическое издательство Kluwer. стр. 135–164.
Кристоф Вальтер (2000). «Критерии прекращения». В С. Хёльдоблере (ред.). Интеллектика и вычислительная логика (постскриптум) . Дордрехт: Kluwer Academic Publishers. стр. 361–386.
Кристоф Вальтер; Стефан Швейцер (2005). «Автоматизированный анализ завершения неполностью определенных программ» (PDF) . У Франца Баадера; Андрей Воронков (ред.). Учеб. 11-й Международный. Конф. по логике программирования, искусственному интеллекту и рассуждению (LPAR) . ЛНАИ. Том. 3452. Спрингер. стр. 332–346.
Адам Копровски; Йоханнес Вальдманн (2008). «Арктическое прекращение ...ниже нуля». У Андрея Воронкова (ред.). Техники и приложения переписывания, 19-й Международный конгресс. Конф., RTA-08 (PDF) . Конспекты лекций по информатике. Том. 5117. Спрингер. стр. 202–216. ISBN 978-3-540-70588-8 .

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

Гизл, Дж. (1995). «Генерация полиномиальных порядков для доказательств завершения (описание системы)». Ин Сян, Цзе (ред.). Техники и приложения переписывания, 6-й Межд. Конф., РТА-95 (постскриптум) . ЛНКС. Том. 914. Спрингер. стр. 426–431.
Олебуш, Э.; Клавес, К.; Марше, К. (2000). «TALP: Инструмент для анализа завершения логических программ (описание системы)». В Бахмайре, Лео (ред.). Техники и приложения переписывания, 11-й Межд. Конф., РТА-00 (сжатый постскриптум) . ЛНКС. Том. 1833. Спрингер. стр. 270–273.
Хирокава, Н.; Мидделдорп, А. (2003). «Инструмент завершения Tsukuba (описание системы)». В Ньювенхейсе, Р. (ред.). Техники и приложения переписывания, 14-й Межд. Конференция, RTA-03 (PDF) . ЛНКС. Том. 2706. Спрингер. стр. 311–320.
Гизл, Дж.; Тиманн, Р.; Шнайдер-Камп, П.; Фальке, С. (2004). «Автоматическое подтверждение прекращения действия с помощью AProVE (описание системы)». Ин ван Оостром, В. (ред.). Техники и приложения переписывания, 15-й Международный конгресс. Конф., RTA-04 (PDF) . ЛНКС. Том. 3091. Спрингер. стр. 210–220. ISBN 3-540-22153-0 .
Хирокава, Н.; Мидделдорп, А. (2005). «Тирольский инструмент терминации (описание системы)». В Гизле, Дж. (ред.). Переписывание терминов и приложения, 16-й Int. конф., РТА-05 . ЛНКС. Том. 3467. Спрингер. стр. 175–184. ISBN 978-3-540-25596-3 .
Копровски, А. (2006). «TPA: прекращение действия подтверждено автоматически (описание системы)». В Пфеннинге, Ф. (ред.). Переписывание терминов и приложения, 17-й Int. конф., РТА-06 . ЛНКС. Том. 4098. Спрингер. стр. 257–266.
Марше, К.; Зантема, Х. (2007). «Конкурс терминации (описание системы)». В Баадер, Ф. (ред.). Переписывание терминов и приложения, 18-й Int. Конференция, RTA-07 (PDF) . ЛНКС. Том. 4533. Спрингер. стр. 303–313.