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)

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

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


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

давай-ка это на один из известных мне ЯП переложим, хорошо? А то вот такая хрень: «ℕ» у мну никуда не лезет.

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

давай-ка это на один из известных мне ЯП переложим, хорошо?

Всё равно что говорить «давай-ка переложим шаблоны C++ на известный мне Си». Если Agda или подобный язык тебе не известны, то в C++ (или, там, Haskell) ты не найдёшь нужных для написания этой программы штук, так же как в Си не найдёшь шаблонов.

А то вот такая хрень: «ℕ» у мну никуда не лезет.

У тбу есть GMP и вообще — http://pwparchive.wordpress.com/2012/03/29/dependent-typing-in-c/.

Если в C++ добавить парочку фич, то переписать можно так:

Nat fib1_rec(Nat a, Nat b, Nat n) {
    return n == 0 ? a : fib1_rec(b, a + b, n - 1);
}

Nat fib1(Nat n) {
    return fib1_rec(0, 1, n);
}

Nat fib2(Nat n) {
    return n < 2 ? n : fib2(n - 2) + fib2(n - 1);
}

template <Nat m, Nat n>
Eq<fib1_rec(fib2(m), fib2(m + 1), n), fib2(m + n)>
go() {
    return
        n == 0 ?
        cong(fib2, sym(n_plus_zero_eq_n<m>())) :
        trans(go<m + 1, n>(),
              cong(fib2, sym(m_plus_one_plus_n_eq_one_plus_m_plus_n<m, n>())));
}

template <Nat n>
Eq<fib1(n), fib2(n)>
fib1_eq_fib2() {
    go<0, n>();
}

где у Nat и его операций, у Eq, sym, cong, trans, n_plus_zero_eq_n, m_plus_one_plus_n_eq_one_plus_m_plus_n есть соответствующие определения (тоже требующие этих фич, но вполне пишущиеся).

Тут, кстати, видно почему запись ResultType f_name(ArgType) из C/C++/Java/C#... не Ъ и более удобна в перспективе (таких фич) запись f_name(ArgType) ResultType как в *ML/F#/Rust/Haskell/Scala/Agda/... (+ если учесть квантификации или implicits из Haskell или Scala/Agda — мы вводим имена на которые могут быть зависимости в типах слева на право, так что в сигнатурах можно обойтись вообще без свободных имён).

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

ооп и функциональщина кратко, внятно. (комментарий), суть в том, что мы можем распространить проверку типов со случаев вида factorial_5_eq_12_mult_10 (конкретная instantiation) до случаев a_plus_0_eq_a (для любых «a» сразу по факту написания такой программы, без instantiations) и fib1_eq_fib2 — проходить проверку будут строго типы которые соответствуют истинным (логическим) утверждениям (непротиворечивость с обоих сторон, так что за языком придётся следить).

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

У тбу есть GMP

есть. Какая разница, сколько бит в числе? 32 или 100500? И то и другое и близко не похоже на бесконечность. Т.е. ты не имеешь никакого права использовать значок ∀, ибо у тебя нет «памяти любого размера», а следовательно и «любого числа». Т.е. твоё доказательство неверно.

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

не. Тьюринг в хорошем смысле педераст (:

А я-то тут причём! :)

Т.е. твоё доказательство неверно.

Да ты офигел. Постоянно время от времени находится чувак которому нужно объяснять что такое индукция и что доказать что-либо для ∀ натуральных чисел можно не перебирая ∀ натуральных чисел. Тебе тоже это нужно рассказывать? Лучше разберись в вопросе прежде чем что-то отрицать — доказательство простое и корректное (собственно, другого и не написать, иначе какой смысл тогда в этих агдах и коках).

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

ты не имеешь никакого права использовать значок ∀, ибо у тебя нет «памяти любого размера», а следовательно и «любого числа». Т.е. твоё доказательство неверно.

Взбугагнул.

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

Тогда почему ты приписываешь ему то, чего он не говорил? Какие-то МТ с бесконечностями, которых у него не было?

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

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

А какого максимального размера есть память?

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

Он не в состоянии даже определение машины Тьюринга понять, а ты ему суешь агды и зависимые типы.

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

Т.е. ты не имеешь никакого права использовать значок ∀

Кстати интересно: в силу принципа переноса, любое истинное высказывание для натуральных чисел истинно и для гипернатуральных! Это значит, что если у нас было «для любого n из N блабла» (нечто выполняется для конечных чисел из N) то истинно и «для любого n из *N блабла» - нечто выполняется и для бесконечностей (которые входят в *N) в том числе.

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

А я-то тут причём!

а ты — в плохом. Во первых потому, что ты не подписываешься, потому спорить с тобой == спорить с дебилом, который во втором предложении опровергает себя же. Я то откуда знаю, кто из вас дебил, а кто — не дебил. Ну ладно если весь пост не по делу «твоя мать шлюха», тут всё ясно. А если что-то по делу, то хуже. Но приходится относится также, как к дебилам.

2 quasimoto извини, это не тебе было. Я промахнулся с цитированием, и хотел сама себе ответить.

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

Постоянно время от времени находится чувак которому нужно объяснять что такое индукция

я уже задолбался всем объяснять, что индукция сформулирована для любых натуральных чисел. Её можно обобщить на рациональные, на иррациональные, ещё на какие-то вещественные, однако бесконечность в них не входит (только косвенно, как их количество). А вот если ты решил таки обобщить, то это как-то особо надо делать...

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

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

А какого максимального размера есть память?

какое-то M. Любое. ЗАРАНЕЕ заданное. Т.е. ты сначала выбираешь некое M (любое), а потом уже доказываешь. И никак иначе. А если вылезаешь за M, то программа не корректна. Как и доказательство. Так вот доказательство Тьюринга основывается на том, что _любой_ алгоритм влезет в его машину. А это не так. Грубо говоря, МТ IRL остановится. Когда лента кончится. Не важно когда, важно — остановится.

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

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

О каком множестве ты говоришь?

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

