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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Но, насколько я понимаю

Ты не понимаешь. Попробуй еще раз. Начни отсюда: https://en.wikipedia.org/wiki/Halting_problem#Sketch_of_proof

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

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

a*a - b*b === (a-b) * (a+b)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ты — тоже.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

У gcc есть опция, запрещающая это безобразие.

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

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

dr_batty знает все о твоих проблемах

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

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

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

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

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

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

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