Как проверить, возвращают ли два алгоритма один и тот же результат для любого ввода?

18

Как проверить, возвращают ли два алгоритма (скажем, сортировка слиянием и наивная сортировка) один и тот же результат для любого входа, когда набор всех входов бесконечен?

Обновление: Спасибо, Бен, за описание того, как это невозможно сделать алгоритмически в общем случае. Ответ Дейва - это краткое изложение как алгоритмических, так и ручных (с учетом человеческого ума и метафоры) методов, которые не всегда работают, но довольно эффективны.

computability formal-methods software-engineering software-verification Андрес Риофрио
источник
5
как сказал ювал, не существует процедуры, которая могла бы определить это для любых двух программ. но в особом случае, таком как ваш пример, вы можете доказать это: например, если вы докажете, что оба ваших алгоритма возвращают отсортированную последовательность и являются стабильными, все будет сделано.
Сашо Николов
1
Вы хотите автоматическую технику / алгоритм или набор ручных техник?
Дейв Кларк
@SashoNikolov, если производительность считается частью вывода, вы также должны показать, что они оба работают в одинаковой сложности времени / пространства.
edA-qa mort-ora-y
1
Вы имеете в виду «проверить» или доказать? Имеется в виду «любой вход» или все входы? Какова мотивация и контекст для вопроса?
Каве
2
@AndresRiorio: методы проверки отличаются от алгоритмов, решающих общую проблему. Например, проблема остановки неразрешима, но, безусловно, можно доказать завершение многих программ (вручную или с помощью автоматической эвристики).
Рафаэль

Ответы:

16

В отличие от того, что говорят «отговорки», для этого существует множество эффективных методов.

  • Бизимуляция является одним из подходов. См., Например, статью Гордона о коиндукции и функциональном программировании .

  • Другой подход заключается в использовании операционных теорий эквивалентности программ, таких как работа Питта .

  • Третий подход заключается в проверке того, что обе программы удовлетворяют одной и той же функциональной спецификации. Есть тысячи работ по этому подходу.

  • Четвертый подход заключается в том, чтобы показать, что одну программу можно переписать в другую, используя звуковые преобразования программ .

Конечно, ни один из этих методов не является полным из-за неразрешимости, но объемы и объемы работы были созданы для решения этой проблемы.

Дэйв Кларк
источник
heu · ris · tic . [Gr. εὑρίσκω "открыть"] n. 1. Техника, предназначенная для решения проблемы, которая игнорирует, может ли решение быть доказано, что оно является правильным, но которая обычно дает хорошее решение или решает более простую проблему, которая содержит или пересекается с решением более сложной проблемы. 2. ( Теорет. ) Алгоритм, который не работает.
Джефф
1
Барт Симпсон: «Не могу победить. Не пытайся».
Дейв Кларк
9
@JeffE: Если вы хотите проверить, возвращают ли два алгоритма один и тот же результат, вы делаете доказательство. Есть много хороших методов для этого. Конечно, все методы неполные, но кого это волнует? Теорема Гёделя о неполноте не является причиной для отказа от математики!
Нил Кришнасвами
3
@JeffE Тот факт, что нет вычислимой функции для определения того, возвращают ли два произвольных алгоритма один и тот же результат, не означает, что вы не можете ответить на вопрос для любых двух конкретных алгоритмов, тем более что процесс поиска доказательства не является вычислимым функция . Точно так же есть множество статей, которые доказывают гарантированное завершение для определенных алгоритмов, независимо от того, что невозможно механически определить, будет ли произвольный алгоритм всегда завершаться.
Бен
2
На практике два алгоритма, которые должны вычислять одну и ту же функцию, вряд ли когда-либо позволят получить доказательство эквивалентности на основе бисимуляции. (В случае вышеупомянутых алгоритмов сортировки промежуточные этапы циклов / рекурсии различны.) Я бы сказал, что использование старой доброй Hoare-логики, чтобы показать, что они оба реализуют одну и ту же спецификацию поведения ввода-вывода, является способом идти.
Кай
10

Чтобы немного уточнить утверждения «невозможно», вот простой набросок доказательства.

