Oleksandr Gavenko -> [email protected] @ Wed, 28 Apr 2010 14:58:19 +0300:
>> OG> Я верю что спустя некоторое время общественность примет машинные >> OG> доказательства как равносильные бумажным. >> >> Я могу поверить, что компьютерное доказательство современной теоремы >> более надежно, чем человеческое. Но вероятность того, что оно верно, >> все равно отлична от 1. А вероятность того, что правильная программа в >> реальной жизни однажды не сработает, даже вполне заметно отлична от 1 - >> практика показывает, что даже для не шибко распространенного софта раз >> лет в 10 такое всплывает. >> OG> Дома стоят, самолеты летают. Хороший пример. И дома, и особенно самолеты падают, прямо скажем, нередко. OG> В софте есть проблемы - пишут его на коленках OG> с использованием опасных языков програмирования OG> для небезопасных платформ. В том случае, который был у нашей конторы, ничем кроме взглюка железа, объяснить проблему не удалось. С перепроверками этого места и попытками воспроизвести проблему возились около года. Кстати, известный факт - да, вероятность детерминированного выполнения детерминированного алгоритма на существующем железе меньше 1. В достаточной степени меньше, чтобы это вызывало вполне реальные проблемы. И чтобы десяток прогонов вероятностного теста на простоту давал лучшую вероятность того, что число простое, чем вероятность, что все арифметические действия в процессе выполнились правильно... >> Не говоря уже о том, что событие с вероятностью 1, как нас учит теория >> вероятностей, тоже может не произойти как нефиг делать. (Мой любимый >> пример на эту тему - выбор точки на отрезке [0;1]. Какая-то точка >> обязательно будет выбрана - но вероятность ее выбора в точности равна >> 0.) >> OG> Ага, мера Лебега одноэлементного множества OG> на действительной прямой равна 0. OG> В формальной логике нет понятия вероятности, OG> либо имеется доказательство теоремы из соответствующих аксиом OG> и правил вывода либо нет. OG> Имеется эффективная процедура для установления того факта OG> является ли последовательность утверждений выводом в логическом OG> исчислении. А иначе как? OG> Человеческий фактор есть проблема. Причем в данном случае принципиально неустранимая. Можно только уменьшить его влияние. -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]
