LINUX.ORG.RU

как статически доказать эквивалентость двух произвольных алгоритмов

 


2

2

Под эквивалентностью я подразумеваю равенство выходных данных и произведенных побочных эффектов

Например, для двух функций вычислений n-го числа фибоначчи (питон)


def fib1(n):
    a, b = 0, 1
    for _ in range(n):
        a, b = b, a + b
    return a

def fib2(n):
    if n < 2:
        return n
    return fib2(n-1) + fib2(n-2)

как доказать что соотношения множеств входных и выходных данных для этих функций одинаковы (не учитывая переполнение стека для второй) ?

Питон тут для примера, для какого-нибудь лиспа, наверное, проще будет сделать это


Уже при n = -1 получается разный результат. Алгоритмы не эквивалентны.

Deleted
()
Ответ на: комментарий от Deleted

Поторопися, да. Простите. Суть понятна в общем.

qweqwe
() автор топика

Для общего случая доказать эквивалентность нельзя. Напрмер, алгоритм 1 ищет полным перебором контрпример к задаче Гольдбаха, и когда находит, возвращает 1. А алгоритм 2 всегда возвращает 1. Никто не знает, эквивалентны ли эти два алгоритма.

Deleted
()
Ответ на: комментарий от qweqwe

По вашей ссылке говорится что еще неизвестно к какому классу задач она относится.

Дык, в общем случае решение пока не найдено, поэтому «математическая религия» рекомендует считать NP.

quickquest ★★★★★
()

в общем случае задача неразрешима.

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

MKuznetsov ★★★★★
()

использовать структурную индукцию, например.

invy ★★★★★
()

я не понимаю проблемы. Обе программы считают, очевидно, числа Фибоначчи. Обе считают их верно. Потому и выхлоп будет одинаковый. В чем проблема?

dikiy ★★☆☆☆
()
Ответ на: комментарий от BlackHawk

Если теорем-прувер не тьюринг-полный, то и проблемы останова не существует.

anonymous
()
Ответ на: комментарий от dikiy

очевидно

Кому очевидно?

Обе считают их верно

Почему?

В чем проблема?

Не все функции считают числа Фибоначчи

anonymous
()
Ответ на: комментарий от anonymous

очевидно

Кому очевидно?

мне. А тебе нет?

Обе считают их верно

Почему?

потому что:

Алгоритм 1:
на каждоый итерации цикла мы получаем в переменной b следующее число Фибоначчи. Это слелует из формулы рассчета этих чисел. Доказывается тривиально с помощью матиндукции.

Алгоритм 2:
еще проще. Так как алгоритм напрямую реализует рекурсивную формулу для чисел Фибоначчи.

В чем проблема?

Не все функции считают числа Фибоначчи

но мы же про эти две говорим.

//update

только сейчас внимательно прочитал заголовок и понял, что ресь о произвольных алгоритмах.

dikiy ★★☆☆☆
()
Последнее исправление: dikiy (всего исправлений: 1)
Ответ на: комментарий от dikiy

В чем проблема?

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

qweqwe
() автор топика
Ответ на: комментарий от dikiy

Я себе (и тебе) доверяю меньше, чем вердикту агды или кока. Естественно, ты можешь на бумажке повторить все шаги доказательства и сам, только совершенно не очевидно, что ты не упустишь какой-то edgecase, где функции не равны, в отличие от теорем-прувера.

Ну и да, Фибоначчи, как и написано в посте, это всего лишь пример.

anonymous
()
Ответ на: комментарий от anonymous

В питоне - никак.

Я написал что питон в качестве примера. Да и сомневаюсь, что у питона тут имеется какой-нибудь фатальный недостаток.

qweqwe
() автор топика
Ответ на: комментарий от qweqwe

Да и сомневаюсь, что у питона тут имеется какой-нибудь фатальный недостаток.

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

anonymous
()
Ответ на: комментарий от anonymous

