Comments | thesz: Парадоксы.

thesz

Парадоксы.

Oct 02, 2011 04:50

Что меня ещё интересует ( Read more... )

парадоксы, системы типов, формальные методы

Comments 19

perepertoz October 2 2011, 02:33:05 UTC

ИМХО проверка простая : как только у вас достаточно сложная теория - всё, ловите парадоксы ...
http : //www.scorcher.ru/subject_index/subject_show.php?id=4249

nivanych October 2 2011, 07:25:22 UTC

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

thesz October 2 2011, 10:13:53 UTC

Какая фигня.

Последняя версия теории типов Мартина-Лёфа непротиворечива, а вот её реализация в Агде2 оказалась содержащей возможность противоречия.

Причём, как я понял, по чисто техническим причинам.

pinkbagheera October 2 2011, 04:31:00 UTC

Формализация: "Все, что создано с помощью человеческого интеллекта, заключает в себе парадоксы" :)))

thesz October 2 2011, 10:14:53 UTC

Это неправильно. Ведь кое-что же всё-таки в принципе не содержит парадоксов.

pinkbagheera October 2 2011, 12:35:41 UTC

Например?

thesz October 2 2011, 13:35:38 UTC

Теория множеств Цермело-Френкеля без аксиомы выбора, например. ;)

Thread 8

nivanych October 2 2011, 07:28:26 UTC

Противоречие в агде только там, где пользуются кодом, не прошедшим termination check.
Можно сказать, что возможность противоречия в агде2 возникает оттуда же, что и возможность общей рекурсии в ML (let rec).

thesz October 2 2011, 10:28:53 UTC

Ловили и с termination check.

Отыскать, правда, не могу.

cp_poster October 2 2011, 10:15:42 UTC

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

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

Простите за глупые вопросы и мысли в текст...

Есть ли общий алгоритм, позволяющий определить противоречива ли аксиоматика? Мне кажется это дуально Halting problem.

thesz October 2 2011, 10:36:43 UTC

Да и ладно, с неполнотой-то.

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

Вот наличие противоречий пережить нельзя.

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

Агда построена на теории типов Мартина-Лёфа (Per Martin-Löf). Её расширили парочкой технических возможностей (сравнение с образцом). И где-то в ней получилась возможность внесения противоречий. Её исправили, но осадочек остался.

Что меня и беспокоит. ;)

graninas October 3 2011, 02:04:57 UTC

Ну, вы, конечно, знаете о теореме Геделя о неполноте? Она утверждает, что в любой непротиворечивой системе найдется такое утверждение, которое нельзя ни доказать, ни опровергнуть средствами этой системы. Отсюда следует, что любая, даже самая непротиворечивая система имеет по крайней мере один парадокс - для некоторого выражения А в этой системе невозможно вывести это выражение. К сожалению, нельзя построить систему без этого противоречия.

thesz October 3 2011, 07:37:01 UTC

Это не парадокс.

http://ru.wikipedia.org/wiki/%D0%9F%D0%B0%D1%80%D0%B0%D0%B4%D0%BE%D0%BA%D1%81_%D0%A0%D0%B0%D1%81%D1%81%D0%B5%D0%BB%D0%B0

С наличием истинных утверждений, которые невозможно доказать в какой-то системе все готовы смириться, и я в том числе. А вот наличие неконструктивных путей построения доказательства - это плохо.

Thread 7