Ну ТС предоставил две разных программы — каждая принимает по натуральному числу и возвращает по натуральному. Вопрос — они эквивалентны? То есть для равных аргументов возвращают равные значения? Можем пустить тест для _конечного_ числа случаев. Можем доказать эквивалентность для _всех_ натуральных чисел? Да, мы можем путём математических (на бумажке или формально в подходящем ЯП) рассуждений о структуре этих двух программ (в данном случае тупо по индукции — для нуля так-то, для шага перетасовываем выражения с обоих сторон равенства подходящими преобразованиями) придти к выводу об их эквивалентности, и это будет верно при правильности (модельное понятие) и непротиворечивости (внутреннее-логическое) нашей системы (то что делаем на бумажке или самого ЯП) — «можно проверять программы на эквивалентность» же. И если утверждения языка это некие выражения («числа») Pr и доказательства — тоже, Th, то они все конечны (как строки), любое из них доступно за конечное время (перечислением), вопрос в наличии алгоритма Verify(Pr, Th) -> Bool — такой алгоритм есть, он разрешим, это МТ, так что вопрос о количестве памяти тут к чему? Ещё можно порассуждать о минимальном размере этой машины для данной теории T.

В этой связи — зачем нам бесконечность в натуральных числах? А то я думал это был отдельный подтред, а сейчас мы снова про первый пост :)

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

Ты ничего толкового и полезного придумать не можешь, так как необразован.

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

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

О каком множестве ты говоришь?

не я, а некий гиперрациональный анонимус.

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

не я, а некий гиперрациональный анонимус.

Никто кроме тебя тут про бесконечности не говорил. Так о каком множестве с бесконечностями ты вел речь?

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

какое-то M. Любое. ЗАРАНЕЕ заданное.

Ну назови мне это M, если оно есть.

Т.е. ты сначала выбираешь некое M (любое), а потом уже доказываешь.

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

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

И это так и есть на практике.

А это не так.

Что значит, не так? Почему?

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

Грубо говоря, МТ IRL остановится. Когда лента кончится. Не важно когда, важно — остановится.

IRL проверка fib₁≡fib₂ заняла несколько секунд и съела несколько десятков мегабайт.

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

Чисто теоретически даже тот факт что проверка некого P займёт over 100500GB и лет не должен смущать — 1) по классу такое P ничем не отличается от fib₁≡fib₂ (с высоты Тьюринга с Гёделем, конечно), 2) это именно что теоретический трюк для установки такого класса, практически будут оптимизации и приемлемые времена и память для рассматриваемых задач.

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

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

ответ: да. Это можно доказать для любых целых чисел, заранее заданного размера. Т.е.

1. пусть числа будут из 100500 бит

2. собственно доказательство. В котором мы не вылезаем за эти 100500 бит.

А если вылезает — увы. Нас ждёт жопа и fuckup. Причём вовсе не только в теории, но и на практике. В качестве примера посчитай в float/double первые члены бесконечного знакопеременного ряда дающего ln(2). В прямом и в обратном порядке. Как видишь, от перемены местами слагаемых сумма ВНЕЗАПНО меняется. В теории это просто не получается по той простой причине, что мы не можем начать с конца. Мало того, мы и с начала начать не можем, потому-что первая разность у нас должна иметь точность как у последней. Т.е. теоретически занимать бесконечное число бит. Т.е. идеальный вычислитель не сможет выполнить первую итерацию за конечное время.

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

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

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

Не для «заранее заданного размера», а просто для любых. Точка.

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

А если вылезает — увы.

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

float/double

Мы говорим про тип натуральных чисел.

в бесконечных рядах нельзя действовать как в конечных

Мы говорим про ряд натуральных чисел. [2]

С обычной индукцией, да.

бесконечные алгоритмы

Аааа :)

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

IRL проверка fib₁≡fib₂ заняла несколько секунд и съела несколько десятков мегабайт.

это тебе повезло, т.к. сложение(умножение) по модулю ассоциативно. Однако то, что в C/C++ называется «делением» — увы.

5*56/12=2
5/12*56=0
(mod128)

Мы видим, что наши числа составляют кольцо, но НЕ поле. Что-бы быть полем, нам нужно переделать умножение так, что-бы оно стало полем Галуа. Вот тогда деление станет ассоциативным, и всё будет чудесно(с т.з. логики. Но если кто-нить увидит такое «умножение», шаблон ему порвёт напрочь. Типа 2*2==1(GF3), 2**8==29(GF256))

Т.о. те числа, которые у нас есть, на самом деле натуральными НЕ являются. Они «натуральные» только пока мы близко не подойдём к модулю.

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

Мы говорим про тип натуральных чисел.

ну нету такого типа. Есть тип «целые по модулю M». Причём результат совпадает тогда, и только тогда, когда сомножители <<M. Если сомножители одинаковые, то они должны быть < sqrt(M), что-бы разок перемножить.

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

ага. «нет». На самом деле — есть.

Аааа

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

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

это тебе повезло, т.к. сложение(умножение) по модулю ассоциативно.

Нет, там есть тип для натуральных чисел. Нет никаких сложение(умножение) по модулю. В GMP их тоже нет.

Однако то, что в C/C++ называется «делением»

А почему мы должны говорить про C/C++ и его типы фиксированной точности? По крайней мере, до переполнения они ведут себя как и натуральные числа, все свойства работают. А если нужно изучать именно их финитные кольца — пожалуйста, только это не то что просил TC (он не просил доказать эквивалентность «в расчёте на то что эти программы работают на переполняющихся числах фиксированной точности такой-то битности»).

ну нету такого типа

Ну есть такой тип. В математике, в сущностях предметных областей (чтобы не радоваться как size_t считает «количества» по кругу) и программных реализациях. А ещё есть тип «положительные чётные числа больше 4 и меньше 40».

На самом деле — есть.

Как это? С одной стороны доказательства об эквивалентности программ с точки зрения _семантики языка_, можем мерить в блокнотных листах, с другой — битности чисел. Можно доказать некую теорему про все финитные кольца — столько-то блокнотных листов, она будет работать для чисел любой битности. Или выше пруф про Фибоначчи — несколько строк, а сами натуральные числа могут отжирать в памяти сколько угодно. Никакой корреляции (константа vs что угодно).

Если ты вводишь «бесконечные числа»

Я их нигде не ввожу.

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

Нет, там есть тип для натуральных чисел.