Мы можем смоделировать алгоритмы с выводом на машины Тьюринга, которые останавливаются с выводом на ленту. Если вы хотите иметь машины, которые могут останавливаться, принимая либо вывод на их ленту, либо отклоняя (в этом случае нет вывода), вы можете легко придумать кодировку, которая позволяет вам моделировать эти машины с «остановкой или остановкой, нет брака "машины".

Теперь предположим, что у меня есть алгоритм P для определения, имеют ли два таких ТМ одинаковый выход для каждого входа. Затем, учитывая TM A и вход X , я могу построить новую TM B, которая работает следующим образом:

  1. Проверьте, является ли вход точно X
  2. Если да, то введите бесконечный цикл
  3. Если нет, тогда запустите A на входе

Теперь я могу запустить P на A и B . B не останавливается на X , но имеет тот же вывод, что и A для всех других входных данных, поэтому, если и только если A не останавливается на X, тогда эти два алгоритма имеют одинаковый выход для каждого входа. Но предполагалось, что P сможет определить, имеют ли два алгоритма одинаковые выходные данные для каждого входа, поэтому, если бы у нас был P, мы могли бы сказать, останавливается ли произвольная машина на произвольном входе, что является проблемой остановки. Поскольку известно, что проблема остановки является неразрешимой, P не может существовать.

Это означает, что не существует общего (вычислимого) подхода к определению того, имеют ли два алгоритма один и тот же вывод, который всегда работает, поэтому вы должны применить рассуждения, специфичные для пары алгоритмов, которые вы анализируете. Однако на практике могут быть вычислимые подходы, которые работают для больших классов алгоритмов, и, безусловно, есть методы, которые вы можете использовать, чтобы попытаться выработать доказательство для любого конкретного случая. Ответ Дейва Кларка дает вам некоторые важные вещи, которые стоит посмотреть здесь. Результат «невозможности» относится только к разработке общего метода, который решит проблему раз и навсегда для всех пар алгоритмов.

Бен
источник
п
@ Рафаэль Да, аргумент, который я набросал, ничего не говорит о таком ограниченном P , только то, что не может существовать полностью общий. Мой инстинкт состоит в том, что проблема остановки все еще неразрешима, даже если вы ограничиваете ее «алгоритмами сортировки», а не общими алгоритмами, и в этом случае доказательство невозможности все еще имеет место, хотя я никогда не слышал такого утверждения.
Бен
2
В более общем смысле, теорема Райса утверждает, что не существует вычислимого способа доказать что-либо об алгоритме, как только есть хотя бы один алгоритм, обладающий тем свойством, которое вы пытаетесь доказать, и хотя бы один, который этого не делает. Например, с учетом алгоритма A нет вычислимой функции, которая принимает алгоритм B в качестве входных данных и проверяет, является ли B эквивалентным A.
Жиль "ТАК - перестань быть злым"
Важно отметить, что теорема Райса применима только к свойствам языков , а не к машинам Тьюринга (когда вы используете их в качестве модели «алгоритма»). Если существует возможность существования двух машин Тьюринга, которые оба распознают один и тот же язык, но у одного есть свойство, а у другого его нет, то теорема Райса неприменима, и может существовать общий вычислимый метод для тестирования свойства. Но теорема Райс явно применима к этому случаю, да.
Бен
2

Это вообще невозможно, но многие ограничения могут сделать это возможным. Например, вы можете проверить эквивалентность двух программ с прямым кодом, используя BDD. Символическое исполнение может справиться со многими другими случаями.

Джеймс Коппел
источник
1

Невозможно разработать алгоритм, который доказывает это равенство вообще. Подсказка: сокращение от проблемы остановки.

Юваль Фильмус
источник
Существует много методов, но ни один из них не является полностью автоматическим.
Дейв Кларк
Я не знаю, возможно это или нет, твой ответ - просто комментарий. не ответ
@SaeedAmiri: я немного уточнил контекст ответа; Я думаю, что это достаточно полно, если не очень хорошо.
Рафаэль
@ Рафаэль, Сокращение, которое в уме Ювала, очевидно, и я не думаю, что OP не знает об этом, но трудная проблема IMO - найти способ для особых случаев, так что это очевидное сокращение может быть комментарием к напоминанию OP. для общего случая.
2
@SaeedAmiri: Это должны решать ОП и избиратели, а не мы.
Рафаэль