The nature of my research and why I do it. EWD993.
(Речь на официальном ленче в Лас-Крусес, 14 ноября 1986 года.)
В 1955 году, будучи молодым и многообещающим физиком-теоретиком, я решил вместо этого посвятить свою научную жизнь программированию, поскольку я чувствовал, что программирование будет бо́льшим интеллектуальным вызовом.
Следующее десятилетие я посвятил сбору опыта, проектируя и реализуя системы всё большего размера, амбиций и сложности. К 1965 году я мог убедительно доказать, что способность обнаружить на ранней стадии необходимость в прикладной теории является одним из наиболее важных активов программиста.
Ещё через пять лет я сформулировал ядро задачи программирования: как предотвратить создание сложности, которой невозможно овладеть. Стало ясно — по крайней мере, мне — что эта задача является математической. К 1975 году я разработал формальную систему, в которой можно разрабатывать одновременно программу и доказательство её корректности.
Я был очень взволнован, так как всё сложилось прекрасно: было показано, что ещё одно человеческое занятие в принципе поддаётся математической обработке.
С чисто технической точки зрения, в ретроспективе, то, что мне понадобилось не менее двадцати лет, чтобы достичь этого этапа, кажется удивительным. С социологической точки зрения эту медлительность понять легко: мой вывод отвергали практически везде. Программисты, а ещё больше их производственные менеджеры считали, что вся эта идея слишком академическая, чтобы быть важной на практике. (Многие из них до сих пор так считают.) Математики игнорировали или отрицали этот вывод, потому что тип математики настолько отличался от того, к которому они привыкли, что они признавали её математикой со скрипом. (Многие из них до сих пор не признают.) В то время я не понимал силу их научного противодействия, но она быстро убедила меня, что информатика должна выработать себе тот тип математики, в котором нуждается. В ретроспективе, я могу понять причину, по которой её отвергали: видимо, акценты были расставлены совершенно неправильно. По сути, тогда как в течение последнего столетия математика как интеллектуальная дисциплина стала всё больше и больше ориентированной на знания, бо́льшая часть того знания была для нас полностью не релевантной; для нас, например, выбор нотации намного чаще выглядел критичным.
Итак, я анализировал набор тех привычек и предосторожностей, которые следует культивировать для математического ответа на задачу программирования. Вначале я регистрировал эти исследования под знакомым заголовком «методология программирования».
Но потом начали происходить самые разные события. Благодаря тому, что язык программирования можно механически интерпретировать, он неизбежно представляет собой формальную систему некоторого рода, и поэтому вывод программы неизбежно является в высокой степени формальной деятельностью. Но заниматься этой деятельностью можно только в том случае, если мы найдём способ предотвратить взрывной рост количества необходимой формальной работы. Как только краткость становится сознательной целью, человек спрашивает себя: «Из-за чего формальный вывод становится длинным?» Без особого удивления он обнаруживает, что главным виновником является разбор случаев (case analysis). Тогда человек спрашивает себя: «Какие у нас есть приёмы избежать разбора случаев?» И он находит несколько таких, иногда даже очень эффективных. (Дальше в этом выступлении, если позволит время, я расскажу о некоторых из них.)
После этого чтение хорошо известной, везде рекомендуемой и широко используемой математической книги оставляет его в ужасе! Рассуждения — и даже формулировки теорем — часто бывают настолько невероятно неуклюжими, что он должен заключить, что его исследования относятся к математике в общем.
Пример. В «An Introduction to Number Theory» Харольда М. Старка главная теорема сформулирована следующим образом:
Если n — целое число, большее 1, то или n простое, или n является конечным произведением простых чисел.
Но 1, разумеется, конечное, и, определив произведение 1 множителя — а как иначе? — равным этому множителю, мы можем избавиться от разбора случаев в следствии:
Если n — целое число, большее 1, то n является конечным произведением простых чисел.
Но 0 также, разумеется, конечное, и, определив произведение 0 множителей — а как иначе? — равным 1, мы можем избавиться от исключения:
Если n — положительное целое число, то n является конечным произведением простых чисел.
В конце концов мы можем избавиться от идентификатора n:
Положительное целое число является конечным произведением простых чисел.
(Конец примера.)
В связи с примером выше я хочу подчеркнуть, что неуклюжая формулировка теоремы — это прототип неудачного интерфейса в том смысле, что она приводит к увеличению количества работы по обе стороны забора: из-за неё труднее доказывать теорему и труднее использовать.
Таким образом я вынужденно занялся более широкой темой, чем просто «методология программирования». Иногда я называю её — в основном для себя — «выпрямлением математических рассуждений» (streamlining of the mathematical argument), иногда я называю её «методологией математики», название, которое выбрано частично для того, чтобы выразить, что мы исследуем то, до каких пределов опыт, накопленный в методологии программирования, можно перенести в математику в общем, частично потому, что оно отражает смещение акцента, а именно, со шлифовки существующих рассуждений на дисциплину конструирования новых рассуждений в правильном порядке. Со временем на сцену вышли эвристики.
Эта деятельность показала нам новую ценность формализмов как альтернативы словесному мышлению. Мы узнали, что формализмы есть нечто намного большее, чем сокращения записи: сейчас мы рассматриваем их как главное средство, освобождающее нас от оков наших родных языков.
Позвольте мне привести два примера того, насколько наши языки запутаны. По закону контрапозиции (Law of the Counterpositive), A⇒B есть то же, что ¬B⇒¬A. Лингвистически импликация выражается тем, что мы ставим перед предпосылкой «если», например
Завтра будет дождь, если ветер не переменится.
является совершенно приемлемым предложением. Контрапозиция, однако, даёт:
Ветер переменится, если завтра не будет дождя.
забавное утверждение, по меньшей мере. Очевидно, что союз «если» несёт с собой целую охапку внелогических смыслов до/после, причина/следствие (дихотомия, которой нет места в неживой природе (inanimate world)). Словесная математика научилась очищать союз «если» от внелогических смыслов, но лишь до определённой степени, как показано в следующем примере. Логическая эквивалентность, синоним взаимной импликации, выражается словами «тогда и только тогда», как в
Целое число n чётно тогда и только тогда, когда n+1 нечётно.
Пока что всё хорошо, но посмотрите на следующее предложение:
Я вижу обоими глазами тогда и только тогда, когда я вижу одним глазом тогда и только тогда, когда я слеп.
Лингвистически это полная чепуха, потому что структурный анализ предложения даёт два результата. Из-за его явной синтаксической неоднозначности оно не может быть приемлемым предложением. Логически оно имеет форму A≡B≡C, и мы, как ни удивительно, можем опустить скобки, так как булев оператор эквивалентности является ассоциативным: цепная эквивалентность означает, что количество ложных операндов чётно, и, поскольку у меня не больше 2 глаз, приведённое выше утверждение, хотя и приводит в недоумение, формально является корректным.
В математических рассуждениях эквивалентность используется очень мало, и я нисколько не сомневаюсь, что этот факт тесно связан с лингвистической ущербностью словесного варианта фразы «тогда и только тогда». Учитывая это, я пришёл к выводу, что учить логику, транслируя формулы в прозу — это ошибка, так как это именно тот метод, от которого мы хотим удалиться. Моя характеристика «очень мало» не преувеличение: разумное использование эквивалентности сократило много существующих рассуждений на порядок. (Я видел сокращения в 16—24 раза.) Объяснение этого, возможно, коренится в хороших свойствах эквивалентности, таких как симметрия, ассоциативность и тот факт, что дизъюнкция дистрибутивна над ней; более того, оно имеет полную силу равенства, то есть x = y ⇒ f.x = f.y.
Формализация, в общем случае сведение большей части математики к вычислению, не является нашей целью. Просто так получилось, и в связи с этим я хочу подчеркнуть, что наши наблюдения полностью противоположны тому, что повсеместно считается несокрушимой догмой, что формальное рассмотрение всегда длинное, скучное, трудоёмкое, обычно содержит ошибки и тому подобное. Наоборот, более вычислительное рассмотрение всегда ведёт к более чёткому рассуждению. Я считаю, что формальные методы не заслужили эту дурную славу. Наш опыт настолько поразительный и, в то же время, настолько противоречит распространённому ощущение, что вы, возможно, отказываетесь мне верить. Так позвольте мне отважно предложить объяснение тому, почему так много людей имеют такие дурные впечатления о формальной математике.
(i) Устоявшаяся нотация во многих случаях плохо приспособлена к нашим потребностям в манипуляции, например, потому что она неоднозначна или не даёт нам нужной комбинаторной свободы.
(ii) Некоторые стили вычислений вводят много шагов, без которых лучше обойтись. При использовании ассоциативного оператора кто-то может ограничить себя до выражений с полным набором скобок и тасовать скобки, когда нужно, опираясь на
(X ∙ Y) ∙ Z = X ∙ (Y ∙ Z).
Намного проще просто опустить избыточные скобки.
(iii) Многие люди не смогли выработать достаточно твёрдое умение писать: они думают, что формальная математика трудна, тогда как на самом деле им просто немножко не хватает координации между рукой и глазами.
У Лейбница была мечта: свести все математические рассуждения к универсально применимому исчислению. Так как мы не Лейбницы, наша мечта скромнее: мы без колебаний вычисляем тогда, когда это удобно.
Но мы обязаны упомянуть Лейбница в связи с информатикой, потому что очень вероятно, что эта дисциплина взяла на себя задачу воплотить бо́льшую часть его мечты. Причины этого следующие:
Если воплотить мечту Лейбница действительно завещано нам, давайте проследим, чтобы она не превратилась в кошмар!