где это «где-то там»?

В GMP их тоже нет.

я в курсе. Есть ещё bc, есть common lisp. Там тоже числа «бесконечные». Но это так только на первый взгляд, на самом деле размер числа растёт настолько быстро, что очень скоро вешается _любой_ реальный вычислитель. На практике часть информации отбрасывают, например представляя результат рациональным числом по модулю 2^23 например (float IEEE754). А как я выше показал, это уже не поле. И даже не кольцо(для float). Мало того, кольцо int'ов вовсе НЕ является кольцом целых.

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

вот именно. Потому для доказательства совпадения алгоритмов просто совпадения в математическом плане недостаточно. Ещё нужно доказать отсутствие переполнения, причём НА ВСЕХ этапах, для ВСЕХ чисел.

А ещё есть тип «положительные чётные числа больше 4 и меньше 40».

есть. Только это тоже не кольцо, и тем более не поле. Потому все свои аксиомы можешь отложить в сторону.

Как это?

число бит в числе == информация. Так вот рост этой информации вовсе НЕ линейный. Он линейный только при сложении. При умножении он уже растёт как геометрическая прогрессия, и потому весьма быстро засирает любую реальную память. А нереальную — да, не засирает конечно, вот только её нет.

К тому же ты упрямо забываешь про неопределённость. В конечных множествах она сплошь и рядом. Т.е. если перемножить два любых натуральных числа, то у тебя произведение будет ВСЕГДА натуральным числом больше нуля(ноль я натуральным не считаю). При умножении по модулю это не так — у нас полно нулевых произведений получается. А стало быть — у нас множество делителей нуля. Что с ними делать в рамках твоей теории чисел основанной на аксиомах Пеано — я не понимаю.

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

Вот тогда деление станет ассоциативным

Это же просто песня! На цитаты разбирать можно!

что-бы оно стало полем Галуа.

Не упоминай поля Галуа и вообще алгебраические структуры, пожалуйста. Ты в них ни бум-бум.

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

Мало того, кольцо int'ов вовсе НЕ является кольцом целых.

а unsigned inti'ов вполне является, представь себе.

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

Ещё нужно доказать отсутствие переполнения, причём НА ВСЕХ этапах, для ВСЕХ чисел.

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

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

Не упоминай поля Галуа и вообще алгебраические структуры, пожалуйста.

тебя в детстве по жопе били, до сих пор болит? Или сейчас тоже бьют?

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

а unsigned inti'ов вполне является, представь себе.

да ладно? А делители нуля что в кольце делают? 2*2==0(mod4)

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

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

