May 2nd, 2010

2019

Выразительность, теория категорий, моноидальные диаграммы, ISO 15926L

Хорошая нотация должна соответствовать хорошему языку (я тут осторожно пользуюсь терминологией ISO 24744 -- http://ailev.livejournal.com/817706.html) символ в понятие. Так, если речь идет о числах, то хорошая нотация должна быть позиционной, т.е. содержать один символ для каждой цифры (как арабская), а не несколько (как римская). При придумывании языков программирования, языков моделирования, языков онтологической работы становится важным эргономический (понятность человеку) аспект -- я приводил это в пример, когда рассматривал язык Дракон (http://ailev.livejournal.com/682893.html).

Поскольку мы тут пытаемся думать об "универсальном моделере", то становится интересной "универсальная нотация" (и, конечно, нотационная инженерия -- вспомним только одну из ее школ: http://ailev.livejournal.com/546301.html, http://ailev.livejournal.com/548756.html, http://ailev.livejournal.com/549681.html, http://ailev.livejournal.com/613067.html). Какие мы знаем попытки создать универсальную нотацию? Например:

1. Алфавитное письмо для естественного языка. Это те же римские числа для десятичной нотации.

2. Математика в ее современном/традиционном/не слишком древнем виде. Оставь надежду всяк сюда входящий (хотя, конечно, есть любители, для которых это "само совершенство, и адекватней не бывает"). Математики работают визуально, но затем выдают результаты в виде канонически предписанной смеси естественно-языковых текстов и алгебраических/логических выражений. Мало кто занимался попытками отмоделировать то, что у крутых математиков происходит во время мыслительного процесса "в голове" с целью затем создать нотацию на основе выявленных образов. А ведь это было бы очень интересно!

3. Язык схем СМДМ (http://www.fondgp.ru/lib/mmk/58). Тут без комментариев, но заход на универсальность их языка, несомненно, присутствует. Из интересного: СМДМ-методологи любят приговаривать, что мир не исчерпывается аристотелевской логикой и онтологией, поэтому отмоделировать предлагаемые ими ходы мысли тоже было бы любопытно. Но они свои ходы мысли не рефлексируют в той мере, чтобы можно было моделировать и затем предлагать нотацию. Ну, в том числе непонятно, какие задачи можно будет успешно решать с использованием их формализованной нотации. Оставим в списке как источник постоянных напоминаний, что не весь мир описывается в формализме BWW (Bunge-Wand-Weber, философский формализм, который лежит в основе большинства работ современных объектно-ориентированных разработок).

4. Онтологические языки: на 99% используется текстовая нотация логических языков. Нотации от никаких до ужасных, лучшее из предложенного человечеством в данной области -- таблички Gellish, которые неспециалист хотя бы может понять. Для подъема уровня языка используются специальные приемы работы, типа "шаблоны из части седьмой ISO 15926", которые на поверку оказываются использованием логического языка программирования в его "декларирующей" (а не собственно программирующей, "оценивающей") части.

5. Языки моделирования: победа UML, с маленькой примесью ER-нотации, а при попытке копнуть упираемся в логический язык ограничений (OCL).

6. Языки программирования, в том числе мультипарадигмальные. Нотация тут, наконец, перестала волновать -- наоборот, всех, начало волновать AST (abstract syntax tree). Ну, а дальше -- те же логические языки: ибо выражать нужно прежде всего беготню по этому самому дереву абстрактного синтаксиса.

Ну и так далее, примеров вы можете накидать и сами.

Это все варианты между "плохо" и "очень плохо". Ибо, если нотация отвечает существу дела, то ее очень и прочесть самому, и вогнать в компьютер -- так, что и сам поймешь, компьютер ей не подавится, а будет доволен (см., например, как компьютер может кушать диаграммы TCP/IP в статье "Закон Мура для софта": http://www.moserware.com/2008/04/towards-moores-law-software-part-3-of-3.html, а заодно прочтите и первые две части по ссылкам в первой строке -- крайне полезно).

algebraic_brain указал на то, что можно попробовать использовать одну из нотаций теории категорий: моноидальные диаграммы (одним из частных случаев служат диаграммы Фейнмана). Фишка тут в том, что геометрия этой нотации следует алгебраической сути. А поскольку средний (да и не средний) человек хорошо размышляет геометрически -- крутит в голове разные пространственные фигурки -- но плохо размышляет алгебраически, то сложные письменные вычисления переходят в моноидальных диаграммах в разряд устных ("визуальных внутри головы") упражнений. Пользующиеся такими нотациями становятся гроссмейстерами в логических вычислениях, и начинают устно делать такие доказательства, которые раньше можно было делать только письменно со скрежетом зубовным. Вот пример: http://algebraic-brain.livejournal.com/94290.html (там даже трехмерные диаграммы, а не двумерные). Альтернатива моноидальным диаграммам -- использование сетей Петри (которые можно понимать как нотация для процесса доказательства для логических высказываний ISO 15926, хотя применимость этого подхода еще нужно отдельно обосновывать).

Пример расширения нотации Дирака для квантовомеханических расчетов, доступных детсадовцам (Kindergarten Quantum Mechanics -- http://arxiv.org/abs/quant-ph/0510032) и софта для этой нотации -- http://www.andyturner.info/research_oxford_msc.htm. algebraic_brain пишет: "Когда я показал, как проводить такие расчеты человеку, совершенно далекому от математики, он смог повторить сложнейший расчет, связанный с квантовыми группами. С первого раза, безошибочно, не понимая в квантовых группах ничего вообще". Ну да, даже школьник может сложить пятизначные числа столбиком, ничего не понимая в теории чисел!

Именно этот аппарат замкнутых моноидальных категорий (моноидальные диаграммы следуют этой теории -- в графическом языке: http://www.mscs.dal.ca/~selinger/papers.html#graphical) используется в работе Rosetta stone: физика,топология, логика и теория вычислимости - в одном флаконе, http://arxiv.org/abs/0903.0340 (я уже писал об этой работе в конце января 2010 -- http://ailev.livejournal.com/657139.html). algebraic_brain: "Типы языка Haskell, обычные множества, гильбертовы пространства, плетения и коборизмы, логические дедуктивные системы - это все примеры замкнутых моноидальных категорий. Многие расчеты с перечисленными системами можно делать, не вдаваясь в подробности (физика это или логика или что-то еще), а только лишь зная что это ЗМК".

Дальше у меня мысли пошли в сторону моего любимого текста (много лет я таскал листочек с его распечаткой у себя в портфеле) Accretion model of theory formation (кратенько пересказана в конце постинга http://ailev.livejournal.com/469995.html). Нужно время от времени находить новые формализмы (и непосредственно соответствующие им нотации), и перекодировать большие куски знания в эти формализмы. Иначе каюк, не будет хватать мощности головы (да и компьютера впридачу тоже не хватит).

ISO 15926 в качестве одного из своих формализмов указывает на теорию категорий. Это означает, что есть шанс попробовать и моноидальные диаграммы для записи (аккуратно скажем) в языке, эквивалентном части 2 или даже эквивалентном части 7.

Можно будет написать редактор, поддерживающий подобную моноидальную нотацию -- нотацию, которая поощряет логические (категориальные? категорные?) операции "в уме". Поскольку речь идет о "вычислениях" и "преобразованиях", то можно говорить об ISO 15926L -- языке программирования. Это близко к идее avlasov рассматривать ISO15926 как язык описания типов в языках программирования -- осталось добавить собственно языковую компоненту. Какова идея: иметь вынесенные в RDL общераспространненные промышленные(!) стандартные(!) типы, и программировать с их использованием в их же "родном" языке!

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

Текст этого постинга, конечно, сумбурный -- ровно настолько, насколько сумбурно состояние описываемой предметной области.
2019

Доказательство правильности систем

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

Одной из самых успешных работ в этом направлении был подход B, основанный на теории множеств. 1998 году была запрограммирована линия 14 метро METEOR (Париж). 86тыс. строк кода, до сих пор в версии 1.0, и до сих пор не замечено ошибок.

Но уже следующие линии метро (а применения этого подхода пошли главным образом по железнодорожной части, хотя хватало и других применений) показали, что ошибки таки бывают -- а успех первой реализации был связан с тем, что повышенное внимание уделялось системной инженерии (работе на уровне системы), а не ограничивались вознёй с целевой программой. После того, как это отследили, на рубеже столетия подход B был сознательно эскалирован на уровень системы: назван Event-B, в котором не только прямо говорилось не о софте, а о системе, но и "операции и методы" были заменены на "события". Обзор Event-B -- http://www.bmethod.com/pdf/grace-2010/event-b-overview.pdf

Сейчас Европа закачивает в данный подход деньги налогоплательщиков, получая разнообразный софт для B-моделирования и валидации получающихся моделей. Тут нужно заметить, что получатели этих денег главным образом во Франции.

Меня это все заинтересовало, поскольку появились работы, прямо адресующие разрыв между непонятностью формальных спецификаций и понятностью представления результатов неспециалистам:
-- ProB validation tool поддерживает множество языков спецификаций (B, Z, CSP, Event-B, Promela, dSL, ...) и позволяет делать анимации для того, чтобы эксперты, ничего не понимающие в спецификационных математических нотациях, могли понять то, что за этими нотациями скрывается (http://www.bmethod.com/pdf/grace-2010/pro-b-tokyo-2010.pdf).
-- controlled English для написания требований, из которых потом генерируются спецификации на B, а уж эти спецификации затем контролируются на целостность (http://doi.acm.org/10.1145/1734103.1734114)

Подробности можно копать отсюда:
-- свежайшие (март 2010) презентации в изобилии http://www.bmethod.com/php/conference-grace-2010-en.php
-- гнездо Event-B тут: http://www.event-b.org/ (и там изобилие ссылок)
-- ресурс по B методу компании ClearSy System Engineering: http://www.bmethod.com/ (и там еще ссылки на инструменты)

Еще мне интересна сама постановка задачи доказательства правильности систем по аналогии доказательства правильности программ. Похоже, что скоро нужно любой тезис из software engineering или computer science про программы как first class object переносить на системы. С другой стороны, B-моделирование забирается уже внутрь программы/системы. Поэтому можно ожидать, что скоро для системы будет переформулировано и знаменитое "программа = алгоритмы + данные". "Система = ???". И непонятно, что будет быстрее: самому придумать, как это будет в случае систем, или просто подождать годик-другой, пока другие придумают.