компьютеры и математика: часть третья.
Sep. 10th, 2001 07:34 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avvaСледует за частями первой и второй.
Постараюсь, наконец, увязать всё это вместе. Для этого мне нужно посмотреть внимательнее на то, что математики считают доказательством, а что не считают (не учитывая сейчас эти проблемы с компьютерами и программами). Чтобы немного сэкономить время и место, я не буду подробно проводить разбор и обосновывать его, а вместо этого приведу собственно краткое описание своей точки зрения; если кто-то с ней не согласен, пожалуйста оспорьте:
Математическое доказательство на практике никогда не формально (не является формальным доказательством с точки зрения мат. логики), но всегда сохраняется принципиальная возможность относительно легко добиться абсолютной строгости. Что это значит? Доказательство написано не на формальном языке, а на некоем многоуровневом мета-языке, причём уровни косвенности легко могут множится и пересекаться. Например, заявление вроде "итак, существует как минимум одно решение уравнения (1); пусть a - одно такое решение" очень легко поддаётся формализации. Кусок текста "... но этот случай легко вытекает из леммы 3.41" формализовать сложнее: что значит "легко"? Но математик, владеющий контекстом, с лёгкостью подставит вместо "легко" нужные элементарные шаги, после чего весь процесс можно будет формализовать и превратить в формальное доказательство. Практически каждый шаг в математическом док-ве требует владения конктекстом на самых разных уровнях, начиная с аксиом данной структуры и их элементарных следствий, и кончая сложными результатами, на которые стоят библиографические ссылки. Но все эти детали во время чтения и понимания доказательства математик может подставить, неизвестные ему результаты, на которые ссылаются, принять в качестве допущений, и т.д.
Важно понять, что, с одной стороны, я говорю о принципиальной возможности - никто на самом деле не занимается подобным переводом в формальную цепочку утверждений - но с другой стороны, настаиваю на абсолютной незаменимости этого требования, без которого доказательство не может больше считаться законным и верным.
Если отвлечься на секунду в историю математики, то я утверждаю, что войны конца 19-го и начала 20-го веков между знаменитыми математиками и целыми школами касательно допустимых и недопустимых методов доказательств настолько потрясли математическое сообщество, что де-факто был принят этот, описываемый мной, неформальный и интуитивный метод определения того, что есть математическое доказательство, который опирается на достигнутое к тому времени понимание формального док-ва как строгого математического объекта. Этот метод показал себя с лучшей стороны: интуиционизм уже давно не беспокоит практически никого из практикующих математиков, а споры вокруг той же аксиомы выбора не приводят к расколам и отказу от достигнутых результатов.
Очень вкратце попробую обосновать своё требование принципиальной формализабильности как главного критерия на то, чтобы считаться доказательством. Возьмём пример, который как раз могут привести мне в качестве контраргумента. Пусть есть некая очень сложная статья, написанная математиком В, и математик Д её читает. В какой-то момент В пишет: "а этот случай доказывается аналогично (б), с соответствующими измененями". Д, предположим, принимает во время чтения это на веру; но если мы попросим его формализовать всё доказательство, он вернётся к этому месту и споткнётся: не получается у него ничего аналогично (б). Может, он слишком глупый, или не хватает чего-нибудь из контекста, или ещё чего. Но доказательство всё же верно (предположим мы), просто у Д не получается его формализовать - что же теперь, это не доказательство? Если бы В стоял рядом, он бы в один момент всё Д объяснил.
Да, это верное доказательство. Но, я думаю, мы можем сойтись на том, что оно не было полностью передано Д. Есть некое верное доказательство в голове у В, есть некая его репрезентация в журнальной статье, но у Д не получается из этой репрезентации обратно построить доказательство, т.к. в репрезентации (или в голове Д) чего-то существенного не хватает. Не хватает, по сути дела, какого-то контекста. Даже если там есть просто трудный переход от одного утверждения к другому, и Д недостаточно натренирован в данной области, чтобы этот переход совершить, всё равно же понятно, что в принципе можно было бы это медленно разжевать по кусочкам, чтобы Д мог за этим проследовать - просто В на такие мелочи не разбрасывается. То есть, так или иначе, доказательство (как некий объект) не было успешно передано от В к Д. Поэтому оно и не проходит тест на интуитивную формализабильность. Именно потому, что не проходит, мы и делаем вывод, что у Д нет доказательства (хоть у В и есть). Это и демонстрирует истинность этого критерия.
Для чего нужна вся эта бодяга? Для того, конечно, чтобы математики могли быть уверены в том, что они могут проверить работы друг друга (и понять, заодно; невозможно понять, если не получается убедиться в истинности). Здесь я опять же говорю о принципиальной возможности; естественно, есть куча статей, непонятных никому, кроме их авторов; есть куча статей с ошибками, иногда грубыми, которые никто не заметил, и т.д. и т.п. Но в принципе у математика Д должна быть возможность проверить утверждения математика В. Но что значит "проверить"? Математик В может "мамой поклясться" Д, что у него всё правильно, и тот может поверить, но проверкой это, очевидно, не будет. Проверка как раз и возможна только потому, что есть принципиальная возможность редукции к абсолютно строгой, формальной, форме; как эта редукция выполняется - зависит от принятой нотации, степенью владения контекстом, стандартными сокращениями и т.д. и т.п.; но в любом случае эта редукция возможна и обязательно является чем-то принципиально возможным и осуществимым (feasible); просто никто этого не делает ввиду утомительности и ненужности.
Ох, расписался. Ну да ладно. Итак, весь этот кусок между двумя линиями был посвящен природе математического доказательства.
Вернёмся, наконец, к теореме о четырёх цветах. У неё есть некое нетривиальное доказательство, с теоретической и компьютерной частями, как я описал в своей первой записи. Применим к нему наш критерий. Можем ли мы его формализовать?
Теоретическая часть легко поддаётся формализации, а вот с практической несколько сложнее. В ней мы имеем дело с формальным описанием некоторого алгоритма (алгоритма, не компьютера! для этого важного различия мне нужна была вся дискуссия о двух типах доверия). Этот алгоритм проверяет, например, что все 600+ конфигураций из некоего конечного набора не могут принадлежать контрпримеру к теореме. Делает он это путём сложного интенсивного перебора возможностей редуцировать эти конфигурации при помощи некоего конечного набора правил редукции (применимость и достаточность которого мы тоже доказали в теоретической части).
Как вы сказали, что делает этот алгоритм? Он проверяет... Стоп. Откуда мы это знаем?
И тут мы подходим к проблеме доверия алгоритму. Алгоритму деления в столбик мы доверяем потому, что можем легко доказать его правильность. А правильность нашего алгоритма в док-ве теоремы о цветах мы можем доказать?
Может быть, да, может быть, нет. Вообще говоря общая проблема доказательства того, что данный алгоритм выполняет то, что от него хотят, неразрешима в принципе. Конечно, обычно мы имеем дело с не такими уж сложными алгоритмами, но, с другой стороны, вся область формальной верификации не так уж многого добилась за те десятки лет, что она существует. Доказывать правильность очень простых численных алгоритмов мы умеем; чего-то посложнее, с большим пространством перебора и нетривиальной логикой - вовсе необязательно.
Но так или иначе, можем мы доказать правильность алгоритма или нет, такое доказательство вместе с самим алгоритмом и всем остальным нам не предоставляется. У нас его нет. О верности алгоритма мы вынуждены судить "на глазок", пользуясь интуицией программиста. Но суть нашего критерия того, чтобы считаться доказательством, как раз и состоит в том, что (после необходимой редукции к формальной форме) интуиция не должна быть нужна! По сути дела, этот критерий без формального док-ва правильности алгоритма выполнить не получается. И поэтому-то чувствует себя неуютно математик А.
А: компьютер чего-то там делает, делает, а потом говорит мне 'да' или 'нет' , а на каком основании следует ему верить?
Б: Да вот же программа, вы умеете программировать, посмотрите и убедитесь, что она делает что надо.
А: Ну, программисты всё же нередко ошибаются в таких вещах.
Б: Я проверил и убедился, вы проверили и убедились, чего ещё надо?
А: Чего надо? Надо мне возможности (пусть только принципиальной) элементарной, механической проверки, где интуиция подвести не может в принципе. Какое бы сложное док-во из теории чисел вы бы мне ни привели, я к такой проверке могу придти (редуцировав док-во к формальному уровню с помощью конктеста и возможно с вашей помощью). А с алгоритмом этим ничего подобного не получается. Нет у меня возможности разобрать его "по кусочкам" и убедиться шаг за шагом, что всё работает. То есть, нет формального док-ва правильности.
Но и это ещё не всё. Предположим, есть доказательство правильности работы алгоритма. Всё равно, для того чтобы всё док-во теоремы о четырёх цветах в целом превратить в формальное доказательство (с точки зрения математической логики), нам нужен не алгоритм, а процесс его выполнения. Здесь кроется последняя иллюзия: алгоритм - формальный объект, но это не тот формальный объект. Описание алгоритма ничего не доказывает; доказывает его выполнение.
Разницу между ними легко объяснить на примере того же деления в столбик. Алгоритм там - набор инструкций: делайте то-то и так-то. Но если вдруг кому-то взбредёт в голову формально доказать с помощью этого алгоритма, что 2444/47 = 52 (не советую), то ему мало будет доказательства правильности алгоритма и самого алгоритма. Ему нужна будет сама бумажка с записанными на ней последовательными шагами, т.е. процесс выполнения. Только тогда он сможет выписать формальное доказательство того факта, что 2444/47 = 52. (в терминах машин Тюринга ему нужна не таблица переходов машины, а полный набор конфигураций машины от начала работы и до остановки).
Я не требую от авторов док-ва теоремы о цветах того, чтобы они выписали формальное доказательство по всем правилам мат. логики - это нереально. Но я требую (точнее, не я, а математик А, сам того не зная, требует) принципиальной достижимости такого формального доказательства. А в случае с теоремой о цветах этот критерий не выполняется по двум причинам:
а) нет доказательства правильности алгоритма.
б) нет записи его работы - только эта запись и может служить базисом для формального доказательства, сам алгоритм - всего лишь рецепт, который ничего не доказывает. Но эта запись слишком длинна - именно потому что мы не можем сами вручную выполнить этот алгоритм, нам нужен компьютер. Таким образом, мы не можем, даже имея при себе все мета-данные, преобразовать их в формальное доказательство, и поэтому не можем до конца поверить в предлагаемое нам доказательство. Неудивительно, что А чувствует себя неуютно и пытается так или иначе сохранить подозрительное отношение к нему, не дать ему все "математические права".
Пожалуй, пока всё. Может быть, потом ещё заключение допишу, но явно не сегодня.
Постараюсь, наконец, увязать всё это вместе. Для этого мне нужно посмотреть внимательнее на то, что математики считают доказательством, а что не считают (не учитывая сейчас эти проблемы с компьютерами и программами). Чтобы немного сэкономить время и место, я не буду подробно проводить разбор и обосновывать его, а вместо этого приведу собственно краткое описание своей точки зрения; если кто-то с ней не согласен, пожалуйста оспорьте:
Математическое доказательство на практике никогда не формально (не является формальным доказательством с точки зрения мат. логики), но всегда сохраняется принципиальная возможность относительно легко добиться абсолютной строгости. Что это значит? Доказательство написано не на формальном языке, а на некоем многоуровневом мета-языке, причём уровни косвенности легко могут множится и пересекаться. Например, заявление вроде "итак, существует как минимум одно решение уравнения (1); пусть a - одно такое решение" очень легко поддаётся формализации. Кусок текста "... но этот случай легко вытекает из леммы 3.41" формализовать сложнее: что значит "легко"? Но математик, владеющий контекстом, с лёгкостью подставит вместо "легко" нужные элементарные шаги, после чего весь процесс можно будет формализовать и превратить в формальное доказательство. Практически каждый шаг в математическом док-ве требует владения конктекстом на самых разных уровнях, начиная с аксиом данной структуры и их элементарных следствий, и кончая сложными результатами, на которые стоят библиографические ссылки. Но все эти детали во время чтения и понимания доказательства математик может подставить, неизвестные ему результаты, на которые ссылаются, принять в качестве допущений, и т.д.
Важно понять, что, с одной стороны, я говорю о принципиальной возможности - никто на самом деле не занимается подобным переводом в формальную цепочку утверждений - но с другой стороны, настаиваю на абсолютной незаменимости этого требования, без которого доказательство не может больше считаться законным и верным.
Если отвлечься на секунду в историю математики, то я утверждаю, что войны конца 19-го и начала 20-го веков между знаменитыми математиками и целыми школами касательно допустимых и недопустимых методов доказательств настолько потрясли математическое сообщество, что де-факто был принят этот, описываемый мной, неформальный и интуитивный метод определения того, что есть математическое доказательство, который опирается на достигнутое к тому времени понимание формального док-ва как строгого математического объекта. Этот метод показал себя с лучшей стороны: интуиционизм уже давно не беспокоит практически никого из практикующих математиков, а споры вокруг той же аксиомы выбора не приводят к расколам и отказу от достигнутых результатов.
Очень вкратце попробую обосновать своё требование принципиальной формализабильности как главного критерия на то, чтобы считаться доказательством. Возьмём пример, который как раз могут привести мне в качестве контраргумента. Пусть есть некая очень сложная статья, написанная математиком В, и математик Д её читает. В какой-то момент В пишет: "а этот случай доказывается аналогично (б), с соответствующими измененями". Д, предположим, принимает во время чтения это на веру; но если мы попросим его формализовать всё доказательство, он вернётся к этому месту и споткнётся: не получается у него ничего аналогично (б). Может, он слишком глупый, или не хватает чего-нибудь из контекста, или ещё чего. Но доказательство всё же верно (предположим мы), просто у Д не получается его формализовать - что же теперь, это не доказательство? Если бы В стоял рядом, он бы в один момент всё Д объяснил.
Да, это верное доказательство. Но, я думаю, мы можем сойтись на том, что оно не было полностью передано Д. Есть некое верное доказательство в голове у В, есть некая его репрезентация в журнальной статье, но у Д не получается из этой репрезентации обратно построить доказательство, т.к. в репрезентации (или в голове Д) чего-то существенного не хватает. Не хватает, по сути дела, какого-то контекста. Даже если там есть просто трудный переход от одного утверждения к другому, и Д недостаточно натренирован в данной области, чтобы этот переход совершить, всё равно же понятно, что в принципе можно было бы это медленно разжевать по кусочкам, чтобы Д мог за этим проследовать - просто В на такие мелочи не разбрасывается. То есть, так или иначе, доказательство (как некий объект) не было успешно передано от В к Д. Поэтому оно и не проходит тест на интуитивную формализабильность. Именно потому, что не проходит, мы и делаем вывод, что у Д нет доказательства (хоть у В и есть). Это и демонстрирует истинность этого критерия.
Для чего нужна вся эта бодяга? Для того, конечно, чтобы математики могли быть уверены в том, что они могут проверить работы друг друга (и понять, заодно; невозможно понять, если не получается убедиться в истинности). Здесь я опять же говорю о принципиальной возможности; естественно, есть куча статей, непонятных никому, кроме их авторов; есть куча статей с ошибками, иногда грубыми, которые никто не заметил, и т.д. и т.п. Но в принципе у математика Д должна быть возможность проверить утверждения математика В. Но что значит "проверить"? Математик В может "мамой поклясться" Д, что у него всё правильно, и тот может поверить, но проверкой это, очевидно, не будет. Проверка как раз и возможна только потому, что есть принципиальная возможность редукции к абсолютно строгой, формальной, форме; как эта редукция выполняется - зависит от принятой нотации, степенью владения контекстом, стандартными сокращениями и т.д. и т.п.; но в любом случае эта редукция возможна и обязательно является чем-то принципиально возможным и осуществимым (feasible); просто никто этого не делает ввиду утомительности и ненужности.
Ох, расписался. Ну да ладно. Итак, весь этот кусок между двумя линиями был посвящен природе математического доказательства.
Вернёмся, наконец, к теореме о четырёх цветах. У неё есть некое нетривиальное доказательство, с теоретической и компьютерной частями, как я описал в своей первой записи. Применим к нему наш критерий. Можем ли мы его формализовать?
Теоретическая часть легко поддаётся формализации, а вот с практической несколько сложнее. В ней мы имеем дело с формальным описанием некоторого алгоритма (алгоритма, не компьютера! для этого важного различия мне нужна была вся дискуссия о двух типах доверия). Этот алгоритм проверяет, например, что все 600+ конфигураций из некоего конечного набора не могут принадлежать контрпримеру к теореме. Делает он это путём сложного интенсивного перебора возможностей редуцировать эти конфигурации при помощи некоего конечного набора правил редукции (применимость и достаточность которого мы тоже доказали в теоретической части).
Как вы сказали, что делает этот алгоритм? Он проверяет... Стоп. Откуда мы это знаем?
И тут мы подходим к проблеме доверия алгоритму. Алгоритму деления в столбик мы доверяем потому, что можем легко доказать его правильность. А правильность нашего алгоритма в док-ве теоремы о цветах мы можем доказать?
Может быть, да, может быть, нет. Вообще говоря общая проблема доказательства того, что данный алгоритм выполняет то, что от него хотят, неразрешима в принципе. Конечно, обычно мы имеем дело с не такими уж сложными алгоритмами, но, с другой стороны, вся область формальной верификации не так уж многого добилась за те десятки лет, что она существует. Доказывать правильность очень простых численных алгоритмов мы умеем; чего-то посложнее, с большим пространством перебора и нетривиальной логикой - вовсе необязательно.
Но так или иначе, можем мы доказать правильность алгоритма или нет, такое доказательство вместе с самим алгоритмом и всем остальным нам не предоставляется. У нас его нет. О верности алгоритма мы вынуждены судить "на глазок", пользуясь интуицией программиста. Но суть нашего критерия того, чтобы считаться доказательством, как раз и состоит в том, что (после необходимой редукции к формальной форме) интуиция не должна быть нужна! По сути дела, этот критерий без формального док-ва правильности алгоритма выполнить не получается. И поэтому-то чувствует себя неуютно математик А.
А: компьютер чего-то там делает, делает, а потом говорит мне 'да' или 'нет' , а на каком основании следует ему верить?
Б: Да вот же программа, вы умеете программировать, посмотрите и убедитесь, что она делает что надо.
А: Ну, программисты всё же нередко ошибаются в таких вещах.
Б: Я проверил и убедился, вы проверили и убедились, чего ещё надо?
А: Чего надо? Надо мне возможности (пусть только принципиальной) элементарной, механической проверки, где интуиция подвести не может в принципе. Какое бы сложное док-во из теории чисел вы бы мне ни привели, я к такой проверке могу придти (редуцировав док-во к формальному уровню с помощью конктеста и возможно с вашей помощью). А с алгоритмом этим ничего подобного не получается. Нет у меня возможности разобрать его "по кусочкам" и убедиться шаг за шагом, что всё работает. То есть, нет формального док-ва правильности.
Но и это ещё не всё. Предположим, есть доказательство правильности работы алгоритма. Всё равно, для того чтобы всё док-во теоремы о четырёх цветах в целом превратить в формальное доказательство (с точки зрения математической логики), нам нужен не алгоритм, а процесс его выполнения. Здесь кроется последняя иллюзия: алгоритм - формальный объект, но это не тот формальный объект. Описание алгоритма ничего не доказывает; доказывает его выполнение.
Разницу между ними легко объяснить на примере того же деления в столбик. Алгоритм там - набор инструкций: делайте то-то и так-то. Но если вдруг кому-то взбредёт в голову формально доказать с помощью этого алгоритма, что 2444/47 = 52 (не советую), то ему мало будет доказательства правильности алгоритма и самого алгоритма. Ему нужна будет сама бумажка с записанными на ней последовательными шагами, т.е. процесс выполнения. Только тогда он сможет выписать формальное доказательство того факта, что 2444/47 = 52. (в терминах машин Тюринга ему нужна не таблица переходов машины, а полный набор конфигураций машины от начала работы и до остановки).
Я не требую от авторов док-ва теоремы о цветах того, чтобы они выписали формальное доказательство по всем правилам мат. логики - это нереально. Но я требую (точнее, не я, а математик А, сам того не зная, требует) принципиальной достижимости такого формального доказательства. А в случае с теоремой о цветах этот критерий не выполняется по двум причинам:
а) нет доказательства правильности алгоритма.
б) нет записи его работы - только эта запись и может служить базисом для формального доказательства, сам алгоритм - всего лишь рецепт, который ничего не доказывает. Но эта запись слишком длинна - именно потому что мы не можем сами вручную выполнить этот алгоритм, нам нужен компьютер. Таким образом, мы не можем, даже имея при себе все мета-данные, преобразовать их в формальное доказательство, и поэтому не можем до конца поверить в предлагаемое нам доказательство. Неудивительно, что А чувствует себя неуютно и пытается так или иначе сохранить подозрительное отношение к нему, не дать ему все "математические права".
Пожалуй, пока всё. Может быть, потом ещё заключение допишу, но явно не сегодня.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
Re: Èçâèíèòå
Date: 2001-09-12 05:22 pm (UTC)Íåò, ÿ ÷óâñòâîâàë, ÷òî ïðèìåðíî ê ýòîìó êëîíèòå, íî âñå æäàë ïîäâîõà. È, êàæåòñÿ, íå äîæäàëñÿ. Èëè íå çàìåòèë.