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

Толк в том, что можно проверять программы на эквивалентность.

вернись к первому посту, и продемонстрируй.

Если входные данные - целые числа, то можно по индукции.

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

Работает-ли она на бесконечности — неизвестно.

Датычо? Вот же точная цитата твоих слов:

ВНЕЗАПНО: множество вещественных(натуральных, целых, рациональных, и т.п.) чисел кольцом НЕ является.

Ты, видимо, не читал предыдущие посты? Предполагается, что проблема останова решаема.

Представь себе, есть трансфинитная индукция.

Но в данном случае она не нужна - ведь нам и не нужно доказывать что-либо для бесконечностей. Только для конечных (хотя и любых) чисел. Ведь бесконечностей у нас в МТ не бывает, по определению МТ.

Вот же точная цитата твоих слов:

ВНЕЗАПНО: множество вещественных(натуральных, целых, рациональных, и т.п.) чисел включающее в себя бесконечность, кольцом НЕ является.

//fixed

Ты, видимо, не читал предыдущие посты? Предполагается, что проблема останова решаема.

кем предполагается?

Представь себе, есть трансфинитная индукция.

где она «есть»?

Но в данном случае она не нужна - ведь нам и не нужно доказывать что-либо для бесконечностей. Только для конечных (хотя и любых) чисел. Ведь бесконечностей у нас в МТ не бывает, по определению МТ.

тогда и проблемы останова нет и проблемы эквивалентности тоже нет.

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

где она «есть»?

Что значит «где»?

тогда и проблемы останова нет и проблемы эквивалентности тоже нет.

Алан Тьюринг доказал, что есть.

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

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

Ну и все равно является, я об этом уже упоминал. Множество гиперрациональных - вполне себе поле.

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

PS: перед тем, как ссылаться на себя — зарегся. Анонимус тут уже целый вагон чуши написал. Я не говорю, что ты дебил, но под этим ником кроме тебя полно дебилов.

тогда и проблемы останова нет и проблемы эквивалентности тоже нет.

Алан Тьюринг доказал, что есть.

ну да. Используя МТ с бесконечной лентой.

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

Я не понял, ты сейчас пытаешься нас всех убедить, что ты не писал этих слов:

ВНЕЗАПНО: множество вещественных(натуральных, целых, рациональных, и т.п.) чисел кольцом НЕ является.

?

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

Возьми любой учебник по нестандартному анализу - и найдешь пруфы. Робинсона советовать не буду, конечно, можешь почитать «прикладной нестандартный анализ» Девиса.

ну да. Используя МТ с бесконечной лентой.

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

Поскольку ты сам погуглить неспособен, я сделаю это за тебя: http://neerc.ifmo.ru/wiki/index.php?title=Машина_Тьюринга

Обрати внимание, там даже для особо одаренных:

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

«чтобы строки имели конечную длину» - обрати внимание.

вернись к первому посту, и продемонстрируй

Определения:

open import Data.Nat

fib₁-rec : ℕ → ℕ → ℕ → ℕ
fib₁-rec a b zero = a
fib₁-rec a b (suc n) = fib₁-rec b (a + b) n

fib₁ : ℕ → ℕ
fib₁ = fib₁-rec 0 1

fib₂ : ℕ → ℕ
fib₂ (suc (suc n)) = fib₂ n + fib₂ (suc n)
fib₂ n = n

доказательство эквивалентности:

open import Data.Nat.Properties -- un'private'ized
open import Relation.Binary.PropositionalEquality

fib₁≡fib₂ : ∀ n → fib₁ n ≡ fib₂ n
fib₁≡fib₂ = go 0 where
  go : ∀ m n → fib₁-rec (fib₂ m) (fib₂ (suc m)) n ≡ fib₂ (m + n)
  go m zero = cong fib₂ (sym (n+0≡n m))
  go m (suc n) = trans (go (suc m) n) (cong fib₂ (sym (m+1+n≡1+m+n m n)))

Две строчки, фактически.

Откуда следует, что ∀ n → fib₁ n ≡ fib₂ n и его отрицание не являются независимыми, то есть если начать перечислять все доказательства и опровержения, то за конечное время найдётся доказательство эквивалентности — для не независимых утверждений такая проблема разрешима (вообще — http://en.wikipedia.org/wiki/Entscheidungsproblem с исключениями вроде http://en.wikipedia.org/wiki/Presburger_arithmetic или http://en.wikipedia.org/wiki/Tarski's_axioms — consistent + complete + decidable).

На практике «за конечное время» может быть «за нереально долгое время», так что проще найти доказательство в ручном или полуручном режиме. Agda или Coq это пруф ассистенты (http://en.wikipedia.org/wiki/Proof_assistant), так что они предполагают ручные и полуручные доказательства, но есть и автоматические пруверы (http://en.wikipedia.org/wiki/Automated_theorem_proving), которые вполне способны доказывать такого рода вещи полностью автоматически (решая полуразрешимую проблему, то есть с зависаниями — нужно ставить таймауты).

вы все неправы

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

с педерастами не разговариваю.

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

Всё равно что говорить «давай-ка переложим шаблоны 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 — мы вводим имена на которые могут быть зависимости в типах слева на право, так что в сигнатурах можно обойтись вообще без свободных имён).

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

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

У тбу есть GMP

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

Ты у нас гомофоб, по-этому и приписываешь Тьюрингу

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

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

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

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

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

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

Взбугагнул.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ну я могу и супернатуральные придумать. С делителями нуля. И что?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

А это не так.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

float/double

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

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

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

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

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

Аааа :)

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

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

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

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

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

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

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

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

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

Аааа

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Как это?

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

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

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

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

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

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

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

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

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

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

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

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