о том и речь. Потому-что в теории хоть 100500 терабайтов можно выделить и засрать. А на практике — увы. У меня вот здесь всего 1 гиг. И 1 гиг это вовсе не так много, как ты думаешь(если посчитать что-нить в GMP например, или на clisp'е, или самому свои большие числа накостылять).

Это только кажется что «много».

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

А делители нуля что в кольце делают?

Присутствуют. Представь себе, кольца с делителями нуля - это вполне обычное явление. Например, любое кольцо классов вычетов по непростому модулю (к которому и относится unsigned int) - имеет делители нуля.

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

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

Потому-что в теории хоть 100500 терабайтов можно выделить и засрать.

На практике как раз так и есть, да.

У меня вот здесь всего 1 гиг.

А на другом компьютере не 1 гиг, а 2. А можно взять и доставить оперативку на ходу.

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

где это «где-то там»?

Конкретно я написал на Agda2. Ну и в других подобных языках есть такой тип в удобном (в математическом смысле) виде.

вот именно

Ну вот. А желателям помучить сишку можно посмотреть на книжку EoP и в сторону верификаторов для сишки (там и фиксед поинт и флоат будет).

Только это тоже не кольцо, и тем более не поле. Потому все свои аксиомы можешь отложить в сторону.

Что с ними делать в рамках твоей теории чисел основанной на аксиомах Пеано — я не понимаю.

Так ты не перекладывай с одного на другое — есть N, Z/nZ, {4, 6, ..., 40}, три разных типа, три разных набора аксиом и разные свойства. Была продемонстрирована эквивалентность двух функций на N, любые другие подобные эквивалентности и свойства на других типах доказываются аналогично.

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

Присутствуют. Представь себе, кольца с делителями нуля - это вполне обычное явление. Например, любое кольцо классов вычетов по непростому модулю (к которому и относится unsigned int) - имеет делители нуля.

я знаю, что они присутствуют.

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

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

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

Потому-что в теории хоть 100500 терабайтов можно выделить и засрать.

На практике как раз так и есть, да.

на практике нет даже одного.

А на другом компьютере не 1 гиг, а 2. А можно взять и доставить оперативку на ходу.

я рад за тебя, но у меня нет такой возможности.

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

Конкретно я написал на Agda2. Ну и в других подобных языках есть такой тип в удобном (в математическом смысле) виде.

к сожалению, такого типа нет, и быть не может.

Его можно сделать например в C++, вот только ничего полезнее самого себя оно не докажет.

Так ты не перекладывай с одного на другое — есть N, Z/nZ, {4, 6, ..., 40}, три разных типа, три разных набора аксиом и разные свойства. Была продемонстрирована эквивалентность двух функций на N, любые другие подобные эквивалентности и свойства на других типах доказываются аналогично.

я не понимаю, как эквивалентность на N обобщается на конечное множество с достижимой бесконечностью? Мне даже умножение не обобщить, так, что-бы множество стало хотя-бы полем.

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

да я прекрасно знаю эти факты

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

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

Аксиомы кольца как были правильными, так и остались правильными, представь себе.

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

я рад за тебя, но у меня нет такой возможности.

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

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

я не понимаю, как эквивалентность на N обобщается на конечное множество с достижимой бесконечностью?

Нету никакой достижимой бесконечности. Откуда ты ее вырыл, ты ответишь?

Мне даже умножение не обобщить, так, что-бы множество стало хотя-бы полем.

Тебе - не обобщить, а математики спокойно обобщают и пользуют поля с бесконечностями.

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

такого типа нет, и быть не может

Натуральных чисел не существует? Или программных реализаций? Или они не удобны в «математическом смысле»?

Второе — http://en.wikipedia.org/wiki/Arbitrary-precision_arithmetic, ну и Кнута же ты читал. Третье — всего лишь вопрос компиляции из «удобного» представления в эффективное, не вижу проблем.

конечное множество с достижимой бесконечностью

Я не знаю что это такое, зачем оно нам и откуда влезло в разговор.

Ну и я сказал — не обязательно обобщать, если у тебя есть некая структура со своими начальными аксиомами, то всегда можно доказать любые её свойства (и память/время затрачиваемые доказателем конечны (обычно практически не велики), константы для данного утверждения (с доказательством) и никак не коррелируют с памятью/временем которую тратят программы о которых проводятся доказательства). Например ещё — http://toccata.lri.fr/gallery/index.en.html, это консервативный подход. Вообще, любой язык с семантикой предполагает возможность экстракции программ в семантические домены, то есть в некие математические структуры о которой можно проводить рассуждения математическими же средствами (какая-та FOL, Coq и т.п.), доказывая свойства программ.

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

Кстати

>>> def fib1(n):
...     a, b = 0, 1
...     for _ in range(n):
...         a, b = b, a + b
...     return a
... 
>>> fib1(5000)
3878968454388325633701916308325905312082127714646245106160597214895550139044037097010822916462210669479293452858882973813483102008954982940361430156911478938364216563944106910214505634133706558656238254656700712525929903854933813928836378347518908762970712033337052923107693008518093849801803847813996748881765554653788291644268912980384613778969021502293082475666346224923071883324803280375039130352903304505842701147635242270210934637699104006714174883298422891491273104054328753298044273676822977244987749874555691907703880637046832794811358973739993110106219308149018570815397854379195305617510761053075688783766033667355445258844886241619210553457493675897849027988234351023599844663934853256411952221859563060475364645470760330902420806382584929156452876291575759142343809142302917491088984155209854432486594079793571316841692868039545309545388698114665082066862897420639323438488465240988742395873801976993820317174208932265468879364002630797780058759129671389634214252579116872755600360311370547754724604639987588046985178408674382863125L

а ты говоришь по модулю.

Вот с точки зрения семантики питона, как я понимаю, это две разные программы дающие одну и ту же функцию (с точки зрения денотационной семантики), что доказывается — соответствующие рекурсивные функции равны экстенсионально.

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

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

ты просто идиот. Я говорю про РЕАЛЬНЫЕ вычислители, и про реальные множества вроде чисел int. А ты мне тут тыкаешь в свой учебник математики, который совсем о других множествах.

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

Ну и я сказал — не обязательно обобщать, если у тебя есть некая структура со своими начальными аксиомами, то всегда можно доказать любые её свойства (и память/время затрачиваемые доказателем конечны (обычно практически не велики)

ну «обычно» не велики. Никто не дал тебе право обобщать твоё «обычно» на всё. Тут нужно дополнительное исследование.

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

ага. Но только в фантазиях теоретика это возможно.

На практике — увы, приходится упрощать и/или округлять. Даже если ты Кнут. Строго можно доказать лишь очень небольшое множество утверждений и алгоритмов. Вот пример в первом посте например. Ты неявно пользуешься аксиомами Пеано, и правильно ведь делаешь, ибо числа в питоне составляют кольцо. Другое, не такое как обычное кольцо, но если не приближаться к модулю, то разницы нет. Потому-то всё и работает. В этом, одном из 3.5 тривиальных случаев.

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

существуют. НЕ все.

Какое негодное у тебя IRL, даже натуральных чисел толком нет :)

Никто не дал тебе право обобщать твоё «обычно» на всё.

Ну так примеры когда они велики — в студию.

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

Натуральные числа не составляют кольца. Так что с Пеано мимо (хотя я их использовал и даже вполне явно).

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

Нет там никакого модуля — как статически доказать эквивалентость двух произвольных алгоритмов (комментарий).

В этом, одном из 3.5 тривиальных случаев

http://toccata.lri.fr/gallery/index.en.html — явно > 3.5, и это только одна конкретная ссылка.

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

Почему мимо:

>>> fib1(-2)
0
>>> fib2(-2)
-2

то есть доказательство о полукольце натуральных чисел с использованием PA никак не распространяется на кольцо целых — это нам нужно взять «ту же» программу и заменить в ней все числа и операции на другие (в питоне они перегружены), от другой структуры, естественно, что всякая эквивалентность может исчезнуть (в случае замены на фиксированную арифметику или плавающую — тоже).

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

Какое негодное у тебя IRL, даже натуральных чисел толком нет

у тебя не лучше.

Ну так примеры когда они велики — в студию.

возьми любой алгоритм, который Кнут не осилил разобрать аналитически. Там много (:

Натуральные числа не составляют кольца. Так что с Пеано мимо (хотя я их использовал и даже вполне явно).

пусть будут целые. Без разницы. А числа в компьютере кольца составляют. И unsigned тоже. Только другие.

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

Нет там никакого модуля

это ты так думаешь.

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

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

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

пусть будут целые. Без разницы. А числа в компьютере кольца составляют. И unsigned тоже. Только другие.

Но на целых fib1 и fib2 не эквивалентны. Есть разница. N не составляет кольца :( — GMP правильно реализует N, Z и Q, так что не надо рассказывать, что типа N не существует. signed с unsigned (8, 16, ...) — да, но ими «числа в компьютере» не ограничиваются. Такие кольца называются финитные кольца, точнее кольцами классов вычетов — Z/nZ (между signed и unsigned есть изоморфизм колец в случае two's complement путём переименования чисел).

это ты так думаешь

Ты же видишь, что в питоне длинная арифметика — модуля нет.

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

Интерпретатора питона нету?

Это, очевидно, результаты работы рекурсивных функций из топика (fib1(n) = go(0, 1, n); go(a, b, n) = n <= 0 ? a : go(b, a + b, n - 1) и fib2(n) = n < 2 ? n : fib(n-1) + fib2(n-2)) на Z (в питоне они на нём определены, в том числе — как и на float и т.п.) — на Z же определены операции <, <=, - и + и числа 0, 1 и 2.

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

Я говорю про РЕАЛЬНЫЕ вычислители, и про реальные множества вроде чисел int.

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

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

существуют. НЕ все.

Можешь привести приме натурального чеисла, которого не существует?

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

но если не приближаться к модулю

У чисел питона нету никакого модуля, ебанько. К чему ты собрался «не приближаться»?

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

Такие кольца называются финитные кольца, точнее кольцами классов вычетов

Ну не все конечные кольца являются кольцами классов вычетов.

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

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

ты слишком многого просишь от простого быдлокодера.

пусть будут целые. Без разницы. А числа в компьютере кольца составляют. И unsigned тоже. Только другие.

Но на целых fib1 и fib2 не эквивалентны.

да и ладно. Разве они вообще смысл имеют?

GMP правильно реализует N, Z и Q

только теоретически.

кольцами классов вычетов

я в курсе, как оно называется. Заметь — это кольца, а не поля. Причём совсем другие.

Ты же видишь, что в питоне длинная арифметика — модуля нет.

ЕМНИП только с целыми так. Рациональные — увы. Нету ЕМНИП. А с целыми — без разницы, кольцо не нужно, там можно только складывать. А складывать я могу и в сишечке в uint64_t. Мне не дожить до переполнения (: Зачем в питоне такие — для меня загадка.

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

Можешь привести приме натурального чеисла, которого не существует?

никакой вычислитель с памятью в N бит не сможет досчитать до 2**N.

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

Но досчитает вычислитель с памятью n+1 бит. Итого: для любого числа найдется вычислитель, который до него досчитает. Значит, все натуральные числа существуют.

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

Но досчитает вычислитель с памятью n+1 бит. Итого: для любого числа найдется вычислитель, который до него досчитает.

не верно. Существование вычислителя с n+1 битами ты не доказал.

В том вычислителе, на котором я пишу, имеется как минимум 8 514 437 120 бит памяти, как это доказывает существование компьютера с 8 514 437 121 битами?

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

В том вычислителе, на котором я пишу, имеется как минимум 8 514 437 120 бит памяти, как это доказывает существование компьютера с 8 514 437 121 битами?

Никак не доказывает, очевидно. А должно? Зачем?

Существование вычислителя с n+1 битами ты не доказал.

Это эмпирический факт, мы его получаем из наблюдений.

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

Ну и на самом деле ты врешь. Я сомневаюсь, что жесткий диск в твоем вычислителе всего на 8 514 437 120 бит.

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

Никак не доказывает, очевидно. А должно? Зачем?

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

Это эмпирический факт, мы его получаем из наблюдений.

я не наблюдаю компьютеров с резиновой памятью.

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

Ну и на самом деле ты врешь. Я сомневаюсь, что жесткий диск в твоем вычислителе всего на 8 514 437 120 бит.

у меня нет никакого «жёсткого диска». Есть флешка в 8Гб, но хранить там данные программ нельзя(места нет, и медленно). А ещё эту флешку можно выдрать прямо на ходу, и всё будет работать как не в чём не бывало (она нужна только для загрузки и бекапов)

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

signed не кольцо

В случае two's complement signed с unsigned это коды для одного и того же кольца. Но стандарт не обязывает signed быть дополнительным кодом, да, хотя это 99% будет именно так (и инструкции под оба типа будут одни и те же).

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

ты слишком многого просишь от простого быдлокодера

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

Разве они вообще смысл имеют?

Семантику? Ну да :)

только теоретически

$ grep 'i.e. N' /usr/include/gmp.h
/************ Low level positive-integer (i.e. N) routines.  ************/

Плюс подходящий класс легко пишется на основе любой длинной арифметики.

Или ты про то что памяти не хватит?

Это и есть «только теоретически» — в теории не хватит, а ниже ты пишешь, что тебе и uint64_t хватает.

Давай тогда говорить, что и массивов, связных списков, хеш таблиц, да и вообще структур данных не существует (точнее «существуют. НЕ все.»).

И «активная» (по отношению к вычислению) память это не обязательно ОЗУ, взять тот же mapreduce (там может быть достаточно много памяти).

кольца

поля

Рациональные

Слишком много всего :) Я не совсем понял к чему (зачем нам вообще рациональные, кольца, поля, делимость — нам же не свойства а потом вещи нужны, а сначала вещи, потом их свойства).

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

Я говорю довольно простую вещь — компиляция (верификация доказательства относительно утверждения это тоже её часть)

да ладно. Откуда там верификация? Компиляция — просто отображение алгоритма с одного вида в другой. Ошибочная программа корректно скомпилируется и будет некорректно работать.

Отсутствие каких-то программ (или док-в у Кнута) никак не противоречит тому что существующие вполне успешно компилируются (верифицируются).

у тебя странная логика: возьми сортировку qsort и вставки. Они разве эквивалентны? Нет. Однако обе дают одинаковый результат и обе компилируются. И что это доказывает?

Это и есть «только теоретически» — в теории не хватит, а ниже ты пишешь, что тебе и uint64_t хватает.

это смотря для чего. Для чисел Фибоначчи — да, хватает, они отлично влазят в uin64_t, не сложно это доказать. А вот для чего-то другого — увы, ответ «не известно». И нет никакой возможности это доказать и опровергнуть.

Давай тогда говорить, что и массивов, связных списков, хеш таблиц, да и вообще структур данных не существует (точнее «существуют. НЕ все.»).

структуры существуют, но они КОНЕЧНЫ. И числа тоже существуют, и тоже КОНЕЧНЫ. И не важно, какое именно на них наложено ограничение, важно что наложено, и не одно. Это не только и не столько 64 бита разрядной сетки твоего CPU, с ним как раз всё просто.

Кроме очевидного ограничения по времени (мне твоё доказательство, которое работает сто лет, нафиг не нужно), есть ещё и ограничение по точности. Целые/рациональные числа бесконечно точные, т.е. при любом N ты смело пишешь N<N+1, да? А если у тебя N занимает всю память твоего компьютера, что ты будешь делать? С рациональными так вообще беда, ибо даже ответ на вопрос, сколько содержится информации в R+1 уже не совсем ясен, и не совсем тривиален(если считать грубо, то число информации растёт линейно с каждым инкрементом, т.е. R+1 тыщу раз на 1000 бит длиннее. На практике не на 1000, а меньше. А на сколько меньше — я без понятия. В любом случае — линейно, хоть и не на 1 бит. Попробуй посчитай, а то у меня мозгов мало :)

И «активная» (по отношению к вычислению) память это не обязательно ОЗУ, взять тот же mapreduce (там может быть достаточно много памяти).

сколько волка не корми, а у слона всё равно больше. Если не веришь, разложи на простые множители число в 128 бит. Там пофиг, сколько у тебя ДЦ.

Слишком много всего :) Я не совсем понял к чему (зачем нам вообще рациональные, кольца, поля, делимость — нам же не свойства а потом вещи нужны, а сначала вещи, потом их свойства).

ну нету у нас таких «вещей», смирись. Есть некое КОНЕЧНОЕ множество объектов(чисел), и свойства этого множества очень сильно отличаются от свойств бесконечного множества.

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

Откуда там верификация?

Верификация это проверка типов (* может быть проверкой типов).

Ошибочная программа корректно скомпилируется и будет некорректно работать.

В бедном языке. В достаточно выразительном — не скомпилируется.

Они разве эквивалентны?

С точки зрения денотационной семантики — да. С точки зрения операционной — нет. Вопрос ТС был про денотационную. В математике есть понятие о равенстве функций, называется экстенсиональное равенство (extensional equality). Вот разные fib и sort «равны» если дают одинаковые результаты — реализуют одну и ту же функцию (одна семантика, но разные программы, алгоритмы, сложности, операции).

И что это доказывает?

Что они эквивалентны modulo extensional equality? В математике есть понятие об отношении вообще и отношении эквивалентности в частности :)

они отлично влазят в uin64_t, не сложно это доказать

fib(100) > 2 ^ 64.

мне твоё доказательство, которое работает сто лет, нафиг не нужно

Ты о каком доказательстве сейчас говоришь?

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

Извини, не сталкивался :)