В том доказательстве говорится, что эта задача неразрешима на тьюринг-машине. Но есть же еще, как минимум, лямбда-исчисление, которое вроде бы ей (машине) противопоставляется. И, следовательно, общего доказательства таки нет. Или я ошибаюсь?

qweqwe
() автор топика
Ответ на: комментарий от anonymous

эквиваленто в выразительности, но это разве значит что доказательства для одного справедливы и для другого?

qweqwe
() автор топика
Ответ на: комментарий от qweqwe

Эквивалентно значит эквивалентно. Все, что справедливо для машины Тьюринга, справедливо и для любой другой Тьюринг-полной системы - лямбда-исчисления, алгорифмов Маркова, комбинаторной логики, и т.п.

anonymous
()
Ответ на: комментарий от qweqwe

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

anonymous
()
Ответ на: комментарий от true_admin

Там достаточно изящное доказательство. Предположим, у нас есть функция, которая по коду программы и её аргументам определяет, остановится она или нет; если программа с такими аргументами не остановится, то функция нам вернет, к примеру, false, если же программа остановится, то функция зависнет. Напишем такую программу: она скармливает функции собственный код и аргументы и завершается. Что в итоге: программа завершится, если функция сказала, что она не завершится, и наоборот. Печалька, противоречие и разумный вывод: такую функцию написать нельзя.

Разумеется, все это формально описывается, а я тут на пальцах объясняю.

devsdc ★★
()
Ответ на: комментарий от true_admin

А ты понимаешь суть доказательства этой теоремы? Мне оно кажется бредом.

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

Ну это если ты под бредом понимаешь не тезис Тьюринга («вычислимо == реализуемо на машине Тьюринга»).

ilammy ★★★
()

в общем случае - никак.

в частных - придумавай и проверяй инварианты

MyTrooName ★★★★★
()
Ответ на: комментарий от MyTrooName

Наверное, глупо прозвучит, но зачем понадобилось ее так конструировать? Подогнать под противоречие?

qweqwe
() автор топика
Ответ на: комментарий от qweqwe

Затем, чтобы доказать теорему.

Ты не мал ли эквивалентность программ проверять? Может сначала с мат логикой на минимальном уровне хотя бы ознакомишься?

aedeph_ ★★
()
Ответ на: комментарий от qweqwe

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

MyTrooName ★★★★★
()
Последнее исправление: MyTrooName (всего исправлений: 1)
Ответ на: комментарий от qweqwe

Да. Потому что где-то должна быть бесконечность. Машина Тьюринга потому и машина Тьюринга, что у неё по определению бесконечная лента с памятью и существует бесконечное количество программ для неё. И проблема останова как раз и говорит о том, что машина Тьюринга не может за конечное время перебрать бесконечное количество программ под саму себя.

Можно построить эквивалентное доказательство несуществования функции h(p, d), которая за конечное время отвечает на вопрос: «остановится ли вычисление p(d)» в виде «да» или «нет». Но для этого понадобится программа, которая проверяет наличие конкретной бесконечной последовательности в бесконечной последовательности бесконечных последовательностей, что те же яйца, только в профиль.

ilammy ★★★
()
Последнее исправление: ilammy (всего исправлений: 1)
Ответ на: комментарий от aedeph_

Затем, чтобы доказать теорему.

ок, начну сначала

функция(код_который_не_завершается) --> false 
функция(код_который_завершается)    --> функция зависла 

Зачем это нужно и где тут противоречия? Функция вернет/не вернет ровно то, что в ней записано вернуть, а записать туда можно что угодно. Каким образом она вообще поможет доказать что-либо?

впрочем, ладно, автор писал что это на пальцах, вернемся к «источнику»:

Назовем Анализатором гипотетический алгоритм, который получает на вход пару натуральных чисел (N,X), и:

  • останавливается и возвращает 1, если алгоритм с номером N не останавливается, получив на вход X
  • не останавливается в противном случае (если алгоритм с номером N останавливается, получив на вход X).

