Настроение:	optimistic
Музыка:	Einstürzende Neubauten -- Negativ Nein (live)

Break up your fallow ground, and sow not among thorns.
В январе 2014 года чел из университета Токио разместил работу, в которой улучшил показатель степени для сложности быстрого матричного умножения с 2.3729269 до 2.3728639. В 2014 г. Да еще и в ворде статью написал. Можно было бы отнести в разряд курьезов, но давайте посмотрим на список того, что считают главными нерешенными проблемами в computer science. Быстрое матричное умножение (с упоминанием этого чела) там сразу после P=?NP и односторонних функций. Если вам нужно было определение словосочетания ``ссаный позор'', то вот по-моему неплохой кандидат.



IMO, цель computer science -- это более справедливое разделение труда между человеком и машиной. Не все средства хороши для ее достижения. Нужны концептуальные прорывы, а всякие трюки в жанре ``чертики из табакерки'' не нужны. Концептуальные прорывы -- это, например, когда люди думают над тем, что такое ``data'', индукция, а потому расширяют механизм deriving в Haskell, для автоматического определения разных полезных функций. Очень удобно, меньше работы. Или вот все что связно с автоматическим построением парсеров по описанию грамматик определенных классов. Хорошая теория помогает получать полезные инструменты. Поэтому эпистемологические ценности должны превалировать.

Чем, скажем, должна заниматься теория сложности? Ну вот есть теорема Поста о функциональной полноте. Простая, понятная, конструктивная и полезная. Есть язык спецификаций (таблицы булевых функций), язык [domain specific] программирования (заданная система функций с операцией композиции), есть отношение ``программа реализует спецификацию''. Теорема в числе прочего позволяет построить хотя бы одну функцию, реализующую данную спецификацию, или доказать, что это невозможно. Поскольку, вообще говоря, имеется много способов реализовать заданную спецификацию, имеет смысл ввести меру сложности для программ и изучать всякие вопросы, которые естественно возникают. Теория сложности, как мне кажется, должна исследовать аналогичные вопросы для разных языков спецификаций, программирования (не обязательно bullshitTuring-complete) и способов измерения сложности. Естественно, в общем случае такая задача неразрешима, но ничто не запрещает существование интересных случаев, в которых какое-то адекватное описание возможно.

Вот скажем как устроено множество алгоритмов поиска подстроки в строке? Это очень зависит от базового языка, такой вопрос явно не под силу современной науке. Есть такой-то, с такой-то сложностью, есть такой-то... Как описать комбинаторику этого дела? С чего тут вообще начать? Есть интересный подход, позволяющий выводить программы из спецификаций, заданных отношениями, называется program transformation. Отлично изложен в этой книжке на примере задач так называемого динамического программирования. Он не отвечает на все вопросы, но хоть что-то. Как только сузили область, оказалось, что можно получать интересные результаты.

Замечу еще, что видимо не случайно мастера древности типа Кнута или де Брейна были еще и хардкоровыми комбинаторщиками. Честный анализ сложности заключается в вычленении underlying комбинаторных структур, а не асимптотических оценок.

Причем тут теории типов? Продвинутые интуиционистские теории типов, основанные на Мартин-Лефе, -- это хорошие языки для описания и рассуждения о вычислениях. Они могут передавать тонкие смыслы. В них спецификации задаются на уровне типов, программы -- это типизированные выражения, а отношение ``программа реализует спецификацию'' -- это ``выражение t имеет тип T''. Интересно, что Колмогоров еще в тридцать каком-то году написал, что интуиционистское исчисление высказываний (которое эквивалентно просто типизированному лямбда-исчислению) нужно интерпретировать как исчисление задач. Он там, конечно, точно не определял, что такое задача; приводил в пример геометрические задачи на построение. Теперь-то мы понимаем, что речь идет о программах. Великого ума, видать, был мужик.

Теории типов отлично описывают логическую сторону вычислений, но как прикрутить к ним комбинаторику -- большой вопрос. Это не единственная проблема. Во всех имеющихся реализация типа Agda, Epigram или Idris есть проблема с модульностью. Проблема заключается в том, что никто не знает что это. У МакБрайда есть разные интересные инструменты, связанные с этой проблемой. А кто изучал свойства теории типов вместе механизмом рефлексии? А вопросы, связанные с новыми техниками оптимизации, основанными, например, на вычислительно иррелевантых типах? Кто всем этим будет заниматься? Тютькин?



На самом деле я настроен весьма оптимистично. В Haskell community полно полностью поехавших гиков, которые, вдоволь наигравшись с Хаскеллем, переходят на более тяжелые наркотики. А это означает, что more crazy shit coming soon along w/ some other cool stuff.