Случайные туры вокруг улик

Сегодня Райан Уильямс опубликовал статью о arXiv (ранее появившуюся в SIGACT News), содержащую менее техническую версию своего недавнего метода нижней границы ACC .

Мой вопрос не о самой технике (конечно, заслуживающей огромной похвалы), а о стиле бумаги. В аннотации он пишет:

Доказательство будет описано с точки зрения того, кто пытается его обнаружить.

Потрясающе! В разделе «Фон» он добавляет:

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

Это удивительно, и я впервые это вижу. Я всегда удивлялся, почему авторы статьи не пишут, как они получили доказательства, включая неудачные подходы, которые они пробовали, прежде чем попасть на путь, который привел к решению. Когда я увидел статью Райана на arXiv, я почувствовал сильную мотивацию читать. Я считаю это революционной статьей с этой точки зрения. В большинстве случаев единственное, что вы можете сделать с бумагой, это проверить ее правильность.

Вопрос в следующем:

• Вам известны другие работы в TCS, в которых прорывные результаты представлены в «случайном туре», а не в серии технических лемм?

Я имею в виду публикации в журналах, а не сообщения в блогах или технические отчеты.

Кроме того, я отметил это как большой список с надеждой, что это будет на самом деле.

Есть статья (2001) аналогичного стиля, написанная Ловом Гровером, в которой описывается путь к его прорывному алгоритму квантового поиска (1996).

Тим Гауэрс - фанат такого рода вещей. См. Конкретно его изложение метода приближений Разборова .

В своем вступлении Гоуэрс ссылается на мою пояснительную статью о принуждении , которая является (не совсем успешной) попыткой сделать то же самое для принуждения. Форсирование обычно считается техникой в ​​логике и теории множеств, но иногда оно попадает в TCS. Он возникает при изучении ограниченной арифметической и пропозициональной доказательственной сложности (Крайчек и Такеути - два исследователя, которые преследовали эту связь), и концепция универсального оракула связана с концепцией универсального фильтра.

(Это началось как комментарий и получилось слишком долго).

Вам может понравиться статья Уильяма Терстона « Доказательство и прогресс в математике» .

Математика в некотором смысле имеет общий язык: язык символов, технических определений, вычислений и логики. Этот язык эффективно передает некоторые, но не все способы математического мышления. Математики учатся переводить некоторые вещи почти бессознательно из одного ментального режима в другой, так что некоторые утверждения быстро становятся ясными. [...]

Люди, знакомые со способами работы в подполе, распознают различные шаблоны утверждений или формул как идиомы или обходные пути для определенных понятий или мысленных образов. Но для людей, еще не знакомых с тем, что происходит, одни и те же закономерности не очень освещают; они часто даже вводят в заблуждение. Язык не живой, кроме тех, кто его использует. [...]

Мы, математики, должны приложить гораздо больше усилий для распространения математических идей. Чтобы достичь этого, мы должны уделять гораздо больше внимания сообщению не только наших определений, теорем и доказательств, но и нашего мышления. Нам нужно оценить ценность разных способов мышления об одной и той же математической структуре. Нам нужно сосредоточить гораздо больше энергии на понимании и объяснении базовой психической инфраструктуры математики, и, следовательно, меньше энергии на самых последних результатах. Это влечет за собой разработку математического языка, который эффективен для радикальной цели передачи идей людям, которые их еще не знают.

Что касается исходного вопроса, существуют статьи, в которых не представлены идеи в формате «Определение-теорема-доказательство» (DTP). У Тимоти Чоу есть несколько работ, посвященных обмену идеями (хотя это не первые (или вторые) статьи по теме / результату).

1. Вы могли бы изобрести спектральные последовательности , Тимоти Чоу, Уведомления об AMS
2. Форсинг для чайников , Тимоти Чоу

