On 2010.04.28 13:26, Artem Chuprina wrote:
Oleksandr Gavenko -> debian-russian@lists.debian.org @ Wed, 28 Apr 2010
10:55:18 +0300:
>> Реализацию лиспа, на которой оно выполняется, кто доказывать будет?
>> -Пушкин- МакКарти?
OG> Было бы время и возможности.
Пара лишних возрастов Вселенной?
Действительно тут нужно конструктивное доказательство - привести пример.
Не доказано, но и не опровергнуто.
>> И в общем, да, ты тот лисп вообще видел? Программы на нем писал?
OG> не CL но elisp достаточно, но это не важно
>> Отлаживал? А реальные программы, не учебные задачи? Я б тебя еще
>> понял, если б ты Хаскель назвал - тот чисто функциональный, там
>> действительно существенно легче верифицировать. А как только у тебя
>> в языке есть присваивание - все, туши свет...
>>
OG> в этой области профан
Ну, стало быть, и в доказательстве программ тоже профан.
Согласен. Баловался основаниями математики и
использованием цифрового друга для
полуавтоматического доказательства теорем.
Но освоить lambda calculus и Martin-Löf type theory
выпускникам мех-мата не проблема ))
OG> Но сложности все таки есть. Например
OG> http://en.wikipedia.org/wiki/Kepler_conjecture
OG> из осторожности не признают доказанной. Хотя машинное доказательство
OG> http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer
OG> было принято общественностью.
... т.е. общественность после продолжительных дебатов решила "черт с
вами, поверим".
Нет - просто бородатые профессора еще боятся компьютеров.
OG> Я верю что спустя некоторое время общественность примет машинные
OG> доказательства как равносильные бумажным.
Я могу поверить, что компьютерное доказательство современной теоремы
более надежно, чем человеческое. Но вероятность того, что оно верно,
все равно отлична от 1. А вероятность того, что правильная программа в
реальной жизни однажды не сработает, даже вполне заметно отлична от 1 -
практика показывает, что даже для не шибко распространенного софта раз
лет в 10 такое всплывает.
Дома стоят, самолеты летают.
В софте есть проблемы - пишут его на коленках
с использованием опасных языков програмирования
для небезопасных платформ.
Не говоря уже о том, что событие с вероятностью 1, как нас учит теория
вероятностей, тоже может не произойти как нефиг делать. (Мой любимый
пример на эту тему - выбор точки на отрезке [0;1]. Какая-то точка
обязательно будет выбрана - но вероятность ее выбора в точности равна
0.)
Ага, мера Лебега одноэлементного множества
на действительной прямой равна 0.
В формальной логике нет понятия вероятности,
либо имеется доказательство теоремы из соответствующих аксиом
и правил вывода либо нет.
Имеется эффективная процедура для установления того факта
является ли последовательность утверждений выводом в логическом
исчислении. А иначе как?
Человеческий фактор есть проблема.
--
С уважением, Александр Гавенко.
--
To UNSUBSCRIBE, email to debian-russian-requ...@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
Archive: http://lists.debian.org/4bd822db.8010...@bifit.com.ua
