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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

вот именно

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Кстати

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

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

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

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

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

Натуральных чисел не существует?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Почему мимо:

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

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

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

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

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

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

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

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

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

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

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

fib1(-2)

с какого перепуга ты считаешь fib(-2)?, что это вообще за HEX?

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

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

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

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

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

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

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

Это, очевидно, результаты работы рекурсивных функций из топика (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.

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

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

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

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

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

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

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

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

Да, я имел в виду, что signed и unsigned это конечные кольца, а точнее...

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

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

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

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

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

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

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

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

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

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

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

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

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

signed не кольцо, т.к. стандартом не определено поведение в случае переполнения

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

signed не кольцо

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

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

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

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

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

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

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

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

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

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

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

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

кольца

поля

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

fib(100) > 2 ^ 64.

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

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

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

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

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

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

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

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

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

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

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

А у меня есть.

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

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

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

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

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

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

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

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

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

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

fib(100) > 2 ^ 64.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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