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)

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

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


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

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

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

пардон, ответил анонимусу

Блин, а я уже книжку «Практическая психотерапия» листать начал...

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

спасибо, мне `M-x doctor'-а вполне достаточно :)

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

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

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

плюсую. У меня тот же вопрос возник.

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

Я не уверен, что блок-схемы даже для кода из ОП будут иметь что-то общее, кроме примитивных структурных элементов.

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

Я имею в виду, что требование изоморфизма графов-блок-схем сильнее, чем требования ТСа.

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

Я не уверен, что блок-схемы даже для кода из ОП будут иметь что-то общее, кроме примитивных структурных элементов.

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

Я имею в виду, что требование изоморфизма графов-блок-схем сильнее, чем требования ТСа.

Ключевое требование ТСа — «как статически доказать», поэтому окромя графов мне на ум ничего «статического» не идёт :)

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

ТС, что ты имеешь в виду, когда говоришь про побочные эффекты?

эквивалентные участки кода после завершения своей работы должны одинаково модифицировать внешнее состояние (глобальные переменные, io) Но это я уже, конечно, совсем губу раскатал. Для начала хотел разобраться с чистыми функциями.

Потому что первый метод, например, подразумевает выделение памяти под какой-то range, а во втором просто стек засирается. Это считается?

нет, интересует только конечный результат вычислений

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

Ключевое требование ТСа — «как статически доказать», поэтому окромя графов мне на ум ничего «статического» не идёт :)

Ну и на фига тут графы?

Статически из кода выводятся инварианты (то есть, система уравнений). Эквивалентность инвариантов при соблюдении определенных условий будет гарантировать эквивалентность семантики. Только вот условия эти такие, что язык получится не-Тьюринг-полным (см. выше по треду про Coq).

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

О, еще один, не понимающий смысла доказательства от противного.

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

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

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

попытайся вывести второй алгоритм из первого. Если это получится, то первый эквивалентен второму. Задача скорее из математики, нежели из программирования.

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

Это неразрешимая задача.

для многих важных частных случаев решение есть. Часто оно тривиально. Например для

a*a - b*b === (a-b) * (a+b)
в левой и правой части записаны алгоритмы вычисления. И они эквивалентны. (с некоторыми допущениями).

А в общем случае — да, решение не найдено. И сдаётся мне, даже если его и найти, оно будет не нужно на практике.

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

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

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

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

можно привести обе записи алгоритма к одному виду и тем доказать эквивалентность. Но это скорее исключение

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

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

Статически из кода выводятся инварианты (то есть, система уравнений).

Ага, или из кода выводятся инварианты графа (то есть, структуры).

Ну и на фига тут графы?

Стандартный математический формализм.

quickquest ★★★★★
()

Если функции без сайдэффектов, а диапазон значений n ограничен, то перебором. Иначе (чувствую) никак.

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

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

в том, что считают по разному. Вот две функции:

float f1(float a, float b)
{
  return a*a-b*b;
}

float f2(float a, float b)
{
  return (a-b)*(a+b);
}

они очевидно разные, и очевидно дают один и тот же результат.

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

Они не дают один и тот же результат, придурок.

Результат плавучей арифметики зависит от порядка действий, придурок. Например, a*a и b*b могут терять точность быстрее чем (a-b) и (a+b).

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

Ага, или из кода выводятся инварианты графа (то есть, структуры).

Зачем тебе представлять код в виде графа? Можно, конечно же, перевести все в SSA, и потом уже инварианты выводить, но это далеко не единственный способ.

Стандартный математический формализм.

Но для этой задачи совершенно не нужный. Если только не считать банальное дерево (AST) графом, но это уже за гранью.

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

Ты представляешь себе, насколько сложна формализация алгебры для плавучих чисел? Даже для целых учет переполнения будет кошмаром, а уж для плавучки и вовсе жопа.

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

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

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

Ты используешь в своё доказательстве внутренне противоречивое число «бесконечность». Дело в том, что всегда есть число y большее x(*). Но бесконечность больше всех чисел, что доказывает то, что бесконечность — не существует как число(в силу противоречия с аксиомой (*)). А твоя программа не может зависнуть в абстрактном смысле. Время работы бесконечного цикла неопределено, но вовсе не бесконечно. Ты подменил понятия «неопределено» и «бесконечно». Таким образом можно доказать всё что угодно, хоть 2*2==5.

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

почему зависнет, а не вернет true?

потому-что с true доказательства не получится. Ему обязательно надо поделить на ноль.

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

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

Пиздец, товарищи. Полный пиздец.

Баття, как ты с таким говном вместо мозга вообще функционировать умудряешься, а?

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

но это далеко не единственный способ.

Естественно. «Моё дело идею подарить, а ТСу думать, что с этой хренью делать». © :)

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

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

а зачем нужны рассуждения с ошибками? Машина Тьюринга полна, но внутренне противоречива. Она противоречит как сама себе, так и реальности. В данном случае алгоритмы вполне конечные, и машина Тьюринга тут не нужна. Потому и проблемы остановки не существует. Она появится, вот сразу как только ты сделаешь бесконечную память. Но пока эта бесконечная память не существует IRL.

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

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

ты — тоже.

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

В алгебре есть механизм для доказательства эквивалентности этих формул.

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

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

Результат плавучей арифметики зависит от порядка действий, придурок. Например, a*a и b*b могут терять точность быстрее чем (a-b) и (a+b).

детка, учись читать. Я сказал «при некоторых допущениях». Ограничь диапазон входных значений, и погрешностей не будет. Например попробуй просчитать все комбинации a,b=[0..10], и удивись.

В общем случае, руководствуясь IEEE754, диапазон надо задать так, что-бы меньшая из разностей всегда была больше 2^-(20-log(x)), где x — значение этой разности, а числа «целые», в том смысле, что они действительно либо целые, либо целые умноженные на любую степень двойки. (иные числа ты в принципе не сможешь точно представить в float).

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

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

а ты — нет. На самом деле, там нет ничего сложного.

Даже для целых учет переполнения будет кошмаром, а уж для плавучки и вовсе жопа.

это твоя проблема. Проблема твоего невежества и тупости.

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

Компьютерочислопроблемы

да. Причём давно решённые. Просто данный анон не в курсе про решение, как и про символьные вычисления. Видать его выперли с первого курса.

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

Всё. Батти пришёл в тред, теперь здесь будет адов угар.

у вас тут и без меня адов угар.

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

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

Ага, ну ну, ничего сложного, только ты обосрался жидко выше по треду. На минуточку, плавучка - моя специальность, уже лет 20 как. Но формализовать алгебру я не возьмусь. И братва из Inria не возьмется тоже.

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

Решенные? Баття, ты проститутка. Или признай себя пиздливым чмом, публично, с деанонимизацией, или давай ссылку на плавучую алгебру.

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

Ты и десятой части необходимых тут допущений не перечислило, говнецо. Ты не понимаешь плавучки, быдло.

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

На минуточку, плавучка - моя специальность, уже лет 20 как. Но формализовать алгебру я не возьмусь

ну а если ограничится сложение/вычитанием/умножением/делением и только для i8087? Я тоже не возьмусь, ибо долго. Но ничего сложного я в этом не вижу.

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

Решенные? Баття, ты проститутка.

ох... Ну есть немного. У проститутки есть ЖПП, и она её успешно продаёт тем, у кого её нет. Я умею работать с такими числами, и успешно продаю своё умение тем, кто этого не умеет.

Что именно тебе непонятно-то? Есть же теория чисел, там вроде подробно рассмотрены вычисления с погрешностями, в чём проблема-то? Тебе учебников что-ли нагуглить?

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

Ты и десятой части необходимых тут допущений не перечислило, говнецо. Ты не понимаешь плавучки, быдло.

да, дорогая. Дополни мои допущения своими, о которых я не знаю.

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

Проститутка сказала явно, что float. Какие такин «символьные вычисления», идиот?!?

детка, а как gcc квадрат разности раскрывает?

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

да какая разница, что там у него есть. У него есть опция, при которой он вообще машинный код не создаёт. И что? Важно, что он умеет квадрат разницы, и совсем не с помощью перебора. А как раз символьно, как в средней школе делают. И создателям gcc насрать на твоё мнение и на твой сраный «опыт». Впрочем, как и мне.

Не умеешь — учись. Или помолчи, за умного сойдёшь.

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

Ты хотя бы знаешь, что такое теория чисел, проститутка? К вычислениям с погрешностью она ни малейшего отношения не имеет.

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

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

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

А этот тред про эквивалентность.

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

не, ты вправду хочешь помочь мне решить МОЮ проблему, да?

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

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

да, дорогая. А дай мне ссылку на формализацию какой-то другой алгебры.

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