Ну и всё относительно же — сколько там байт «хватит всем»?

Есть некое КОНЕЧНОЕ множество объектов(чисел), и свойства этого множества очень сильно отличаются от свойств бесконечного множества.

Ну это тоже «вещь». Я о том что любая непротиворечивая хрень, сколь бы странной она не была, имеет модель (теорема о _полноте_, кстати :)). Всегда можно проводить рассуждения, причём вполне эффективно — формально или нет (а то тебя смущают какие-то бесконечности, и какие-то доказательства по сто лет проверяются).

Ну и я так и не понял чем плохи бесконечные типы GMP и разных ЯВУ (понятно, что есть вопрос производительности).

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

я не наблюдаю компьютеров с резиновой памятью.

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

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

у меня нет никакого «жёсткого диска».

А у меня есть.

Есть флешка в 8Гб, но хранить там данные программ нельзя(места нет, и медленно).

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

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

С точки зрения денотационной семантики — да. С точки зрения операционной — нет.

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

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

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

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

Ошибочная программа корректно скомпилируется и будет некорректно работать.

В бедном языке. В достаточно выразительном — не скомпилируется.

значит ты говнокодер (:

С точки зрения денотационной семантики — да. С точки зрения операционной — нет. Вопрос ТС был про денотационную

даже с этой т.з. так можно доказывать лишь эквивалентность тривиальных алгоритмов.

fib(100) > 2 ^ 64.

вот именно. А значит я ВСЁ множество могу тупо перебрать за конечное время.

А вот если у меня две сортировки массива целых uint8_t в 10 элементов, то это всего навсего 12778 лет, если за 1 секунду проверять 3 миллиарда вариантов. Т.ч. перебор тут не прокатит, а ничего другого нет даже у самого Кнута.

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

Извини, не сталкивался

столкнёшься. Причём намного раньше, чем ты это ожидаешь.

Ну и я так и не понял чем плохи бесконечные типы GMP и разных ЯВУ (понятно, что есть вопрос производительности).

размер и время СЛИШКОМ быстро растёт.

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

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

ну будет не 12 тысяч лет, а 12 миллионов лет. Действительно — не имеет значения.

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

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

Это смотря какая. Можно и операционную и денотационную задать так, что время и память будет считаться. А можно и ту и ту задать так, что не будет.

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

ну будет не 12 тысяч лет, а 12 миллионов лет.

И что дальше? С моей точки зрения совершенно безразлично: 12 тысяч или 12 миллионов.

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

С моей точки зрения совершенно безразлично: 12 тысяч или 12 миллионов.

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

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

Т.е. ничего не доказывает, и ничего не опровергает.

Как же не доказывает? Вполне доказывает. Что задача может быть решена за конечное время. То, что тебе такой факт неинтересен - это исключительно твои половые проблемы.

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

значит ты говнокодер

Потому что некорректная программа не компилируется? Как-то не уловил логику :)

