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)

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

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


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

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

durashka. Kak raz a*a-b*b lu4we, 4em (a+b)(a-b). Sam idiot, a na dtugix naezzhaew. Cyrk urodov, blin.

(a+b)(a-b) eto fakto4eski (a+b+eps1)(a-b+eps2)=a*a-b*b+eps1(a-b)+eps2(a+b)+eps1*eps2

a*a-b*b fakti4eski a*a+eps1-b*b+eps2

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

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

детка, «эквивалентность вообще» не существует. Существует лишь в некоторых рамках. Например числа int32_t эквивалентны целым числам, но не всегда, а только-лишь в некотором определённом диапазоне. Так и с любыми другими числами.

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

ты точно уверен, что ТСу нужна именно твоя «абсолютная эквивалентность»? Или может ему хватит и моей, ограниченной, но за то реальной?

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

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

Ты хоть обдрочись, шлюшка, а компилятор эквивалентность обеспечивать обязан.

И еще, сучка, ответь по всей форме за свой жидкий обсёр про «теорию чисел».

anonymous
()

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

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

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

man Hoare logic. Ну или его бородатые статьи про program refinement для последовательных программ, если и так все понятно.

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

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

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

Kak raz a*a-b*b lu4we, 4em (a+b)(a-b).

ну IRL оно зависит от удельной цены каждой операции, если «лучше» по скорости.

(a+b)(a-b) eto fakto4eski (a+b+eps1)(a-b+eps2)=a*a-b*b+eps1(a-b)+eps2(a+b)+eps1*eps2

в этом смысле — да, получше. Если a примерно равно b. В противном случае a*a-b*b вырождается в a*a(при том, что a>>b), а вот из (a-b) возможно можно вытянуть немного бит информации, потому потери могут быть меньше(если разность a-b где-то около 2^-30, если она намного меньше, то вторая формула даёт результат, который вырождается в a*a-a*b). ЕМНИП истинный результат лежит между этими двумя значениями.

Это всё можно проверить аналитически или численно... Сейчас попробую.

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

в этом смысле — да, получше. Если a примерно равно b. В противном случае a*a-b*b вырождается в a*a(при том, что a>>b)

ono i tak i tak vyroditsa. Tak kak pri a>>b 4to a+b, 4to a-b ravny a.

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

а компилятор эквивалентность обеспечивать обязан.

только в определённых рамках. 1 != 3/3, что в этом удивительного? Просто 1/3 не представимо точно в float, потому есть некоторая ошибка, которая может появится после умножения на 3. А может и не появится. Формально, при сложении(а значит и при умножении), добавляется последний отбрасываемый разряд. А значит ошибка в точности равна x=младший_бит*случайное число_равное_0_или_1. Для умножения float таких битов 23 штуки, причём общий их вес равен x1/2+x2/4+x3/8+...+x23/2^23. При делении ошибка такая же, ибо деление реализовано через умножение, путём дихотомии(AFAIK). Фактичски деление — тоже умножение, но вместо 23х сложений 23 вычитания(23 максимум, в среднем 23/2).

И еще, сучка, ответь по всей форме за свой жидкий обсёр про «теорию чисел».

так тебе учебников нагуглить, детка? А то ты задаёшь вопросы, которые попросту не имеют смысла.

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

начни отсюда: https://en.wikipedia.org/wiki/Halting_problem#Sketch_of_proof

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

if (halts(arg)) { while(1); } else return false;
все доказывает. Зачем быть такими?

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

O. Tak v wiki okazivaetsa tozhe tak napisano. Nu dyk pravilnoe zhe dokazatelstvo. A oblivajut govnom potomu 4tho LOR. Nu i potomu 4to sami malo 4to znajut i ispolzujut svoj wans.

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

ono i tak i tak vyroditsa.

да, но уже тогда, когда |a-b|<2^-46.

ну путём моделирования так и получается: если положить a=1.0, и уменьшать b, то до b=2.441406e-04 ошибка равна нулю, а потом она скачком достигает 1.490116e-08, и потом уменьшается до 2.220446e-16 для обоих формул(при b=1.490116e-08), при дальнейшем уменьшении b ошибка опять становится нулевой, т.е. формула опять становится точной.

Формулы дают одну и туже погрешность и в float и в longdouble, за исключением аномального значения

a=1.000000, b=5.960464e-08, a*a-b*b=1.000000(3.552714e-15), (a+b)*(a-b)=1.000000(-5.960464e-08)
это всё в сопроцессоре i686 Intel(R) Atom(TM) CPU N270, в других CPU картина будет конечно иная количественно, но не качественно.

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

все доказывает.

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

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

Nu dyk pravilnoe zhe dokazatelstvo.

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

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

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

mozhno dopustit', 4to pamjat' beskone4na.

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

и да, эквивалентные формулы вовсе не обязаны давать одинаковый результат, т.к. в каждой из формул имеется случайный компонент, который ни от чего не зависит. Т.о. 1+x != 1+x, и это несмотря на то, что 1===1. Всё дело в случайном компоненте, который и приводит к неравенству эквивалентных формул.

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

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

mozhno dopustit', 4to pamjat' beskone4na.

можно. Но тогда придётся допустить и бесконечные алгоритмы. Но нужны-ли они тебе? Какая практическая ценность в них?

А если ты ограничил алгоритмы конечным числом _разных_ операций(т.е. цикл while(true); тоже конечный алгоритм), то твоё доказательство недействительно.

IRL мы имеем дело не с бесконечными, а с неопределёнными алгоритмами. Цикл while(x-x==0); работает неопределённо долго. Может сразу закончится, а может год проработать. В общем случае это неизвестно.

