Проблема с остановкой
Эта статья включает список общих ссылок , но в ней отсутствуют достаточные соответствующие встроенные цитаты . ( сентябрь 2018 г. ) |
В теории вычислимости проблема остановки — это проблема определения на основе описания произвольной компьютерной программы и входных данных, завершит ли программа работу или продолжит работать вечно. Проблема остановки неразрешима , а это означает, что не существует общего алгоритма , который бы решал проблему остановки для всех возможных пар программа-вход. Эта проблема часто возникает при обсуждении вычислимости , поскольку она показывает, что некоторые функции математически определимы , но не вычислимы .
Ключевой частью формальной постановки задачи является математическое определение компьютера и программы, обычно с помощью машины Тьюринга . Затем доказательство показывает, что для любой программы f , которая может определять, остановлены ли программы, существует «патологическая» программа g , для которой f делает неправильное определение. В частности, g — это программа, которая при вызове с некоторыми входными данными передает свой собственный источник и свои входные данные в f и делает противоположное тому, что f предсказывает, что g будет делать. Поведение f на g показывает неразрешимость, поскольку это означает, что ни одна программа f не решит проблему остановки во всех возможных случаях.
Фон
[ редактировать ]Проблема остановки — это проблема решения свойств компьютерных программ на фиксированной модели вычислений , полной по Тьюрингу , то есть всех программ, которые могут быть написаны на некотором заданном языке программирования , который достаточно общий, чтобы быть эквивалентным машине Тьюринга. Проблема состоит в том, чтобы определить, учитывая программу и входные данные для программы, остановится ли программа в конечном итоге при запуске с этими входными данными. В этой абстрактной структуре нет ограничений по ресурсам на объем памяти или время, необходимое для выполнения программы; это может занять сколь угодно много времени и использовать произвольный объем памяти перед остановкой. Вопрос просто в том, остановится ли когда-нибудь данная программа на определенном входе.
Например, в псевдокоде программа
while (true) continue
не останавливается; скорее, это продолжается вечно в бесконечном цикле . С другой стороны, программа
останавливается.
Хотя решить, стоит ли останавливать эти программы, просто, более сложные программы оказываются проблематичными. Одним из подходов к решению проблемы может быть запуск программы на некоторое количество шагов и проверка, не зависает ли она. Однако пока программа работает, неизвестно, остановится ли она в конечном итоге или будет работать вечно. Тьюринг доказал, что не существует алгоритма, который всегда правильно решает, остановится ли программа для данной произвольной программы и входных данных при запуске с этими входными данными. Суть доказательства Тьюринга состоит в том, что любой такой алгоритм может давать противоречивые результаты и, следовательно, не может быть правильным.
Последствия программирования
[ редактировать ]Некоторые бесконечные циклы могут быть весьма полезны. Например, циклы событий обычно кодируются как бесконечные циклы. [1] Однако большинство подпрограмм предназначены для завершения. [2] В частности, при вычислениях в режиме жесткого реального времени программисты пытаются писать подпрограммы, которые не только гарантированно завершатся, но также гарантированно завершатся до заданного срока. [3]
Иногда эти программисты используют какой-нибудь язык программирования общего назначения (полный по Тьюрингу). но попытайтесь писать в ограниченном стиле, таком как MISRA C или SPARK , чтобы легко доказать, что полученные подпрограммы завершаются раньше заданного срока. [ нужна ссылка ]
В других случаях эти программисты применяют правило наименьшей мощности — они намеренно используют компьютерный язык, который не полностью по Тьюрингу. Часто это языки, которые гарантируют завершение всех подпрограмм, например Coq . [ нужна ссылка ]
Распространенные ловушки
[ редактировать ]Сложность проблемы остановки заключается в том, что процедура решения должна работать для всех программ и входных данных. Конкретная программа либо останавливается на заданном вводе, либо не останавливается. Рассмотрим один алгоритм, который всегда отвечает «остановлено», и другой, который всегда отвечает «не останавливается». Для любой конкретной программы и ввода один из этих двух алгоритмов отвечает правильно, даже если никто не знает, какой именно. Однако ни один из алгоритмов не решает проблему остановки в целом.
Существуют программы ( интерпретаторы ), которые имитируют выполнение любого исходного кода, который им предоставлен. Такие программы могут продемонстрировать, что программа действительно останавливается, если это так: интерпретатор сам в конечном итоге остановит свою симуляцию, что показывает, что исходная программа остановлена. Однако интерпретатор не остановится, если его программа ввода не остановится, поэтому этот подход не может решить указанную проблему остановки; он не дает успешного ответа «не останавливается» для программ, которые не останавливаются.
Проблема остановки теоретически разрешима для линейных ограниченных автоматов (LBA) или детерминированных машин с конечной памятью. Машина с ограниченной памятью имеет конечное число конфигураций, и поэтому любая детерминированная программа на ней в конечном итоге должна либо остановить, либо повторить предыдущую конфигурацию: [4]
... любая машина с конечным числом состояний, если ее полностью предоставить самой себе, в конечном итоге превратится в идеально периодически повторяющуюся структуру . Продолжительность этого повторяющегося шаблона не может превышать количество внутренних состояний машины...
Однако компьютер с миллионом мелких деталей, каждая из которых имеет два состояния, будет иметь как минимум 2 1,000,000 возможные состояния: [5]
Это единица, за которой следует примерно триста тысяч нулей... Даже если бы такая машина работала на частотах космических лучей, эоны галактической эволюции были бы ничем по сравнению со временем путешествия по такому циклу:
Хотя машина может быть конечной, а конечные автоматы «имеют ряд теоретических ограничений»: [5]
... задействованные величины должны привести к подозрению, что теоремы и аргументы, основанные главным образом на простой конечности [] диаграммы состояний, могут не иметь большого значения.
Также можно автоматически решить, остановится ли недетерминированная машина с конечной памятью ни на одной, ни на некоторых, ни на всех возможных последовательностях недетерминированных решений, путем перечисления состояний после каждого возможного решения.
История
[ редактировать ]В апреле 1936 года Алонсо Чёрч опубликовал своё доказательство неразрешимости проблемы лямбда -исчисления . Доказательство Тьюринга было опубликовано позже, в январе 1937 года. С тех пор было описано множество других неразрешимых проблем, включая проблему остановки, возникшую в 1950-х годах.
Хронология
[ редактировать ]- 1900 Давид Гильберт ставит свои «23 вопроса» (теперь известные как проблемы Гильберта ) на Втором Международном конгрессе математиков в Париже. «Из них вторым было доказательство непротиворечивости « аксиом Пеано », от которых, как он показал, зависела строгость математики». : [6]
- 1920 Эмиль Пост исследует проблему остановки систем тегов , рассматривая ее как кандидата на неразрешимость. [7] Ее неразрешимость была установлена гораздо позже Марвином Мински . [8] — 1921 :
- 1928 Гильберт переформулирует свою «Вторую проблему» на Болонском международном конгрессе. [9] Он поставил три вопроса: например, № 1: Была ли математика полной ? №2: Была ли математика последовательной ? №3: Была ли математика разрешима ? [10] Третий вопрос известен как Entscheidungsproblem (проблема принятия решения). [11] :
- 1930 Курт Гёдель объявляет доказательство как ответ на первые два вопроса Гильберта 1928 года. [12] «Сначала он [Гильберт] был только зол и разочарован, но затем начал пытаться конструктивно решить проблему... Сам Гёдель чувствовал — и выразил эту мысль в своей статье — что его работа не противоречит формалистической точке зрения Гильберта о вид" : [13]
- 1931 Гёдель публикует «О формально неразрешимых положениях Principia Mathematica и родственных систем I». : [14]
- 19 апреля 1935 г. Алонсо Чёрч публикует «Неразрешимую проблему элементарной теории чисел», в которой предлагается, что интуитивное понятие эффективно вычислимой функции может быть формализовано с помощью общерекурсивных функций или, что то же самое, с помощью лямбда-определяемых функций. функции . Он доказывает, что проблема остановки лямбда-исчисления (т. е. имеет ли данное лямбда-выражение нормальную форму ) не поддается эффективному вычислению. : [15]
- 1936 Чёрч публикует первое доказательство неразрешимости проблемы Entscheidungsproblem , используя понятие вычислений с помощью рекурсивных функций . : [16]
- 7 октября 1936 г. Эмиля Поста Получена статья «Конечные комбинаторные процессы. Формула I». Пост добавляет к своему «процессу» инструкцию «(С) Стоп». Он назвал такой процесс «типом 1… если определяемый им процесс завершается для каждой конкретной проблемы». : [17]
- Май 1936 Алана Тьюринга статья « О вычислимых числах с применением к проблеме Entscheidungs» выходит в печать в мае 1936 года и выходит в печать в январе 1937 года. [18] Тьюринг доказывает три неразрешимые проблемы: проблему «удовлетворения», проблему «печати» и проблему Entscheidungsproblem . [19] Доказательство Тьюринга отличается от доказательства Чёрча введением понятия машинных вычислений. Это один из «первых примеров, когда проблемы принятия решений оказались неразрешимыми». [20] [ нужна страница ] – январь 1937 :
- 1939 Дж. Баркли Россер отмечает существенную эквивалентность «эффективного метода», определенного Гёделем, Чёрчем и Тьюрингом. : [21]
- 1943 В статье Стивен Клини утверждает, что «при создании полной алгоритмической теории мы описываем процедуру... которая обязательно завершается и таким образом, что по результату мы можем прочитать определенный ответ». , «Да» или «Нет» на вопрос «Истинно ли значение предиката?»». :
- 1952 Клини включает обсуждение неразрешимости проблемы остановки для машин Тьюринга и переформулирует ее в терминах машин, которые «в конечном итоге останавливаются», то есть останавливаются: «...не существует алгоритма для определения того, является ли какая-либо данная машина когда он начинается в любой конкретной ситуации, в конечном итоге останавливается ». : [22]
- 1952 Мартин Дэвис использует термин «проблема остановки» в серии лекций в Лаборатории систем управления Университета Иллинойса в 1952 году. Вполне вероятно, что это первое подобное использование этого термина. : [23]
Происхождение проблемы остановки
[ редактировать ]Во многих статьях и учебниках определение и доказательство неразрешимости проблемы остановки отсылаются к статье Тьюринга 1936 года. Однако это неверно. [19] [24] Тьюринг не использовал термины «остановка» или «остановка» ни в одной из своих опубликованных работ, включая статью 1936 года. [25] Поиск академической литературы с 1936 по 1958 год показал, что первым опубликованным материалом, в котором использовался термин «проблема остановки», был Роджерс (1957) . Однако Роджерс говорит, что у него был в распоряжении черновик Дэвиса (1958) : [19] и Мартин Дэвис во введении заявляет, что «эксперт, возможно, найдет некоторую новизну в расположении и рассмотрении тем», [26] поэтому эту терминологию следует отнести к Дэвису. [19] [24] Дэвис заявил в письме, что говорил о проблеме остановки с 1952 года. [23] В книге Дэвиса используется следующее: [27]
«[...] мы хотим определить, остановится ли в конечном итоге [машина Тьюринга] Z, если ее поместить в заданное начальное состояние. Мы называем эту проблему проблемой остановки для Z. [...]
Теорема 2.2. Существует машина Тьюринга, проблема остановки которой рекурсивно неразрешима .
Связанной с этим проблемой является задача печати простой машины Тьюринга Z относительно символа S i ".
Возможным предшественником формулировки Дэвиса является заявление Клини 1952 года, которое отличается только формулировкой: [19] [22]
не существует алгоритма, позволяющего решить, остановится ли в конечном итоге какая-либо данная машина при запуске из той или иной ситуации.
Проблема остановки по Тьюрингу эквивалентна как проблеме печати Дэвиса («печатает ли машина Тьюринга, начиная с заданного состояния, когда-либо заданный символ?»), так и проблеме печати, рассмотренной в статье Тьюринга 1936 года («может ли машина Тьюринга начинать с чистого листа?»). лента когда-нибудь печатала данный символ?»). Однако эквивалентность Тьюринга довольно неопределенна и не означает, что эти две проблемы одинаковы. Есть машины, которые печатают, но не останавливаются, и останавливаются, но не печатают. Проблемы печати и остановки касаются разных проблем и демонстрируют важные концептуальные и технические различия. Таким образом, Дэвис просто проявил скромность, когда сказал: [19]
Можно также отметить, что неразрешимость этих задач по существу впервые была получена Тьюрингом.
Формализация
[ редактировать ]В своем первоначальном доказательстве Тьюринг формализовал концепцию алгоритма , введя машины Тьюринга . Однако результат никоим образом не является специфичным для них; это в равной степени применимо к любой другой модели вычислений , эквивалентной по своей вычислительной мощности машинам Тьюринга, таким как алгоритмы Маркова , лямбда-исчисление , почтовые системы , регистровые машины или системы тегов .
Важно то, что формализация позволяет напрямую сопоставить алгоритмы с некоторым типом данных , с которыми алгоритм может работать. Например, если формализм позволяет алгоритмам определять функции над строками (например, машины Тьюринга), тогда должно быть отображение этих алгоритмов в строки, а если формализм позволяет алгоритмам определять функции над натуральными числами (например, вычислимые функции ), тогда должно быть быть отображением алгоритмов на натуральные числа. Сопоставление со строками обычно является наиболее простым, но строки в алфавите с n символами также можно сопоставить с числами, интерпретируя их как числа в n -арной системе счисления .
Представление в виде набора
[ редактировать ]Традиционное представление задач решения представляет собой набор объектов, обладающих рассматриваемым свойством. Остановочный набор
- K знак равно {( я , Икс ) | программа i останавливается при запуске на входе x }
представляет собой проблему остановки.
Этот набор является рекурсивно перечислимым , что означает, что существует вычислимая функция, которая перечисляет все содержащиеся в нем пары ( i , x ). Однако дополнение этого множества не является рекурсивно перечислимым. [28]
Существует множество эквивалентных формулировок проблемы остановки; такой формулировкой является любое множество, степень Тьюринга которого равна степени проблемы остановки. Примеры таких наборов включают в себя:
- { я | программа i в конечном итоге останавливается при запуске с вводом 0}
- { я | существует ввод x такой, что программа i в конечном итоге останавливается при запуске с вводом x }.
Концепция доказательства
[ редактировать ]Кристофер Стрейчи предложил доказательство от противного , что проблема остановки неразрешима. [29] [30] Доказательство проводится следующим образом: предположим, что существует полностью вычислимая функцияhalts (f) , которая возвращает true, если подпрограмма f останавливается (при запуске без входных данных), и возвращает false в противном случае. Теперь рассмотрим следующую подпрограмму:
def g():
if halts(g):
loop_forever()
Остановки(g) должны возвращать либо true, либо false, поскольку останавливает предполагается, что значение total . Если приостановка(g) возвращает true, то g вызовет цикл_forever и никогда не остановится, что является противоречием. Еслиhalts (g) возвращает false, то g остановится, потому что он не будет вызывать цикл_forever ; это тоже противоречие. В целом, g делает противоположное тому, что, останавливающего действия, по словам g должен делать , поэтому приостановка(g) не может возвращать значение истинности, согласующееся с тем, останавливается ли g . Следовательно, первоначальное предположение о том, что остановка является полностью вычислимой функцией, должно быть ложным.
Эскиз строгого доказательства
[ редактировать ]Приведенная выше концепция показывает общий метод доказательства, но вычислимая функция останавливается не принимает подпрограмму напрямую в качестве аргумента; вместо этого он принимает исходный код программы. Более того, определение g является самореферентным . Строгое доказательство решает эти проблемы. Общая цель — показать, что не существует полностью вычислимой функции , которая решает, остановится ли произвольная программа i на произвольном вводе x ; то есть следующая функция h (для «остановок») невычислима: [31]
Здесь программа i относится к i- й программе в перечислении всех программ фиксированной Тьюринг-полной модели вычислений.
е ( я , j ) | я | ||||||
1 | 2 | 3 | 4 | 5 | 6 | ||
дж | 1 | 1 | 0 | 0 | 1 | 0 | 1 |
2 | 0 | 0 | 0 | 1 | 0 | 0 | |
3 | 0 | 1 | 0 | 1 | 0 | 1 | |
4 | 1 | 0 | 0 | 1 | 0 | 0 | |
5 | 0 | 0 | 0 | 1 | 1 | 1 | |
6 | 1 | 1 | 0 | 0 | 1 | 0 | |
ж ( я , я ) | 1 | 0 | 0 | 1 | 1 | 0 | |
г ( я ) | В | 0 | 0 | В | В | 0 |
Возможные значения полной вычислимой функции f, расположенной в двумерном массиве. Оранжевые клетки — это диагональ. Значения f ( i , i ) и g ( i ) показаны внизу; U указывает, что функция g не определена для конкретного входного значения.
Доказательство продолжается путем непосредственного установления того, что никакая полная вычислимая функция с двумя аргументами не может быть требуемой функцией h . Как и в наброске концепции, для любой полностью вычислимой двоичной функции f следующая частичная функция g также вычислима некоторой программой e :
Проверка того, что g вычислима, опирается на следующие конструкции (или их эквиваленты):
- вычислимые подпрограммы (программа, которая вычисляет f, является подпрограммой в программе e ),
- дублирование значений (программа e вычисляет входные данные i , i для f из входных данных i для g ),
- условное ветвление (программа e выбирает между двумя результатами в зависимости от значения, которое она вычисляет для f ( i , i )),
- не дает определенного результата (например, путем бесконечного цикла),
- возвращает значение 0.
Следующий псевдокод для e иллюстрирует простой способ вычисления g :
procedure e(i):
if f(i, i) == 0 then
return 0
else
loop forever
Поскольку g частично вычислима, должна существовать программа e , которая вычисляет g , исходя из предположения, что модель вычислений является полной по Тьюрингу. Эта программа является одной из всех программ, в которых функция остановки h определена . Следующий шаг доказательства показывает, что h ( e , e ) не будет иметь то же значение, что и f ( e , e ).
Из определения g следует , что должен выполняться ровно один из следующих двух случаев:
- f ( e , e ) = 0 и, следовательно, g ( e ) = 0. В этом случае программа e останавливается на вводе e , поэтому h ( e , e ) = 1.
- f ( e , e ) ≠ 0, поэтому g ( e ) не определен. В этом случае программа e не останавливается на вводе e , поэтому h ( e , e ) = 0.
В любом случае f не может быть той же функцией, что и h . Поскольку f была произвольной полностью вычислимой функцией с двумя аргументами, все такие функции должны отличаться от h .
Это доказательство аналогично диагональному аргументу Кантора . Можно визуализировать двумерный массив с одним столбцом и одной строкой для каждого натурального числа, как указано в таблице выше. Значение f ( i , j ) помещается в столбец i , строка j . Поскольку предполагается, что f — полная вычислимая функция, любой элемент массива можно вычислить с помощью f . Построение функции g можно наглядно представить с помощью главной диагонали этого массива. Если массив имеет 0 в позиции ( i , i ), то g ( i ) равен 0. В противном случае g ( i ) не определен. Противоречие возникает из-за того, что существует некоторый столбец e массива, соответствующий самому g . Теперь предположим, что f была функцией остановки h , если g ( e ) определена ( g ( e в данном случае ) = 0), g ( e ) останавливается, поэтому f ( e,e ) = 1. Но g ( e ) = 0 только тогда, когда f ( e,e ) = 0, что противоречит f ( e,e ) = 1. Аналогично, если g ( e ) не определен, то функция остановки f ( e,e ) = 0, что приводит к g ( e ) = 0 по конструкции g . Это противоречит предположению о том, что g ( e ) не определен. В обоих случаях возникает противоречие. Поэтому любая произвольная вычислимая функция f не может быть функцией остановки h .
Теория вычислимости
[ редактировать ]Типичный метод доказательства проблемы быть неразрешимым — значит свести проблему остановки к . Например, не может быть общего алгоритма, который решает, является ли данное утверждение о натуральных числах истинным или ложным. Причина этого в том, что утверждение о том, что определенная программа остановится при определенных входных данных, может быть преобразовано в эквивалентное утверждение о натуральных числах. Если бы алгоритм мог найти истинностное значение каждого утверждения о натуральных числах, он наверняка смог бы найти истинностное значение этого утверждения; но это определит, остановится ли исходная программа.
Теорема Райса обобщает теорему о неразрешимости проблемы остановки. В нем говорится, что для любого нетривиального свойства не существует общей процедуры принятия решения, которая для всех программ определяет, обладает ли частичная функция, реализованная входной программой, этим свойством. (Частичная функция — это функция, которая не всегда может выдавать результат, поэтому она используется для моделирования программ, которые могут либо выдавать результаты, либо не останавливаться.) Например, свойство «остановка для ввода 0» неразрешимо. Здесь «нетривиальный» означает, что набор частичных функций, удовлетворяющих этому свойству, не является ни пустым набором, ни набором всех частичных функций. Например, утверждение «останавливается или не может остановиться на входе 0» очевидно верно для всех частичных функций, поэтому это тривиальное свойство, и его можно определить с помощью алгоритма, который просто сообщает «истина». Кроме того, эта теорема справедлива только для свойств частичной функции, реализуемой программой; Теорема Райса не применима к свойствам самой программы. Например, «остановка на входе 0 в пределах 100 шагов» — это Это не свойство частичной функции, реализуемой программой, — это свойство программы, реализующей частичную функцию, и оно вполне разрешимо.
Грегори Чайтин определил вероятность остановки , представленную символом Ω , типом действительного числа, которое, как неофициально считается, представляет вероятность остановки случайно созданной программы. Эти числа имеют ту же степень Тьюринга, что и проблема остановки. Это нормальное и трансцендентное число , которое можно определить , но невозможно полностью вычислить . Это означает, что можно доказать, что не существует алгоритма , который вычисляет цифры Ω, хотя в простых случаях его первые несколько цифр можно вычислить.
Поскольку отрицательный ответ на проблему остановки показывает, что существуют проблемы, которые не могут быть решены с помощью машины Тьюринга, тезис Чёрча-Тьюринга ограничивает возможности любой машины, реализующей эффективные методы . Однако не все машины, мыслимые человеческим воображением, подчиняются тезису Чёрча-Тьюринга (например, машины-оракулы ). Остается открытым вопрос, могут ли существовать реальные детерминированные физические процессы , которые в долгосрочной перспективе ускользнут от моделирования с помощью машины Тьюринга, и, в частности, можно ли с пользой использовать любой такой гипотетический процесс в форме вычислительной машины (гиперкомпьютера ) . это могло бы, среди прочего, решить проблему остановки машины Тьюринга. Также остается открытым вопрос, участвуют ли какие-либо подобные неизвестные физические процессы в работе человеческого мозга и могут ли люди решить проблему остановки. [32]
Приближения
[ редактировать ]Доказательство Тьюринга показывает, что не может быть механического общего метода (т. е. машины Тьюринга или программы в какой-либо эквивалентной модели вычислений ), позволяющей определить, останавливаются ли алгоритмы. Однако каждый отдельный случай проблемы остановки имеет окончательный ответ, который может быть или не быть практически вычислимым. Учитывая конкретный алгоритм и входные данные, часто можно показать, что он останавливается или не останавливается, и на самом деле ученые-компьютерщики часто делают именно это как часть доказательства правильности . Существуют некоторые эвристики , которые можно использовать в автоматическом режиме, чтобы попытаться построить доказательство, которое часто оказывается успешным в типичных программах. Эта область исследований известна как автоматический анализ завершения .
Были получены некоторые результаты по теоретической эффективности эвристики проблем остановки, в частности, по доле программ заданного размера, которые могут быть правильно классифицированы с помощью рекурсивного алгоритма. Эти результаты не дают точных цифр, поскольку дроби невычислимы, а также сильно зависят от выбора программной кодировки, используемой для определения «размера». Например, рассмотрите возможность классификации программ по количеству состояний и использования конкретной модели вычислений «полубесконечная лента Тьюринга», которая выдает ошибку (без остановки), если программа выходит за пределы левой стороны ленты. Затем , над программами выбираются равномерно по числу штатов. Но этот результат в некотором смысле «тривиален», потому что эти разрешимые программы — это просто те, которые слетают с ленты, а эвристика заключается в том, чтобы просто предсказать, что работа не остановится из-за ошибки. Таким образом, кажущаяся несущественной деталь, а именно обработка программ с ошибками, может оказаться решающим фактором при определении доли программ. [33]
Чтобы избежать этих проблем, было разработано несколько ограниченных понятий «размера» программы. Плотная гёделева нумерация присваивает программам такие номера, что каждая вычислимая функция встречается в положительной дроби в каждой последовательности индексов от 1 до n, т. е. гёделизация φ плотна тогда и только тогда, когда для всех , существует такой, что . Например, нумерация, присваивающая индексы для нетривиальных программ и всех других индексов состояние ошибки не является плотным, но существует плотная гёделева нумерация синтаксически правильных программ Brainfuck . [34] Плотная гёделева нумерация называется оптимальной, если для любой другой гёделевой нумерации , существует тотально рекурсивная функция 1-1 и константа такой, что для всех , и . Это условие гарантирует, что все программы будут иметь индексы, не намного превышающие их индексы в любой другой нумерации Гёделя. Оптимальные нумерации Гёделя строятся путем нумерации входов универсальной машины Тьюринга . [35] Третье понятие размера использует универсальные машины, работающие с двоичными строками, и измеряет длину строки, необходимую для описания входной программы. Универсальная машина U — это машина, для которой для любой другой машины V существует полная вычислимая функция h такая, что . Оптимальная машина — это универсальная машина, которая достигает границы инвариантности сложности Колмогорова , т.е. для каждой машины V существует c такой, что для всех выходов x , если V -программа длины n выводит x , то существует U -программа максимальная длина вывод х . [36]
Рассмотрим частично вычислимые функции (алгоритмы) . Для каждого мы рассматриваем дробь ошибок среди всех программ с метрикой размера не более , считая каждую программу для чего не завершается, выдает ответ «не знаю» или выдает неправильный ответ, т.е. останавливается и результаты DOES_NOT_HALT
, или не останавливается и результаты HALTS
. Поведение можно описать следующим образом для плотных гёделизаций и оптимальных машин: [34] [36]
- Для каждого алгоритма , . Другими словами, любой алгоритм имеет положительную минимальную частоту ошибок, даже если размер задачи становится чрезвычайно большим.
- Существует такая, что для любого алгоритма , . Другими словами, существует положительная частота ошибок, при которой любой алгоритм сколь угодно часто будет работать хуже, чем эта частота ошибок, даже если размер проблемы растет бесконечно.
- . Другими словами, существует последовательность алгоритмов, в которой частота ошибок становится сколь угодно близкой к нулю для определенной последовательности возрастающих размеров. Однако этот результат позволяет использовать последовательности алгоритмов, которые дают неправильные ответы.
- Если рассматривать только «честные» алгоритмы, которые могут быть неопределенными, но никогда не дают неправильных ответов, то в зависимости от метрики может быть равно 0, а может и не быть. В частности, для универсальных машин с левым итогом оно равно 0, но для эффективно оптимальных машин оно больше 0. [36]
Сложный характер этих границ обусловлен колебательным поведением . Нечасто встречаются новые разновидности программ, состоящие из сколь угодно больших «блоков» и постоянно растущей доли повторов. Если блоки новых сортов включены полностью, то частота ошибок будет не менее , но между блоками доля правильно классифицированных повторов может быть сколь угодно высокой. В частности, эвристика «подсчета», которая просто запоминает первые N входных данных и распознает их эквиваленты, позволяет бесконечно часто достигать сколь угодно низкой частоты ошибок. [34]
Теоремы Гёделя о неполноте
[ редактировать ]Этот раздел нуждается в дополнительных цитатах для проверки . ( Август 2019 г. ) |
Идеи, возникающие в теоремах Гёделя о неполноте, очень похожи на концепции, возникающие в проблеме остановки, и доказательства очень похожи. Фактически, более слабая форма Первой теоремы о неполноте является простым следствием неразрешимости проблемы остановки. Эта более слабая форма отличается от стандартной формулировки теоремы о неполноте тем, что утверждает, что аксиоматизация натуральных чисел, которая является одновременно полной и правильной, невозможна. «Звуковая» часть является ослабляющей: она означает, что мы требуем от рассматриваемой аксиоматической системы доказательства только истинных утверждений о натуральных числах. Поскольку надежность подразумевает последовательность , эту более слабую форму можно рассматривать как следствие сильной формы. Важно отметить, что утверждение стандартной формы Первой теоремы Гёделя о неполноте совершенно не касается истинности утверждения, а касается только вопроса о том, можно ли найти его с помощью математического доказательства .
Более слабая форма теоремы может быть доказана из неразрешимости проблемы остановки следующим образом. [37] Предположим, что у нас есть обоснованная (и, следовательно, непротиворечивая) и полная аксиоматизация всех истинных логических утверждений первого порядка о натуральных числах . Затем мы можем построить алгоритм, который перечисляет все эти утверждения. Это означает, что существует алгоритм N ( n ), который по натуральному числу n вычисляет истинное логическое утверждение первого порядка о натуральных числах, и что для всех истинных утверждений существует хотя бы одно n такое, что N ( n ) дает это утверждение. Теперь предположим, что мы хотим решить, остановится ли алгоритм с представлением a на входе i . Мы знаем, что это утверждение можно выразить с помощью логического утверждения первого порядка, скажем, H ( a , i ). Поскольку аксиоматизация завершена, отсюда следует, что либо существует n такое, что N ( n ) = H ( a , i ), либо существует n ′ такое, что N ( n ′ ) = ¬ H ( a , i ). Таким образом, если мы будем перебирать все n, пока не найдем H ( a , i ) или его отрицание, мы всегда остановимся, и, более того, ответ, который он нам даст, будет истинным (по обоснованности). Это означает, что это дает нам алгоритм для решения проблемы остановки. Поскольку мы знаем, что такого алгоритма не может быть, из этого следует, что предположение о том, что существует непротиворечивая и полная аксиоматизация всех истинных логических утверждений первого порядка о натуральных числах, должно быть ложным.
Обобщение
[ редактировать ]Многие варианты проблемы остановки можно найти в учебниках по вычислимости. [38] Обычно эти задачи являются RE-полными и описывают наборы сложности. в арифметической иерархии то же, что и стандартная задача остановки. Таким образом, варианты неразрешимы, и стандартная проблема остановки сводится к каждому варианту и наоборот. Однако некоторые варианты имеют более высокую степень неразрешимости и не могут быть сведены к стандартной задаче об остановке. Следующие два примера являются общими.
Остановка на всех входах
[ редактировать ]Универсальная проблема остановки , также известная (в теории рекурсии ) как тотальность , представляет собой проблему определения того, остановится ли данная компьютерная программа для каждого ввода (название тотальность происходит от эквивалентного вопроса о том, является ли вычисленная функция полной ). Эта проблема не только неразрешима, как и проблема остановки, но и в высшей степени неразрешима. С точки зрения арифметической иерархии это -полный. [39]
невозможно решить даже с помощью оракула Это означает, в частности, что проблему остановки .
Распознавание частичных решений
[ редактировать ]Существует множество программ, которые для некоторых входных данных возвращают правильный ответ на задачу остановки, а для других входных данных они вообще не возвращают ответ. Однако проблема «данная программа p является ли она решателем частичной остановки» (в описанном смысле) по крайней мере так же сложна, как и проблема остановки. Чтобы убедиться в этом, предположим, что для этого существует алгоритм PHSR («распознаватель частично останавливающегося решателя»). Затем его можно использовать для решения проблемы остановки, следующее: Чтобы проверить, останавливается ли входная программа x на y , создайте программу p, которая на входе ( x , y ) сообщает true и расходится на всех остальных входах. Затем проверьте p с помощью PHSR.
Приведенный выше аргумент представляет собой сведение проблемы остановки к распознаванию PHS, и таким же образом более сложные проблемы, такие как остановка на всех входах, также могут быть уменьшены, подразумевая, что распознавание PHS не только неразрешимо, но и находится выше в арифметической иерархии , в частности -полный.
Вычисления с потерями
[ редактировать ]Машина Тьюринга с потерями — это машина Тьюринга, в которой часть ленты может недетерминированно исчезнуть. Проблема остановки разрешима для машины Тьюринга с потерями, но не примитивно рекурсивной . [40]
машины Oracle
[ редактировать ]Машина с оракулом для решения проблемы остановки может определить, остановятся ли конкретные машины Тьюринга на определенных входных данных, но они не могут определить в целом, остановятся ли эквивалентные им машины.
См. также
[ редактировать ]- Занятой бобер
- Теорема Гёделя о неполноте
- Споры Брауэра и Гильберта
- Колмогоровская сложность
- Проблема P и NP
- Анализ завершения
- Наихудшее время выполнения
Примечания
[ редактировать ]- ^ МакКоннелл, Стив (2004). Код завершен (2-е изд.). Пирсон Образование. п. 374. ИСБН 9780735636972 .
- ^ Хуан, Хан-Вэй (2009). HCS12/9S12: Введение в интерфейс программного и аппаратного обеспечения . п. 197.
... если программа застревает в определенном цикле, ... выясните, в чем дело.
- ^ Саймон, Дэвид Э. (1999). Учебник по встроенному программному обеспечению . п. 253.
Поэтому для систем жесткого реального времени важно писать подпрограммы, которые всегда выполняются за одно и то же время или имеют четко идентифицируемый худший случай.
- ^ Минский 1967 , с. 24. курсив в оригинале
- ^ Jump up to: а б Минский 1967 , с. 25.
- ^ Ходжес 1983 , с. 83; Комментарий Дэвиса в Davis 1965 , с. 108
- ^ Абсолютно неразрешимые проблемы и относительно неразрешимые предложения - отчет об ожидании , перепечатано в Дэвисе 1965 , стр. 340–433.
- ^ Минский 1967 .
- ^ Рид 1996 , стр. 188–189.
- ^ Ходжес 1983 , с. 91.
- ^ Ходжес 1983 , с. 91; Пенроуз 1989 , с. 34.
- ^ Рид 1996 , с. 198.
- ^ Рид 1996 , с. 199.
- ^ перепечатано в Дэвисе 1965 , с. 5 и далее
- ^ Церковь 1936 .
- ^ Заметка о проблеме Entscheidungs , перепечатано в Дэвисе 1965 , с. 110
- ^ Дэвис 1965 , с. 289 и далее.
- ^ перепечатано в Дэвисе 1965 , с. 115
- ^ Jump up to: а б с д и ж Лукас 2021 .
- ^ Клини 1952 .
- ^ Россер, «Неофициальное изложение доказательств теоремы Гёделя и теоремы Чёрча», перепечатано в Дэвисе 1965 , стр. 223
- ^ Jump up to: а б Клини 1952 , с. 382.
- ^ Jump up to: а б письмо Дэвиса Коупленду от 12 декабря 2001 г., сноска 61 в Copeland 2004 , стр. 40
- ^ Jump up to: а б Коупленд 2004 , с. 40.
- ^ Текстовый поиск в собрании сочинений Тьюринга: Good (1992) , Gandy & Yates (2001) , Ince (1992) , Saunders (1992) . Точно так же Ходжес (1983) не использует в своем указателе слово «остановка» или слова «проблема остановки».
- ^ Дэвис 1958 , с. vii-viii.
- ^ Дэвис 1958 , стр. 70–71.
- ^ Мур и Мертенс 2011 , стр. 236–237.
- ^ Стрейчи, К. (1 января 1965 г.). «Невозможная программа» . Компьютерный журнал . 7 (4): 313. дои : 10.1093/comjnl/7.4.313 .
- ^ Дневной свет, Эдгар Г. (16 апреля 2021 г.). «Проблема остановки и языковой подход к безопасности: похвала и критика со стороны технического историка» (PDF) . Вычислимость . 10 (2): 141–158. дои : 10.3233/COM-180217 . S2CID 233329507 . Проверено 26 августа 2021 г.
- ^ Пенроуз 1989 , стр. 57–63.
- ^ Коупленд 2004 , с. 15.
- ^ Хэмкинс, Джоэл Дэвид; Мясников, Алексей (1 октября 2006 г.). «Проблема остановки разрешима на множестве асимптотической вероятности один» (PDF) . Журнал формальной логики Нотр-Дама . 47 (4). дои : 10.1305/ndjfl/1168352664 . S2CID 15005164 . Проверено 5 ноября 2022 г.
- ^ Jump up to: а б с Кёлер, Свен; Шиндельхауэр, Кристиан; Зиглер, Мартин (2005). «О приближении реальных проблем остановки» . Основы теории вычислений . Конспекты лекций по информатике. Том. 3623. стр. 454–466. дои : 10.1007/11537311_40 . ISBN 978-3-540-28193-1 .
- ^ Линч, Нэнси (октябрь 1974 г.). «Приближения к проблеме остановки» (PDF) . Журнал компьютерных и системных наук . 9 (2): 143–150. дои : 10.1016/S0022-0000(74)80003-6 .
- ^ Jump up to: а б с Бьенвеню, Лоран; Дефонтен, Дэмиен; Шен, Александр (5 апреля 2016 г.). «Общие алгоритмы решения проблемы остановки и новый взгляд на оптимальные машины». Логические методы в информатике . 12 (2): 1. arXiv : 1505.00731 . дои : 10.2168/LMCS-12(2:1)2016 . S2CID 14763862 .
- ^ Ааронсон, Скотт (21 июля 2011 г.). «Теорема Россера через машины Тьюринга» . Shtetl-Оптимизированный . Проверено 2 ноября 2022 г.
- ^ например, Сипсер 2006 , Дэвис 1958 , Мински 1967 , Хопкрофт и Ульман 1979 , Бёргер 1989.
- ^ Бёргер 1989 , с. 121.
- ^ Абдулла и Йонссон 1996 , стр. 92.
Ссылки
[ редактировать ]- Черч, Алонсо (1936). «Неразрешимая проблема элементарной теории чисел». Американский журнал математики . 58 (2): 345–363. дои : 10.2307/2371045 . JSTOR 2371045 .
- Коупленд, Б. Джек, изд. (2004). Главное Тьюринга: плодотворные работы по информатике, логике, философии, искусственному интеллекту и искусственной жизни, а также секреты «Энигмы» . Оксфорд: Кларендон Пресс. ISBN 0-19-825079-7 .
- Дэвис, Мартин (1965). Неразрешимые, основные статьи о неразрешимых предложениях, неразрешимых проблемах и вычислимых функциях . Нью-Йорк: Рэйвен Пресс. . Статья Тьюринга занимает третье место в этом томе. В число статей входят работы Гёделя, Чёрча, Россера, Клини и Поста.
- Дэвис, Мартин (1958). Вычислимость и неразрешимость . Нью-Йорк: МакГроу-Хилл. .
- Роджерс, Хартли (младший) (1957). Теория рекурсивных функций и эффективная вычислимость . Массачусетский технологический институт.
- Клини, Стивен Коул (1952). Введение в метаматематику . Северная Голландия. ISBN 0923891579 . . Глава XIII («Вычислимые функции») включает обсуждение неразрешимости проблемы остановки для машин Тьюринга. Отходя от терминологии Тьюринга о неостановящихся машинах без кругов, Клини вместо этого обращается к машинам, которые «останавливаются», то есть останавливаются.
- Лукас, Сальвадор (июнь 2021 г.). «Истоки проблемы остановки». Журнал логических и алгебраических методов программирования . 121 : 100687. doi : 10.1016/j.jlamp.2021.100687 . hdl : 10251/189460 . S2CID 235396831 .
- Мински, Марвин (1967). Вычисления: конечные и бесконечные машины . Энглвуд Клиффс, Нью-Джерси: Прентис-Холл. ISBN 0131655639 . . См. главу 8, раздел 8.2 «Неразрешимость проблемы остановки».
- Мур, Кристофер ; Мертенс, Стефан (2011). Природа вычислений . Издательство Оксфордского университета. doi : 10.1093/acprof:oso/9780199233212.001.0001 . ISBN 978-0-19-923321-2 .
- Рид, Констанс (1996). Гильберт . Нью-Йорк: Коперник. ISBN 0387946748 . . Впервые опубликованная в 1970 году, это увлекательная история немецкой математики и физики с 1880-х по 1930-е годы. На его страницах появляются сотни имен, знакомых математикам, физикам и инженерам. Возможно, она омрачена отсутствием явных ссылок и небольшим количеством сносок: Рид утверждает, что ее источниками были многочисленные интервью с теми, кто лично знал Гильберта, а также письма и документы Гильберта.
- Сипсер, Майкл (2006). «Раздел 4.2: Проблема остановки» . Введение в теорию вычислений (второе изд.). Издательство ПВС. стр. 173–182 . ISBN 0-534-94728-Х .
- Тьюринг, AM (1937). «О вычислимых числах с применением к проблеме Entscheidungs» . Труды Лондонского математического общества . с2-42(1). Уайли: 230–265. дои : 10.1112/plms/s2-42.1.230 . ISSN 0024-6115 . S2CID 73712 . [ постоянная мертвая ссылка ] , Тьюринг, AM (1938). «О вычислимых числах с применением к проблеме Entscheidungs. Исправление» . Труды Лондонского математического общества . с2-43(1). Уайли: 544–546. дои : 10.1112/plms/s2-43.6.544 . ISSN 0024-6115 . [ постоянная мертвая ссылка ] Это эпохальная статья, в которой Тьюринг определяет машины Тьюринга , формулирует проблему остановки и показывает, что она (как и проблема Entscheidungsproblem ) неразрешима.
- Пенроуз, Роджер (1989). Новый разум императора: о компьютерах, разуме и законах физики (исправленное переиздание 1990 г.). Оксфорд: Издательство Оксфордского университета. ISBN 0192861980 . . См. Глава 2 «Алгоритмы и машины Тьюринга». Чрезмерно сложное изложение (более лучшую модель см. в статье Дэвиса), но подробное изложение машин Тьюринга и проблемы остановки, а также лямбда-исчисления Чёрча.
- Хопкрофт, Джон Э .; Уллман, Джеффри Д. (1979). Введение в теорию автоматов, языки и вычисления (1-е изд.). Аддисон-Уэсли. ISBN 81-7808-347-7 . . См. главу 7 «Машины Тьюринга». Книга посвящена машинной интерпретации «языков», NP-полноте и т. д.
- Ходжес, Эндрю (1983). Алан Тьюринг: загадка . Нью-Йорк: Саймон и Шустер. ISBN 0-671-49207-1 . . См. Глава «Дух истины» содержит историю, ведущую к его доказательству, и обсуждение его.
- Бёргер, Эгон (1989). Вычислимость, сложность, логика . Амстердам: Северная Голландия. ISBN 008088704X .
- Абдулла, Парош Азиз; Йонссон, Бенгт (1996). «Проверка программ с ненадежными каналами» . Информация и вычисления . 127 (2): 91–101. дои : 10.1006/inco.1996.0053 .
- Собрание сочинений А. М. Тьюринга.
- Хорошо, Ирвинг Джон, изд. (1992). Чистая математика . Северная Голландия. ISBN 978-0-444-88059-8 .
- Ганди, РОД; Йейтс, CEM, ред. (5 декабря 2001 г.). Математическая логика . Эльзевир. ISBN 978-0-08-053592-0 .
- Инс, округ Колумбия, изд. (1992). Механический интеллект . Северная Голландия. ISBN 978-0-444-88058-1 .
- Сондерс, PT, изд. (26 ноября 1992 г.). Морфогенез . Эльзевир. ISBN 978-0-08-093405-1 .
Дальнейшее чтение
[ редактировать ]- c2: Проблема с остановкой
- Альфред Норт Уайтхед и Бертран Рассел , Principia Mathematica — *56, Кембридж в University Press, 1962. Касательно проблемы парадоксов, авторы обсуждают проблему того, что множество не может быть объектом ни в одной из своих «определяющих функций», в в частности «Введение», глава 1, стр. 24 «...трудности, возникающие в формальной логике», и глава 2.I. «Принцип порочного круга», стр. 37 и далее, и глава 2.VIII. «Противоречия». " стр. 60 и след.
- Мартин Дэвис , «Что такое вычисление», в «Математике сегодня », Линн Артур Стин, Vintage Books (Random House), 1980. Замечательная небольшая статья, возможно, лучшая из когда-либо написанных о машинах Тьюринга для неспециалистов. Дэвис сводит машину Тьюринга к гораздо более простой модели, основанной на модели вычислений Поста. Обсуждает доказательство Чайтина . Включает небольшие биографии Эмиля Поста и Джулии Робинсон .
- Эдвард Белтрами , Что такое случайность? Случайность и порядок в математике и жизни , Коперник: Springer-Verlag, Нью-Йорк, 1999. Приятное, нежное чтение для неспециалистов с математическим складом ума, в конце помещаются более сложные вещи. Имеет модель машины Тьюринга. Обсуждает вклад Чайтина .
- Эрнест Нагель и Джеймс Р. Ньюман , «Доказательство Гёделя» , издательство Нью-Йоркского университета, 1958. Замечательное письмо на очень сложную тему. Для математически склонных неспециалистов. Обсуждает . доказательство Генцена на страницах 96–97 и сносках В приложениях кратко обсуждаются аксиомы Пеано , мягко знакомящие читателей с формальной логикой.
- Дарас, Николас Дж.; Рассиас, Фемистокл М. (2018). Современная дискретная математика и анализ: с приложениями в криптографии, информационных системах и моделировании . Чам, Швейцария. ISBN 978-3319743240 .
{{cite book}}
: CS1 maint: отсутствует местоположение издателя ( ссылка ) . Глава 3. Раздел 1 содержит качественное описание проблемы остановки, доказательство от противного и полезное графическое изображение проблемы остановки. - Тейлор Бут , Последовательные машины и теория автоматов , Уайли, Нью-Йорк, 1967. Ср. Глава 9. Машины Тьюринга. Сложная книга, рассчитанная на инженеров-электриков и технических специалистов. Обсуждает рекурсию, частичную рекурсию со ссылкой на машины Тьюринга, проблему остановки. Имеет модель машины Тьюринга . Ссылки в конце главы 9 охватывают большинство старых книг (т.е. с 1952 по 1967 год, включая авторов Мартина Дэвиса, Ф.К. Хенни, Х. Гермеса, С.К. Клини, М. Мински, Т. Радо) и различные технические статьи. См. примечание в разделе «Программы Busy-Beaver».
- Программы Busy Beaver описаны в журнале Scientific American, август 1984 г., а также в марте 1985 г., стр. 23. Ссылка у Бута приписывает их работе Радо Т. (1962), О невычислимых функциях, Bell Systems Tech. J. 41. Бут также определяет задачу занятого бобра Радо в задачах 3, 4, 5, 6 главы 9, с. 396.
- Дэвид Болтер , Человек Тьюринга: Западная культура в компьютерную эпоху , Издательство Университета Северной Каролины, Чапел-Хилл, 1984. Для широкого читателя. Может быть датировано. Есть еще одна (очень простая) модель машины Тьюринга.
- Свен Кёлер, Кристиан Шиндельхауэр, Мартин Циглер, О приближении реальных проблем остановки , стр.454-466 (2005) ISBN 3540281932 Конспекты лекций Springer по информатике, том 3623: Неразрешимость проблемы остановки означает, что не на все случаи можно ответить правильно; но, может быть, «некоторые», «многие» или «большинство» смогут? С одной стороны, постоянный ответ «да» будет бесконечно часто правильным, и также бесконечно часто неправильным. Чтобы сделать вопрос разумным, учтите плотность случаев, которые можно решить. Оказывается, это существенно зависит от системы программирования . рассматриваемой
- Логические ограничения машинной этики с последствиями для смертоносного автономного оружия - статья, обсуждаемая в статье: Означает ли проблема остановки отсутствие моральных роботов?
Внешние ссылки
[ редактировать ]- Выхватывание петли - поэтическое доказательство неразрешимости проблемы остановки
- анимационный фильм - анимация, объясняющая доказательство неразрешимости проблемы остановки.
- Двухминутное доказательство второй по важности теоремы второго тысячелетия – доказательство всего в 13 строках