А значит я ВСЁ множество могу тупо перебрать за конечное время

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

так можно доказывать лишь эквивалентность тривиальных алгоритмов

Почему, вполне нетривиальные и сложные свойства можно доказывать, если руками, это автоматически нельзя в общем случае (http://en.wikipedia.org/wiki/Rice's_theorem, там же про понятие тривиальности).

столкнёшься

А ты сталкивался? Какие у тебя числа были что GMP (или что) делал очередную аллокацию настолько большого размера?

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

Потому что некорректная программа не компилируется? Как-то не уловил логику

ну некорректность-то в алгоритме. Каким образом компилятор обнаружит, что я вместо a+b написал a-b?

речь была про вполне реальные возможности формальных доказательств нетривиальных свойств программ.

любое доказательство опирается на аксиомы. К примеру есть аксиома утверждающая, что если есть n, то есть и n+1, при этом n<n+1 для любого n. И она НЕ выполняется для uint32_t. Также и другие аксиомы ломаются. Потому все твои доказательства годные для целых(например) чисел, становятся негодными для доказательства эквивалентности алгоритмов.

В смысле посчитать Фибоначчи в границах uint64_t за приемлемое время?

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

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

можно. Но только руками, и очень осторожно, помня о том, что любая аксиома может быть поломанной.

А ты сталкивался? Какие у тебя числа были

сталкивался. Числа сами по себе очень небольшие могут быть, например рациональные дроби. Это только кажется, что числа растут медленно, на самом деле это не так — если ты ограничиваешь величину чисел, то растёт требуемая точность, причём экспоненциально. Грубо говоря, одна операция увеличивает энтропию(число бит) вдвое, и уже через пару-тройку десятков операций память исчерпывается.

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

вот как раз для чисел Фибоначчи можно доказать, что множество uint64_t эквивалентно кольцу натуральных чисел(слово «кольцо» я условно использовал, т.к. вообще говоря множество натуральных не закольцовано по вычитанию, однако вычитать ничего нам не нужно)

Еще одна песня. Одна охуительнее другой. Продолжай радовать нас своими математическими открытиями и дальше.

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

при котором память кончится.

А как она может кончиться, если я всегда могу добавить еще? Докажи, что она обязательно закончится.

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

Каким образом компилятор обнаружит, что я вместо a+b написал a-b?

Я же говорю — с помощью проверки типов. Типы это утверждения, а программы — их доказательства, то есть существуют такие системы типов в которых типы настолько же выразительны как и произвольные логические утверждения, доказательства осуществляются самими программами (proof carrying code), а проверка типов эквивалентна верификации доказательств.

Обратно — можешь взять типы C++ (struct unit {}; bool, int, ..., std::tuple/структуры, boost::variant/наследование, std::function/функции, шаблонные функции) и подумать каким логическим утверждениям они могут соответствовать, каким доказательствам соответствуют программы и как это проверяется.

Возьмём эту программу — как статически доказать эквивалентость двух произвольных алгоритмов (комментарий). Чуть ниже я написал её аналог на псевдо-плюсах (расширенных dependent types). Эта программа компилируется. Заменим в ней + на - или на *, или прибавим 1 где-нибудь и т.п. — она перестанет компилироваться.

Аналогично можешь взять что-нибудь из http://toccata.lri.fr/gallery/index.en.html (там вместо расширения системы типов логическая настройка поверх — то что в комментариях находится) и попробовать там где-нибудь изменить ненавязчиво алгоритм — верификацию (ещё до компиляции) не пройдёт.

Потому все твои доказательства годные для целых(например) чисел, становятся негодными для доказательства эквивалентности алгоритмов.

Они годны для алгоритмов которые работают с целыми числами. Приведённый код на питоне работает с целыми числами. Точно такой же код на C++ с gmpxx будет с ними работать (и по виду не отличаться от кода с fixed point числами). Никаких uint32_t тут нет, вот я про них ничего и не доказываю. Хочешь алгоритмы которые работают с uint32_t — пиши их и доказывай про них. Точно так же. Никаких проблем.

вот как раз для чисел Фибоначчи можно доказать, что множество uint64_t эквивалентно кольцу натуральных чисел

Дык fib(100) же не влезает в uint64_t или я чего-то не понял? То есть для натуральных один результат, а с uint64_t — другой. Хм?

Но только руками, и очень осторожно

А http://en.wikipedia.org/wiki/Computer-assisted_proof это ещё в большей степени руками и очень осторожно.

любая аксиома может быть поломанной

Ага, на полном серьёзе будем доказывать факты про uint64_t используя аксиомы Пеано, типа как строить подводную лодку для полёта на Марс — ничего не может быть поломано, просто в здравом уме у тебя не получится перепутать две совсем разные структуры и доказывать что-то об одной используя теорию другой (это вообще технически нереально).

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

Ага, на полном серьёзе будем доказывать факты про uint64_t используя аксиомы Пеано, типа как строить подводную лодку для полёта на Марс

На самом деле не все так плачевно. Для uint64_t единственная аксиома арифметики Пеано, которая не выполняется - это то, что «не существует x: inc(x) = 0», то есть числа предшествующего нулю. С остальными аксиомами все в порядке и мы смело можем их использовать. Вообще говоря, любое кольцо классов вычетов будет моделью для такой аксиоматики Пеано (без этой аксиомы).

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

В плане библиотек натуральных чисел от Agda/Coq (а там же куча уже готовых пруфов для них) от этой аксиомы никак не избавиться, так что как-то проблематично рассуждать о программах с переполнениями не построив для начала теорию для uint64_t и т.п. вместо N.

Хотя с fib1 и fib2 прикол в том, что эквивалентность на uint*_t следует из эквивалентности на N :)