Замена «бесконечности» в индукции на «неопределённость» просто лишает смысла эту индукцию.

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

mozhno dopustit', 4to pamjat' beskone4na.

можно. Но тогда придётся допустить и бесконечные алгоритмы. Но нужны-ли они тебе? Какая практическая ценность в них?

net. kone4nyj po vremeni algoritm ne mozhet byt beskone4nym po pamjati.

dikiy ★★☆☆☆
()

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

В общем случае - никак. См. «Проблема эквивалентности».

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

net. kone4nyj po vremeni algoritm ne mozhet byt beskone4nym po pamjati.

IRL может. Например если память растёт как n!. Задолго до 20й итерации тебе не хватит всех атомов во вселенной, даже если ты будешь на каждом по 1 биту хранить.

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

net. kone4nyj po vremeni algoritm ne mozhet byt beskone4nym po pamjati.

IRL может. Например если память растёт как n!. Задолго до 20й итерации тебе не хватит всех атомов во вселенной, даже если ты будешь на каждом по 1 биту хранить.

IRL eto ne beskone4nyj algoritm, a algoritm, kotoromu nado o4en mnogo pamjati.

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

Пиздец, детский сад.

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

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

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

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

IRL eto ne beskone4nyj algoritm, a algoritm, kotoromu nado o4en mnogo pamjati.

да. Ну и что? Какое это вообще отношение имеет к нашему спору? В случае ТСа память можно считать бесконечной, а сам алгоритм — конечным.

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

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

2анон: ты настолько тупой, что можешь выражаться исключительно как чурка, который вчера из чуркистана приехал, и выучил всего 10 русских слов, из которых 4 запрещены здешними правилами? Ну выучи ещё 10, а потом возвращайся. Попроси своего хозяина прочитать и растолковать тебе этот пост по-вашему.

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

Соска, отвечай, какой из разделов http://en.wikipedia.org/wiki/Number_theory и под какими веществами ты приплел к «вычислениям с погрешностью»? Или признавай себя публично тупым, некомпететным, ничтожным пиздоболом.

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

Ты пиздец как упорот. Как такое уебище вообще функционировать-то умудряется?!?

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

Соска, отвечай, какой из разделов http://en.wikipedia.org/wiki/Number_theory и под какими веществами ты приплел к «вычислениям с погрешностью»?

и к чему-же по твоему относятся вычисления с погрешностью, такие как с числами float, и, ВНЕЗАПНО int32_t? Может к поэзии?

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

К арифметике, деточка, к банальной арифметике. А что такое теория чисел ты тупо не знаешь. Зачем ты воняешь о том, в чем не разбираешься?

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

К арифметике, деточка, к банальной арифметике.

вот смотри, сложили Over9000 чисел от 0 до 1 (с равномерным распределением). В каком диапазоне лежит 95% сумм? Ответ обоснуй с помощью арифметики. Использовать теорию чисел не нужно(по твоему).

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

«Численные методы» это называется, а теория чисел — совсем другое.

численные методы — часть теории чисел. Да, совсем другое.

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

Numeric analysis пользуется некоторыми из выводов теории чисел, но к теории чисел не относится. Садись, два.

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

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

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

ты, козлик, просто знаешь лишь малую часть теории чисел. Ту, про что что в вике рассказано. Все 3 странички.

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

Пиздец, детский сад.

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

Рассказывай, какая тут будет потеря точности,

[latex] A+ \sum a_i + \sum \epsilon_i[/latex]

и почему ее нельзя выразить через epsilon для каждой из операций.

можно. См. выше, петушок.

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

Ты в своём дойчланде забыл синтаксис команды setxkbmap?

на той тачке он не работал.

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

да. Ну и что? Какое это вообще отношение имеет к нашему спору? В случае ТСа память можно считать бесконечной, а сам алгоритм — конечным.

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

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

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

и к чему-же по твоему относятся вычисления с погрешностью, такие как с числами float, и, ВНЕЗАПНО int32_t? Может к поэзии?

к чему угодно, но не к теории чисел :) Относятся просто к разделу численной методов. Этот раздел занимает объем в две лекции. Там нечего собсно учить.

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

Слушай, ну не позорься, а. Тебе правильно говорили, что погрешность float операций через «эпсилон» не выразить. Поскольку этот эпсилон будет зависеть от обоих аргументов. И этот придурок пишет суммы. Попробуй литературу что ли почитать, если своего ума не хватает.

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

мимокрокодил

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

while(true)

Почему ты считаешь, что это конечный алгоритм? Семантически, для отдельно взятого ЯП, он бесконечен. Ты можешь прервать его только переопределив значение тру или значение самого уайл, что семантика ЯП не предусматривает, либо, специальной конструкцией return, но это относиться к сахару языка а не алгоритму. Твой алгоритм эквивалентен бесконечной рекурсии, имхо.

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

Слушай, ну не позорься, а. Тебе правильно говорили, что погрешность float операций через «эпсилон» не выразить.

выразить. читаем стандарт IEEE и видим там, что eps для double равен 1.11e-16.

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

в стандарте есть верхняя граница ошибки.

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

читаем стандарт IEEE и видим там, что eps для double равен 1.11e-16

Ты совсем упорот, дебил? Ты откуда это вообще взял? По-твоему погрешность для чисел порядка 1e10 и порядка 1e-10 одинакова? (Подсказка: мантисса и порядок float'ов всегда занимает одинаковое число бит)

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

еще один анонимусоламер. Я взял это из стандарта IEEE754. Да, верхняя граница погрешности для этих чисел одинакова. Мы же говорим о a=\tilde a(1+eps).

dikiy ★★☆☆☆
()
Последнее исправление: dikiy (всего исправлений: 1)
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.