avva | компьютеры и математика: часть вторая

Продолжение вот этой записи.

Перед тем, как перейти к алгоритмической стороне дела - ещё немного о различии двух типов доверия. Этот пример прямо-таки взят из жизни. Несколько лет назад в процессоре Пентиум был обнаружен баг - в некоторых редких ситуациях он неправильно делил действительные числа. Интель, естественно, исправила баг в следующих версиях и бесплатно заменила процессоры всем желающим.

Представим себе математика М, который не знает об этом баге, и который решил проверить, не забыл ли он ещё, как делят в столбик числа без компьютера. Поделив два довольно больших действительных числа, он запускает программу calc на своих Виндоуз и видит, что она выдаёт ему совсем другой результат. Вот примерный сценарий его мыслей и действий.

Первый импульс: ошибся при счёте. Пересчитал заново и получил такой же результат.
Вторая возможность: дурацкий баг в программе. Запустил другую программу-калькулятор - не помогло.
Теперь М практически убеждён, что всё-таки что-то не так сделал при делении в столбик. Он повторяет всю процедуру ещё раз и очень внимательно. Не помогает. Он звонит коллеге и просит того поделить в столбик два числа вручную, не объясняя зачем. Не помогает.
Может, что-то не так с моим компьютером? Просит коллегу (у того тоже Пентиум) посчитать на компьютере - не помогает.
Тут, наконец, М начинает подозревать модель процессора (или модель компьютера "вообще", если он в этом не разбирается и не знает, что такое процессор). Он достаёт свой старенький электронный калькулятор (или делит оба числа на своём юниксовском счету на факультетском сервере) - ура! Сходится с его ручными подсчётами. Ошибка обнаружена, можно писать письмо в Интель. Между прочим, примерно так и был обнаружен этот баг - стараниями математика, не понимавшего, почему его программа выдавала абсурдные результаты.

Но вот что важно: ни разу во время поисков источника проблемы М не задумался о правильности алгоритма деления в столбик. Он подвергал сомнению свою способность безукоризненно выполнить этот алгоритм - "физический" вид доверия. Но после нескольких независимых проверок (собственных и коллег) это сомнение по сути дела исчезло. Он подвергал сомнению способность компьютера правильно выполнить свой алгоритм (и потому выполнял деление несколько раз - мало ли что там могло закоротить) - тоже "физическое" доверие. Наконец, он подверг сомнению правильность компьютерного алгоритма (о котором он ничего не знал) - "математический" вид доверия - и это оказалось верным шагом. Но в алгоритме деления в столбик он не сомневался. Почему?

Потому что он знал, что может строго доказать его правильность (она же soundness, если использовать жаргон логиков). Даже проще: это доказательство являлось для него очевидным свойством алгоритма. Он мог бы выписать долгое подробное формальное доказательство, но это всего лишь подтвердило бы очевидное.

Продолжение следует.