И ещё о доказательности.
Jul. 20th, 2011 10:17 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
fat_yankeyНезадолго до 1977 года две независимые команды топологов (американская и японская) аннонсировали результаты касающиеся одной и той же гомотопической группы. Результаты противоречили друг другу, а так как оба доказательства оказались весьма сложными, то было совершенно неочевидно кто же из двоих прокололся. Ставки, однако, были достаточно высоки, чтобы не спускать дело на тормозах, и обе команды обменялись результатами для взаимной проверки. Очевидно, что и у тех и у других имелась достаточно сильная мотивация чтобы найти ошибку в доказательстве "соперников", однако же из этого ничего не вышло. Ни американское ни японское доказательство так и не удалось опровергнуть; при том, что одно из них непременно должно было быть неверно.
Как бы в насмешку, вскоре появилось третье, независимое, доказательство, подтверждающее результаты американской команды. Оказавшись в меньшинстве японцы отозвали свои результаты. Рассказывают, что один из американцев после этой истории оставил занятия математикой, видимо в поисках работы, где бы результаты его труда оценивались более объективно.
Эта история была рассказана в статье Social processes and proofs of theorems and programs, by Richard A. DeMillo, Richard J. Lipton, Alan J. Perlis; Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1977. Статья (не история) наделала много шума и дала начало т.н. Proof of Correctness Wars. К сожалению, авторы из этических соображений не называют никаких имён и фактов, поэтому независимо проверить эту историю у меня не вышло.
На момент выхода этой статьи в математических журналах мира публиковались доказательства примерно 200,000 теорем в год.
Чтение по теме:http://elementy.ru/lib/431269?context=5085665
Как бы в насмешку, вскоре появилось третье, независимое, доказательство, подтверждающее результаты американской команды. Оказавшись в меньшинстве японцы отозвали свои результаты. Рассказывают, что один из американцев после этой истории оставил занятия математикой, видимо в поисках работы, где бы результаты его труда оценивались более объективно.
Эта история была рассказана в статье Social processes and proofs of theorems and programs, by Richard A. DeMillo, Richard J. Lipton, Alan J. Perlis; Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1977. Статья (не история) наделала много шума и дала начало т.н. Proof of Correctness Wars. К сожалению, авторы из этических соображений не называют никаких имён и фактов, поэтому независимо проверить эту историю у меня не вышло.
На момент выхода этой статьи в математических журналах мира публиковались доказательства примерно 200,000 теорем в год.
Чтение по теме:http://elementy.ru/lib/431269?context=5085665
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2011-07-21 02:56 am (UTC)no subject
Date: 2011-07-21 03:16 am (UTC)no subject
Date: 2011-07-21 03:47 am (UTC)no subject
Date: 2011-07-21 03:56 am (UTC)Урежьте осетра хотя бы на три нулика
no subject
Date: 2011-07-21 07:42 am (UTC)no subject
Date: 2011-07-21 07:46 am (UTC)> независимое, доказательство, подтверждающее результаты
> американской команды
Почему "как бы в насмешку"? Просто исследования продолжались.
> Рассказывают, что один из американцев после этой истории
> оставил занятия математикой
Кто рассказывает? В статье ДеМилло и др. этого рассказа нет.
Статья, кстати, очень хороша. Один из её авторов, R.J.Lipton, сейчас входит в число наиболее авторитетных исследователей сложности вычислений и алгоритмов (фундаментальная проблема "P=NP" и всё вокруг неё). Он ведет отличнейший блог Gödel's Lost Letter and P=NP (highly recommended).
no subject
Date: 2011-07-21 10:31 am (UTC)no subject
Date: 2011-07-21 10:33 am (UTC)no subject
Date: 2011-07-21 10:38 am (UTC)Это скрытая цитата. Но вот курьез: он начисто разрушил все пять доказательств, а затем, как бы в насмешку над самим собою, соорудил собственное шестое доказательство!
> Кто рассказывает? В статье ДеМилло и др. этого рассказа нет. Статья, кстати, очень хороша.
Действительно хороша. Поэтому посоветую - перечитайте. Найдёте искомый рассказ.
no subject
Date: 2011-07-21 10:48 am (UTC)Совершенно необязательно. Возможно, что в основе топологии лежит противоречивая система аксиом.
Так что может оказаться, что требования "запретить нахуй блядскую топологию" могут воплотиться в жизнь.
no subject
Date: 2011-07-21 10:49 am (UTC)Да, неплоха. Для чайников.
Упрощённый пересказ теоремы Геделя о неполноте.
no subject
Date: 2011-07-21 10:51 am (UTC)Я не шучу.
no subject
Date: 2011-07-21 10:53 am (UTC)no subject
Date: 2011-07-21 10:58 am (UTC)no subject
Date: 2011-07-21 11:00 am (UTC)no subject
Date: 2011-07-21 11:06 am (UTC)no subject
Date: 2011-07-21 11:12 am (UTC)no subject
Date: 2011-07-21 11:17 am (UTC)Что до Гёделя - вывод сделал, послушав http://rutube.ru/tracks/1543805.html
no subject
Date: 2011-07-21 11:21 am (UTC)Возможно, конечно. Вон коллега
ДеМилло сотоварищи представляли статью в кругу коллег по цеху, поэтому и никаких имён - все и так знали о какой истории речь. И видимо всем было достаточно очевидно, что дело тут не в возможной противоречивости системы аксиом.
no subject
Date: 2011-07-21 11:21 am (UTC)Вы, видимо, пересказ в исполнении Рабиновича читали.
no subject
Date: 2011-07-21 11:26 am (UTC)В исторических чтениях вы любите обращать внимание на разночтения между изданиями. Попробуйте применить это своё умение и здесь.
no subject
Date: 2011-07-21 11:33 am (UTC)no subject
Date: 2011-07-21 11:33 am (UTC)Вот та версия, из которой Вы цитируете:
href="http://www.cs.yale.edu/publications/techreports/tr82.pdf
А вот та, что читал я (судя по номеру, более поздняя, но я не уверен):
http://www.cs.yale.edu/publications/techreports/tr136.pdf
В первой нужная цитата есть, во второй -- нет.
no subject
Date: 2011-07-21 11:35 am (UTC)no subject
Date: 2011-07-21 07:06 pm (UTC)За последние годы выявилось много случаев, где решения ряда знаменитых математических проблем топологии, динамических систем, различных ветвей алгебры и анализа, как выяснилось, не проверялись никем очень много лет. Потом оказалось, что доказательство неполно (см. мою статью в томе журнала GAFA 2000, посвященного конференции «Vision in Mathematics - 2000», Tel Aviv, August 1999). При этом отнюдь не во всех случаях пробелы могут сейчас быть устранены. Если никто не читает «знаменитых» работ, то как же обстоит дело со сложными доказательствами в более заурядных работах? Ясно, что их в большинстве просто никто не читает. Я могу понять, что решенные в тот же период проблемы Ферма и четырех красок стоят и длинного доказательства, и их проверят. Но постоянно жить в мире сверхдлинных доказательств, никем не читаемых, просто нелепо. Это - дорога в никуда, нелепый конец программы Гильберта.
no subject
Date: 2011-07-21 09:04 pm (UTC)СПЕЦИФИКА...
Пруфы будут?
no subject
Date: 2011-07-22 04:10 am (UTC)no subject
Date: 2011-07-22 12:07 pm (UTC)Дяденька Понтрягин нарисовал левую лемму, которую сам кстати и исправил позже на пару с Вайтхедом. Первый вариант леммы с еще левым результатом японцы впаяли в свой инструментарий (Тода и К.) и настрогали левых результатов. Которые не понравились американским монстрам Борелу (хорощее имя) и Хирзербруху. Благодаря некому конфликту (почему разные результаты?) в дело включился другой монстр с не менее замечательной фамилией Бот и используя оригинальный путь сгенерировал замечательную обобщающую теорему периодичности "размера" хомотоптных груп.
сама статья на которую ссылается автор блога "политическая" и служит как "аргументация" против строгой формализации программирования.
Аргументация левая: благодаря строгой формализации и многочисленным WTF возникающих в математике математика выросла вглубь и вширь. WTF в немалой степени были отличным стимулом для активации новых людей и расширения решений до обеспечения их непротиворечивости. Сопутствующая проблема формализации (нечитаемость и сложность прослеживания всех углов) неизбежный спутник любой непрерывно развивающейся системы и в неформализованных системах проявляется еще хуже. Горизонт растет и ничего с этим не сделаешь.
При всей "неформальности" программирования, программирование уже давным давно "не читаемо" и намного менее "социально" чем формальная теорматематика.
Ба
no subject
Date: 2011-07-23 01:36 am (UTC)Вам осталось только добавить "средневековая" и можно уверенно деанономизировать - вы дух покойного Эдсгера Дейкстры.
На самом деле статья не политическая, а философская. И не "против" proof of correctness, а за осмысление. Осмысление того, почему практика доказательства корректности программ не нашла поддержки в программистком сообществе.
> Аргументация левая
Та, что вы проводите - несомненно. Но в статье линия аргументации другая.
no subject
Date: 2011-07-23 09:48 am (UTC)Авторы статьи явно не ставили перед собой такой задачи - упрощенно рассказать о Теореме Геделя, наверное Петр имел ввиду, что говорят они примерно о том же, что и Гедель, но проще. Но и это не так. Они как раз говорят об обратном.
Гедель (утрированно, без использования выражений типа "рекурсивной непротиворечивости") говорит, что в рамках непротиворечивой теории всегда можно придумать теорему, которую нельзя вывести из набора аксиом данной теории, но которая будет верна. В статье же говорится о случае, когда в рамках теории (конкретно, топологии) при помощи стандартной логики из одного набора аксиом получаются противоречивые результаты. Т.е. что топология не подпадает под теорему Геделя, т.к. данная теория является противоречивой.
Аскер
no subject
Date: 2011-07-23 05:00 pm (UTC)че серьезно не нашла? и Algorithm correctness и functional correctness изчезли из куррикулума CS? позвольте не поверить.
Дяденьки мешают в одну кучу инструментарий (алгоритмы) который вполне развивается как часть "математики" и следует тем же принципам (формальное символьное описание и пр.) и их применение (программы на к.языках) которое вполне себе подчининяется инженерным принципам и является развитой достаточно стандартизированной инженерной дисциплиной (с возникновением всяких Agile подходов, библиотек алгоритмов и пр. вкусностей которых так хотели эти "философы").
Аргументация левая потому что дяденьки пищут о каких-то "социальных механизмах" в математике. Какие нафиг социальные?
В приведенном примере, примере обычной в современной математике "опубликованной ошибки" Бот прийдя из другой области, прочитал проблему к его счастью написанную на математическом языке, подумал, обсудил и сгенерировал свой подход. Решил проблему. Обобщил. На каждом шагу любой новый Бот может ссесть, закупиться горой колы и пиц, прочитать писанину Бота и сгенерировать следующий шаг. Есть движение потому что язык один, формализованный. Сииимвольныый.
Вообще "Социальность" и математика оксимороны. Дяденьки которые используют два слова вместе не могут быть здоровы.
Да читать современную математическую мешанину тяжело, продираться через лесенки лем тяжко. Теоремы с доказательством на паре сотней страниц норма. Но движение есть. Потому что "верить" не надо, можно просто читать и проверять, результаты улучшать. Расти так сказать над собой.
no subject
Date: 2011-07-24 01:17 pm (UTC)Не исчезли, конечно. Но вы не путайте алгоритмы и программы. Полезность доказательства корректности алгоритмов никем не оспаривалась, в т.ч. и авторами обсуждаемой статьи. Спор шёл только вокруг полезности доказательства корректности программ.
>Дяденьки мешают в одну кучу инструментарий (алгоритмы) который вполне развивается как часть "математики" и следует тем же принципам (формальное символьное описание и пр.) и их применение (программы на к.языках)
Да не дяденьки, а вы в своём восприятии дяденек. Дяденьки-то как раз в курсе.
> Аргументация левая потому что дяденьки пищут о каких-то "социальных механизмах" в математике. Какие нафиг социальные?
Неправы они тут только в том, что сужают область определения до математики. Тогда как те же социальные механизмы действуют во всей науке.
>Вообще "Социальность" и математика оксимороны. Дяденьки которые используют два слова вместе не могут быть здоровы.
Тут вы неправы. Математика по определению социальна. Как и любая другая человеческая деятельность. Доказательная сила теорем к социальности, конечно, отношения не имеет. Но дяденьки рассматривают дело под углом убедительности, а не доказательности.
Конечно нет.
Date: 2011-07-26 11:50 am (UTC)=================
КАК БЫ получаются.
Просто доказательства настолько сложны, что проверить их полностью очень сложно. Т.е. НА САМОМ ДЕЛЕ (тм) в одном из доказательств есть ошибка, но в каком именно - установить на сегодняшний день не получилось.
Недаром доказательства теоремы Ферма и гипотезы Пуанкаре проверяли по нескольку лет (или месяцев, по крайней мере).
Re: Конечно нет.
Date: 2011-07-28 08:35 am (UTC)>>Т.е. НА САМОМ ДЕЛЕ (тм) в одном из доказательств есть ошибка, но в каком именно - установить на сегодняшний день не получилось.
Это уже вопрос веры. Если вы ВЕРИТЕ, что топология является непротиворечивой теорией, т.е. данное утверждение мы считаем истинным - тогда абсолютно логично, что в одном из решений есть ошибка.
А вот если мы верим, что ошибки там нет, поскольку искали ошибку не просто лучшие в этой области, а конкурирующие организации - то та же логика подсказывает другой вывод.
Re: Конечно нет.
Date: 2011-08-01 02:08 pm (UTC)А вот верить, что ошибки нет, не стоит.
Ибо команды математиков, получившие противоположные результаты, - не "конкурирующие фирмы", и как правило никакой выгоды от разоблачения друг друга не получают.
Чем искать ошибки в доказательствах "конкурентов", проще ещё одно своё придумать. Более того, сейчас в научном мире есть проблема - люди не хотят критиковать, потому что критика повышает уровень цитируемости оппонента.
А Вы говорите - "конкурирующие фирмы".