Выразительность, теория категорий, моноидальные диаграммы, 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 общераспространненные промышленные(!) стандартные(!) типы, и программировать с их использованием в их же "родном" языке!
Пока же зафиксируем: с формализмами и нотациями пока все плохо. Моделеориентированность, семантические упражнения крайне трудны, и пока не заметно специальной работы по облегчению участи человека, который хочет эти формальные методы использовать.
Текст этого постинга, конечно, сумбурный -- ровно настолько, насколько сумбурно состояние описываемой предметной области.
Поскольку мы тут пытаемся думать об "универсальном моделере", то становится интересной "универсальная нотация" (и, конечно, нотационная инженерия -- вспомним только одну из ее школ: 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 общераспространненные промышленные(!) стандартные(!) типы, и программировать с их использованием в их же "родном" языке!
Пока же зафиксируем: с формализмами и нотациями пока все плохо. Моделеориентированность, семантические упражнения крайне трудны, и пока не заметно специальной работы по облегчению участи человека, который хочет эти формальные методы использовать.
Текст этого постинга, конечно, сумбурный -- ровно настолько, насколько сумбурно состояние описываемой предметной области.