У нас есть логика Хоара. Почему все еще возможно, что алгоритм верен, но нет никаких доказательств того, что он верен? Предположим, что алгоритм выражен в C. Тогда мы можем шаг за шагом утверждать, что он делает то, что должен делать.
Итак, мой вопрос:
Приведите мне пример алгоритма, который является правильным, но не имеет доказательства правильности.
РЕДАКТИРОВАТЬ: Я думаю, немного фона может помочь уточнить, куда я иду. Позвольте мне процитировать Скотта Ааронсона:
С 1970-х годов появились предположения, что P NP может быть независимым (то есть ни доказуемым, ни опровергаемым) от стандартных систем аксиом математики, таких как теория множеств Цермело-Френкеля. Чтобы было ясно, это будет означать, что либо
Алгоритм полиномиального времени для NP-полных задач не существует, но мы никогда не сможем доказать это (по крайней мере, в наших обычных формальных системах), иначе
полиномиальный алгоритм для NP-полных задач делает существует, но либо мы никогда не можем доказать , что он работает, или мы никогда не можем доказать , что он останавливается в полиномиальное время.
Я имею в виду вторую возможность. Поскольку Ааронсон может так уверенно перечислить это как возможность, я думаю, что должен существовать пример типа 2. Вот почему я задаю этот вопрос. Но, кажется, быстрого и ясного ответа не видно.
источник
Ответы:
Вот алгоритм для функции тождества:
Большинство людей подозревают, что этот алгоритм вычисляет функцию тождества, но мы не знаем, и мы не можем доказать это в общепринятой системе математики ZFC .
источник
Большинство алгоритмов не доказали свою корректность в логике Хоара. Основная причина в том, что такие корректные доказательства чрезвычайно дороги по состоянию на январь 2017 года, вероятно, на несколько порядков по сравнению с «простым» программированием. В настоящее время ведется большая работа по снижению этих затрат за счет автоматизации, но это нелегкая борьба.
Другая причина, по которой у алгоритма может не быть доказательства корректности, и который на практике более актуален, чем явления неполноты, о которых упоминали Ювал и Чи, заключается в том, что мы можем не знать, что это за спецификация. Эта проблема имеет два измерения.
Клиенты не знают, чего хотят. Это хорошо известная проблема в разработке программного обеспечения, и разработчики программного обеспечения разработали множество подходов для решения этой проблемы.
Спецификация сложна. Хорошим примером является правильность криптографических алгоритмов. Только недавно Micali & Goldwasser получили награды Turing за то, что они указали, что означает криптографическая безопасность. Однако обратите внимание, что это определение (насколько мне известно) для «теоретической криптографии», где у вас есть параметр безопасностиn начиная с натуральных чисел, и противники являются вероятностными машинами Тьюринга за полиномиальное время. Насколько мне известно (пожалуйста, исправьте меня, если я ошибаюсь), существует несоответствие между теорией и практикой, и конкретные алгоритмы, такие как AES и SHA256, не вполне соответствуют этим теоретическим спецификациям. Я не думаю, что есть полная спецификация для таких алгоритмов, поэтому мы не можем, в принципе, проверить их в смысле, например, логики Хоара.
источник
Это связано с незавершенностью базовой логики. Действительно, логика Хоара обычно содержит правило ослабления или «до публикации» где значение необходимо доказать в базовой логике, обычно это логика первого порядка (FOL) с некоторой теоретико-множественной аксиоматизацией, такой как Zermelo- Френкель (ZF). P
Сложность в том, что мы знаем, что такая логика неполна, как доказал Гедель почти сто лет назад. Более конкретно, существует предикат о натуральных числах для которого мы можем доказать внутри логики , , и так далее для любой данной натуральной постоянной, но нет никакого способа доказать .Р ( 0 ) Р ( 1 ) Р ( 2 ) ∀ п ∈ N . P ( n )P(n) P(0) P(1) P(2) ∀n∈N. P(n)
Со стороны информатики это странное поведение может быть продемонстрировано с помощью теории вычислимости. Предположим, что машина Тьюринга при запуске на пустой ленте не останавливается за шагов ( ). Тогда в ZF мы можем доказать этот факт, по существу разворачивая выполнение шаг за шагом в доказательстве. Однако, когда расходится, мы не можем надеяться, что сможем доказать дивергенцию в ZF ( ). В самом деле, если бы это было возможно для всех данных , то мы могли бы полуопределить дивергенцию, перечислив все возможные доказательства для и остановившись, когда он найден. Поскольку мы знаем, что дивергенция не является RE, это невозможно.n P ( n ) M ∀ n . P ( n ) M ∀ n . P ( n )M n P(n) M ∀n. P(n) M ∀n. P(n)
источник
Проблема: выведите «Да», если каждое четное число ≥ 4 является суммой двух простых чисел, и «Нет», если существует четное число ≥ 4, которое не является суммой двух простых чисел.
Алгоритм: вывести «Да»
Большинство людей считают, что алгоритм правильный. Там нет известных доказательств, и это вполне возможно , что нет никаких доказательств.
источник
Любой алгоритм, который является правильным, но мы не знаем, сколько времени потребуется для его запуска, может быть преобразован в алгоритм, который останавливается за гарантированное количество времени, но мы не уверены, что он правильный.
Например, чтобы найти простое число больше , начните отсчет с тестирования, если каждое число простое, пока не найдете его. Теперь измените его, чтобы сдаться и вернуть если мы не можем найти простое число после попытки . Если модифицированный алгоритм когда-либо возвращает , это неверно, но никто не знает, случится ли это когда-либо или нет. Даже с помощью шагов, которые мы не можем доказать, простое число всегда будет найдено.n + 1 0 log ( n ) 2 0 √n n+1 0 log(n)2 0 n−−√
Итак, у нас есть алгоритм, который является правильным, но у нас нет доказательств того, что он работает за полиномиальное время, и алгоритм (тот же, но ограниченный по времени), который работает за полиномиальное время, но у нас нет никаких доказательств того, что он верен. Как и в случае с проблемой , для этого примера также вероятно, что таких доказательств не существует.P=NP
источник