Проблему остановки можно переформулировать следующим образом: существует ли Анализатор?

Теорема. Анализатор не существует.

Докажем это от противного. Допустим, Анализатор существует...

Но кого волнует доказательство остутствия анализатора который не останавливается при анализе? Разве нужный нам анализатор не должен останавливаться и просто возращать 0|1?

Ты не мал ли эквивалентность программ проверять?

возможно

Может сначала с мат логикой на минимальном уровне хотя бы ознакомишься?

врядли

qweqwe
() автор топика
Ответ на: комментарий от qweqwe

Может сначала с мат логикой на минимальном уровне хотя бы ознакомишься?

врядли

И зачем нужен ещё один гуманитарный гений с чушью вместо формальных рассуждений? Не нужен, совсем.

aedeph_ ★★
()
Ответ на: комментарий от aedeph_

И зачем нужен ещё один гуманитарный гений

откуда вы знаете кто я, и какое отношение моя нужность имеет к вопросу?

с чушью вместо формальных рассуждений

где именно?

qweqwe
() автор топика
Ответ на: комментарий от aedeph_

Я тебя читаю.

ну и какое же утверждение или совокупность утверждений достаточны для причисления меня к гуманитариям ?

Чушь в том, что ты не понимаешь, о чём говорит теорема останова.

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

qweqwe
() автор топика
Ответ на: комментарий от devsdc

если программа с такими аргументами не остановится, то функция нам вернет, к примеру, false, если же программа остановится, то функция зависнет.

Я читал док-во и у меня главный вопрос: как это связано с исходной задачей. Т.е. почему отсюда следует что нет функции которая вернёт true или false?

cast ilammy

PS читаю английскую статью, там, похоже, эта тема раскрыта.

true_admin ★★★★★
()
Ответ на: комментарий от qweqwe

ну и какое же утверждение или совокупность утверждений достаточны для причисления меня к гуманитариям ?

Полное непонимание метода доказательства от противного и нежелания это непонимание убрать. Следствие этого - классификация как топливо для биореактора.

aedeph_ ★★
()
Ответ на: комментарий от true_admin

Т.е. почему отсюда следует что нет функции которая вернёт true или false?

В общем случае нельзя, потому как есть очевидные исключения. Это как с интеграллами: в общем виде решения нет, но в определённых случаях посчитать можно.

anonymous
()
Ответ на: комментарий от aedeph_

Полное непонимание метода доказательства от противного

Давайте представим, что aedeph_ знает почему доказательство сформулировано именно так как сформулировано. Следовательно он может объяснить это. Цель aedeph_ - показать всем что он самый умный. Объяснить всем суть теоремы и суть ее доказательства это самый быстрый и 100% гарантированный способ для aedeph_ достичь своей цели. Следовательно aedeph_ давно уже должен был рассказать нам свои умные мысли.
Из того, что он этого не сделал следует вывод что он выпендривается.

TDrive ★★★★★
()
Ответ на: комментарий от anonymous

Зачем это нужно

то есть, из непонимания возможности доказательства функцией с подогнанным алгоритмом следует

Полное непонимание метода доказательства от противного

да?)

то есть, вот это вот

if (halts(arg)) { while(1); } else return false

это доказательство, и то что я его не понимаю достаточно для

причисления меня к гуманитариям

все верно?

qweqwe
() автор топика
Ответ на: комментарий от qweqwe

это доказательство, и то что я его не понимаю достаточно для | причисления меня к гуманитариям | все верно?

Это ты мне, типа, шараду загадал, да?

Тебя интересует обобщённое для всех возможных состояний/случаев/функций/программ решение в некотором пространстве состояний или тебе будет достаточно одного частного решения из всех возможных, которое впишется в указанные граничные условия? :D

P.S. Нет, указанный набор не является необходимым и достаточным. И, вообще, смотри на конструирование функций, как на бомбардирование некоторого состояния тестами: провалило тест - в общем виде неработоспособно.

anonymous
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.