Впечатления о симпозиуме по метавычислениям
Не знаю, как лучше перевести английский термин workshop применительно к научным встречам, вот и взял привычное слово...
Симпозиум проходил в Переславле в начале июля. Сразу же скажу основное впечатление. Если на логический коллоквиум ORFIC в Питера в июне я ехал с большими надеждами. но в итоге оказался практически разочарован (хотя одну идею все-таки вынес), то здесь я относился практически без всяких позитивных ожиданий, но оказалось очень интересно и вынесли многое (и я, и моя дочь тоже).
Метавычисления - это преобразования хорошо устроенных программ, соединяющие элементы частичных вычислений и простейшие доказательные конструкции (типа установления вложимости одного символьного метарезультата в другой). В нынешней их форме в результате получается дерево возможных обобщенных исполнений программы, на базе которого либо строится новая программа, которая чем-то лучше, либо, если вычисления имеют дело не с самими значениями, а с их свойствами, производится ее анализ. В частности, метавычисление может быть инструментом верификации или фальсификации (программа верифицирована. если в получившемся дереве каждый путь завершается истиной; она фальсифицирована, если какой-то завершается ложью).
Таким образом, метавычисления - один из самых теоретически емких разделов программирования, и вместе с тем находящийся на грани теории и практики. В частности, А. Немытых проверил с помощью вычислений ряд сетевых протоколов и в одном из них нашел ошибку. Автор, которому он сообщил ее. даже не поблагодарил его и потииихонечку ее исправил в следующих публикациях. То, что автор западный ученый, ничего не значит: так бы мог поступить и наш...
Метавычисления позволяют оптимизировать программы намного сильнее, чем обычные методы оптимизации. В частности, после разгоревшейся дискуссии, когда шотландская группа декларировала. что они могут достичь более чем линейной оптимизации по времени, моя дочь сразу же нашла пример, когда это может делать классический, полностью описанный в книге А. Немытых, метакомпилятор, а не их засекреченная система без открытых исходных кодов, а затем она нашла сама и откопала в очень трудно написанной книге Немытых примеры, когда (правда, по-идиотски написанные) программы оптимизируются экспоненциально. Конечно же, после метавычислений программа может оказаться построенной абсолютно фантастически, и это прекрасный метод обфускации, как заметили Джонс и Гамильтон :). Правда, написать на Рефале или высокоуровневую процедуру на Haskell, Lisp или HOPE, не хуже обфускирует для тех же самых 99.9%...
Практически все доклады были интересными. Как сказал один мой знакомый по поводу другой конференции: "В один из дней один из докладов мне не понравился, но уже не помню, какой". Особенно я отметил бы принципиальные работы Р. Глюка, Гречаника, Романенко и Слесаренко. Доклад болгарина Крустева показал применение суперкомпиляции к реальным задачам. Доклады симпозиума опубликованы и выложены в http://meta2012.pereslavl.ru/papers/'meta2012-proceedings.pdf.
Меня пугали. что мой доклад никто не поймет, что программисты от одного слова "группа", тем более, сопровождаемого "конструктивная логика", упадут в обморок, а очнувшись, заорут: "А на фига нам это нужно знать??? Ты нам код или результат счета покажи!" Оказалось вовсе не так. И вообще, надеюсь что в ходе симпозиума удалось кое-что переломить в отношении связи теории и практики.
А именно, начали диагностироваться случаи. когда теоретические результаты используются как молитва. а не по существу (в частности, по традиции такое произошло здесь с изоморфизмом Карри-Ховарда, который суют везде, где его нет). Далее, когда в коммментариях прозвучали результаты направления, которое сейчас развивается прод названием reverse mathematics, где устанавливаются нижние границы средств, необходимых для доказательства существования решений некоторых задач. и было показано. что они означают с практической точки зрения (неизлечимо и невообразимо высокие нижние границы сложности вычислений), сообщество начало склоняться к тому, чтобы запретить слово "конечный". Надо говорить сложностные оценки, а не блаженненькое словечко, за которым могут скрываться страшные монстры.
Вообще, наметился ряд возможных мостов между суперкомпиляцией, логикой и алгеброй. Часто информатики не знают. что ломятся в давно уже открытую дверь. поскольку те же задачи описаны в других терминах. И слишком часто "практики" пытаются использовать теорию как молитву, а не как результаты и методы. Правда. и теоретикам здесь становится жить труднее: нужно уметь не только продолдонить результат, но и объяснить, каковы его следствия и принципиальные ограничения, к каким структурам он относится, и многое другое
Вот так закончилась первое мое научное мероприятие в Китежграде. А сейчас сижу над статьей, которая возникла из результатов обсуждений с Глюком и которая по мере развития становится все труднее и принципиальнее. Не думал. что еще и по алгебре придется работы писать...
Симпозиум проходил в Переславле в начале июля. Сразу же скажу основное впечатление. Если на логический коллоквиум ORFIC в Питера в июне я ехал с большими надеждами. но в итоге оказался практически разочарован (хотя одну идею все-таки вынес), то здесь я относился практически без всяких позитивных ожиданий, но оказалось очень интересно и вынесли многое (и я, и моя дочь тоже).
Метавычисления - это преобразования хорошо устроенных программ, соединяющие элементы частичных вычислений и простейшие доказательные конструкции (типа установления вложимости одного символьного метарезультата в другой). В нынешней их форме в результате получается дерево возможных обобщенных исполнений программы, на базе которого либо строится новая программа, которая чем-то лучше, либо, если вычисления имеют дело не с самими значениями, а с их свойствами, производится ее анализ. В частности, метавычисление может быть инструментом верификации или фальсификации (программа верифицирована. если в получившемся дереве каждый путь завершается истиной; она фальсифицирована, если какой-то завершается ложью).
Таким образом, метавычисления - один из самых теоретически емких разделов программирования, и вместе с тем находящийся на грани теории и практики. В частности, А. Немытых проверил с помощью вычислений ряд сетевых протоколов и в одном из них нашел ошибку. Автор, которому он сообщил ее. даже не поблагодарил его и потииихонечку ее исправил в следующих публикациях. То, что автор западный ученый, ничего не значит: так бы мог поступить и наш...
Метавычисления позволяют оптимизировать программы намного сильнее, чем обычные методы оптимизации. В частности, после разгоревшейся дискуссии, когда шотландская группа декларировала. что они могут достичь более чем линейной оптимизации по времени, моя дочь сразу же нашла пример, когда это может делать классический, полностью описанный в книге А. Немытых, метакомпилятор, а не их засекреченная система без открытых исходных кодов, а затем она нашла сама и откопала в очень трудно написанной книге Немытых примеры, когда (правда, по-идиотски написанные) программы оптимизируются экспоненциально. Конечно же, после метавычислений программа может оказаться построенной абсолютно фантастически, и это прекрасный метод обфускации, как заметили Джонс и Гамильтон :). Правда, написать на Рефале или высокоуровневую процедуру на Haskell, Lisp или HOPE, не хуже обфускирует для тех же самых 99.9%...
Практически все доклады были интересными. Как сказал один мой знакомый по поводу другой конференции: "В один из дней один из докладов мне не понравился, но уже не помню, какой". Особенно я отметил бы принципиальные работы Р. Глюка, Гречаника, Романенко и Слесаренко. Доклад болгарина Крустева показал применение суперкомпиляции к реальным задачам. Доклады симпозиума опубликованы и выложены в http://meta2012.pereslavl.ru/papers/'meta2012-proceedings.pdf.
Меня пугали. что мой доклад никто не поймет, что программисты от одного слова "группа", тем более, сопровождаемого "конструктивная логика", упадут в обморок, а очнувшись, заорут: "А на фига нам это нужно знать??? Ты нам код или результат счета покажи!" Оказалось вовсе не так. И вообще, надеюсь что в ходе симпозиума удалось кое-что переломить в отношении связи теории и практики.
А именно, начали диагностироваться случаи. когда теоретические результаты используются как молитва. а не по существу (в частности, по традиции такое произошло здесь с изоморфизмом Карри-Ховарда, который суют везде, где его нет). Далее, когда в коммментариях прозвучали результаты направления, которое сейчас развивается прод названием reverse mathematics, где устанавливаются нижние границы средств, необходимых для доказательства существования решений некоторых задач. и было показано. что они означают с практической точки зрения (неизлечимо и невообразимо высокие нижние границы сложности вычислений), сообщество начало склоняться к тому, чтобы запретить слово "конечный". Надо говорить сложностные оценки, а не блаженненькое словечко, за которым могут скрываться страшные монстры.
Вообще, наметился ряд возможных мостов между суперкомпиляцией, логикой и алгеброй. Часто информатики не знают. что ломятся в давно уже открытую дверь. поскольку те же задачи описаны в других терминах. И слишком часто "практики" пытаются использовать теорию как молитву, а не как результаты и методы. Правда. и теоретикам здесь становится жить труднее: нужно уметь не только продолдонить результат, но и объяснить, каковы его следствия и принципиальные ограничения, к каким структурам он относится, и многое другое
Вот так закончилась первое мое научное мероприятие в Китежграде. А сейчас сижу над статьей, которая возникла из результатов обсуждений с Глюком и которая по мере развития становится все труднее и принципиальнее. Не думал. что еще и по алгебре придется работы писать...