За более общий случай нужно смотреть насколько хитро может себя вести переполнение.

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

так что как-то проблематично рассуждать о программах с переполнениями не построив для начала теорию для uint64_t и т.п. вместо N.

Так чего строить-то? Теория uint64_t тривиально вкладывается в Natural.

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

Хотя с fib1 и fib2 прикол в том, что эквивалентность на uint*_t следует из эквивалентности на N :)

Вообще, интуитивно, модель N для нашей «усеченной Пеано» можно построить как ультрапроизведение соответствующе подобранных конечных колец, ну а дальше по теореме Лося можно сделать вывод о том, что множество истиных на интерпретациях формул совпадает.

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

А обратно?

А то как — теория для N есть. Но её утверждения на Z_n не перенести. То есть перенести, например, forall (n : N). f(n) = g(n) если f и g такие, что соответствующие f' и g' на Z_n имеют свойство forall (n : Z_n). f'(n) = mod(f(toZ(n)), n), как эти fib-ы. Но не вообще.

А теория для Z_n где? Какой модуль подключать, типы, конструкторы, леммы где?) Вкладывать неоткуда.

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

А теория для Z_n где?

А зачем? :)

То есть перенести, например, forall (n : N). f(n) = g(n) если f и g такие, что соответствующие f' и g' на Z_n имеют свойство forall (n : Z_n). f'(n) = mod(f(toZ(n)), n), как эти fib-ы.

Это не утверждение арифметики Пеано. В частности, в арифметике Пеано нету N, нету отношения принадлежности, нету Z_n.

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

А зачем?

По идее можно образовать подтип ℤ/_ℤ n = Σ[ x ∈ ℕ ] x < n и определить операции этого кольца, после чего будет подобно рассуждениям про ℕ (так как сводится к ℕ), но с кучей нудных доказательств фактов о делимости. Ещё есть Fin n изоморфный такому ℤ/ n ℤ, но, наверно, менее удобный.

