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)

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

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


Ответ на: комментарий от 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 ★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.