Одна из возможных причин распространенности формата DTP заключается в том, что мы все просто привыкли к нему из книг и газет. Рецензенты (и читатели) иногда находят, что нестандартный стиль письма отвлекает. Срединная позиция - бумаги, которые аккуратно разбивают читателя на результат. Есть статьи, которые представляют собой особый случай или простую задачу, иллюстрирующую общую идею.

1. Топологическая структура асинхронной вычислимости , Морис Херлихи и Нир Шавит. В статье много иллюстраций и демонстрируется общая идея простого протокола перед применением основной теоремы для решения некоторых открытых задач.
2. Логика и узнаваемых наборов целых чисел$p$ : Вероник Брюяр, Жорж Гансель, Кристиан Мишо и Роджер Виллемер. Изложение в стиле опроса прекрасного результата: наборы натуральных чисел, которые кодируются конечными автоматами, независимо от выбранной базы, в точности определяются в арифметике Пресбургера. В статье приведены многочисленные примеры, рассматриваются частные случаи перед общим случаем и приводится историческая справка о ошибочных попытках доказательства.

Ни одно обсуждение нестандартного изложения замечательных идей не будет полным без упоминания о работе Жана-Ива Жирара . «Уникальное», пожалуй, лучшее слово для его описания (не будучи дипломатичным или саркастичным). Из бумаги Линейная логика .

Философское толкование правил Хейтинга оставляет на самом деле очень мало места для дальнейшего обсуждения интуиционистского исчисления; но кто-нибудь когда-нибудь серьезно пытался? Фактически, линейная логика, которая является четким и понятным продолжением обычной логики, может быть достигнута посредством более четкого анализа семантики доказательств (не очень далеко от компьютерного подхода и, таким образом, отнесена к следующему разделу), или определенными более или менее непосредственными соображениями о последовательном исчислении. Эти соображения имеют непосредственное геометрическое значение, но чтобы понять их, нужно забыть о намерениях, помня с китайским лидером, что важен не цвет кошки, а тот факт, что она ловит мышей.

Позже:

Есть еще люди, которые говорят, что для создания информатики нужен паяльник; Это мнение разделяют логики, которые презирают информатику, и инженеры, которые презирают теоретиков. Однако в последние годы потребность в логическом изучении программирования стала все яснее и яснее, и связь логика-информатика кажется необратимой. [...]
В некотором смысле логика играет ту же роль, что и геометрия в физике: геометрический каркас налагает определенные результаты сохранения, например формулу Стокса. Симметрии логики, по-видимому, выражают глубокое сохранение информации в форме, которая еще не была правильно концептуализирована.

Возможно, авторы не включают эти неудачные попытки и историю исследования в свои опубликованные статьи из-за ограничений, наложенных редакторами и членами ПК. Я предполагаю, что для журнала очень необычно (и, возможно, еще более необычно для конференции) принять статью, основная часть которой посвящена неудачным попыткам. Но в большинстве случаев, если вы поговорите с авторами или экспертами в этой области, они объяснят историю и неудачные попытки (и многие говорят об этом на семинарах).

Я видел, как несколько авторов объясняли, откуда взялись идеи в их статьях. В качестве примера Жирар объясняет в своей статье, что идея линейной логики возникла из попытки найти денотационную семантику для интуиционистского ИЛИ. Вы можете найти такую ​​информацию также в монографиях и биографиях известных исследователей и в томах, посвященных им ( вспомнились автобиография Халмоса и более поздняя «Kreiseliana: About and Around Georg Kreisel » под редакцией Одифредди, есть также тома и статьи). посвященный некоторым теоретикам сложности). Надеемся, что больше людей сделают то, что сделал Райан, и систематически объяснят процесс и расскажут историю.

PS: вы можете думать об этом как о устной традиции исследования :) (что-то похожее на Устную Тору, которую нельзя было записать ).

Существует опубликованная статья Ласло Бабая (1990) в форме басни об Артуре и Мерлине, описывающая драматическую последовательность событий, приведшую сообщество к результату IP = PSPACE в 1989 году, который был очень невероятным всего годом ранее.