Это не утверждение арифметики Пеано.

К чему лишний формализм? Допустим, это утверждения теории типов, первое (x : ℕ) → f x ≡ g x внутри PA запишется как ∀ x. f(x) = g(x). Нам интересно можно ли подменить относительно кода f и g типы и операции c ℕ на ℤ/nℤ для некого n и получить (теория типов) (n : ℕ) (x : ℤ/ n ℤ) → f' x ≡ g' x / (теория данного кольца ℤ/nℤ) ∀ x. f'(x) = g'(x) for free. Можно, если f, f', g и g' обладают свойствами (теория типов) (n : ℕ) (x : ℤ/ n ℤ) → toℕ (f' x) ≡ f (toℕ x) % n × toℕ (g' x) ≡ g (toℕ x) % n (утверждение метатеоретическое относительно воображаемых теорий, так что позволяет говорить о том как они по отношению друг к другу), так что перенесли f ≡ g из ℕ в f' ≡ g' из ℤ/nℤ для такого рода функций.

З.Ы. есть сорт, в случае one-sorted нет смысла его прописывать вместе с принадлежностью, но в случае пары one-sorted теорий — вполне, для различия.

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

К чему лишний формализм?

Как к чему? Если речь о сравнении двух теорий, то надо совершенно точно представлять какая что содержит.

Допустим, это утверждения теории типов

В какой теории типов? эта теория типов содержит арифметику? Если содержит - то и аксиому арифметики Пеано о непредшествовании нуля она содержит, а значит толку от нее?

теория данного кольца ℤ/nℤ

Бывает теория кольца (общая), а конкретные кольца являются моделями этой общей теории, а не теориями сами по себе. В рамках теории колец можно выводить только те утверждения, которые верны _для любого_ кольца (то есть истины на любой интерпретации, ну, понятно, полагаем, что теория непротиворечива).

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

По идее можно образовать подтип ℤ/_ℤ n = Σ[ x ∈ ℕ ] x < n и определить операции этого кольца, после чего будет подобно рассуждениям про ℕ (так как сводится к ℕ)

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

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

Теория моделей там ->

Зачем тут это воспроизводить?

В какой теории типов?

Которая большими буковками Теория Типов (по крайней мере, в некоторой литературе). Но в данном контексте не важно что за метатеория ZF+... / CZF+... / MLTT+..., речь о _метатеории_ в рамках которой можно формулировать другие теории и модели (заниматься теорией моделей).

аксиому арифметики Пеано о непредшествовании нуля она содержит, а значит толку от нее?

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

Например, теория — https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Structures.agda#L83. Её теоремы — https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Properties/Group..... Модель — https://github.com/agda/agda-stdlib/blob/master/src/Data/Integer/Properties.a....

PA (PA++ :)) себе так же можно сделать и взять стандартный \bn за модель. Как и Unsigned : NumberOfBit -> Set — если хочешь рассуждать про такой тип (~ Z/(2^n)Z, да) и такие программы (с переполнениями), то для начала нужно его проговорить, вместе со всем сопутствующим, что предполагает соответствующую теорию, явно или нет. Или лучше не нужно — все эти вещи могут быть неявными, но вполне очевидными.

Естественно, всё в контексте именно компьютерной формализации.

конкретные кольца являются моделями этой общей теории, а не теориями сами по себе

Я имею полное право строить себе теории Z/5Z и т.п. К примеру, теорию для uint64_t, или сразу Z/nZ для всех натуральных n. Но вовсе не общую теорию колец.

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

Сходи сделай («статически доказать, что приведённые fib1 и fib2 эквивалентны на uint*_t»).

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

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

Аксиоматика Пеано без соответствующей аксиомы - наша теория. Что тут еще проговаривать, мне непонятно?

Я имею полное право строить себе теории Z/5Z

Ну можешь, конечно, но зачем? Да и при непростом n аксиоматика у нее будет кривоватая.

Но вовсе не общую теорию колец

Я говорил не о теории колец, а о теории кольца :)

В теории колец у нас есть все кольца, их гомоморфизмы и т.д. - ну, в общем, все, что есть в соответствующей категории - любая диаграмма будет высказыванием данной теории. А теория кольца (произвольного) - это ЛПП+аксиомы кольца. При этом что у нас за кольцо конкретно мы не знаем, но можем уточнить, добавляя еще аксиом (например, n+n+n+n+n=0, получаем Z_5)

Сходи сделай («статически доказать, что приведённые fib1 и fib2 эквивалентны на uint*_t»).

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

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

Я говорил не о теории колец, а о теории кольца

Да, вот такая теория (кольца?) — https://github.com/agda/agda-stdlib/blob/master/src/Algebra.agda#L336. При конструировании очередной конкретной модели нужно передать её конструктору множество (тип, на место Carrier), операции и доказать, что они соответствуют аксиомам. Вместо ЛПП — теория типов.

С другой стороны, на этой же структуре определяется гомоморфизм — https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Morphism.agda, так что Ring является коллекцией объектов, а _-Ring⟶_ — морфизмов категории Ring (можно сделать моделью другой теории из https://github.com/copumpkin/categories/blob/master/Categories/Category.agda :)).

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

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

Хотя вообще выглядит правильно — берём наименьшую возможную теорию (не обязательно от PA) и доказываем в её рамках эквивалентность, потом показываем, что N с Unsigned являются моделями этой теории. Но это же нужно ещё сделать («проговорить»).

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

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

Ну это уже «снаружи», а во внутренней теории кольца у нас нету никакой структуры - да и самого кольца нет :)

Верно, только мы ведь ещё не доказали исходное утверждение строго в рамках PA

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

Если второе определение можно переписать как определение в PA, то первое - нет, ведь у нас в PA нету циклов. Нам придется заменить этот цикл рекурсией, а после такого преобразования эквивалентность станет достаточно очевидной.

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

такое впечатление, что у quasimoto раздвоение личности... )))

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

Нам придется заменить этот цикл рекурсией, а после такого преобразования эквивалентность станет достаточно очевидной.

Я так и сделал тут. Очевидно, только это не PA, а конкретная модель натуральных чисел, так что док-во сильно опирается на её свойства.

очевидной

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

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