Обсуждение

А что может дать ISO 15926 использование теории категорий? Т.е. что именно настолько выгоднее делать под нагрузкой соответствующего матаппарата. В предыдущем посте на эту тему я ответа не нашёл. Теоркат в своей традиционной форме настолько мета, что трудно найти что-либо менее сенсорно очевидное. И адаптаций (пока) не замечено. В то же время, наиболее эффективно работают те нотации и интерфейсы (во всех смыслах: человек-человек, человек-компьютер (GUI, CLI) и внутрипрограммные) которые ближе к базовому человеческому восприятию тела, пространства и времени.

offtopic: praxos.ru в последнее время отказывается работать ("Too many database connections")

Есть две теории, обе верные: -- разрабатываемые языки и их нотации должны быть как можно ближе к "фолк онтологии"; -- разрабатываемые языки и их нотации должны быть как можно более выразительны (тут можно пообсуждать слово "выразительны", обычно выделяется два значения: 1. в малом числе знаков много чего сказано и 2. необходимые операции проводятся легко). ISO 15926 пошел сразу по второму пути. Так, чтобы легче было выражать систему поставок продукции, там принята 4D модель времени, что критикуется очень многими людьми (которым, например, эти поставки продукции неинтересны, а интересны какие-то другие аспекты моделирования). Есть предположение, что моноидальные диаграммы могли бы быть полезными для изображения OIM из ISO 15926 (algebraic_brain может рассказать более подробно, поскольку это его мысль, которую я пока слабо понимаю). Кроме того, Matthew West в одной из презентаций будущее стандарта связывал с представлением его не только в виде EXPRESS, FOL или OWL, но и с использованием аппарата теории категорий. Но это другой аспект использования. Основная фишка в том, что моноидальные диаграммы позволяют алгебраическую/логическую сущность сетки понятий выразить геометрически так, что теоретически они будут эквивалентны. Это будет означать возможность геометрических преобразований таких, которые отвечают алгебраическим/логическим.

Эффект праздников. :) Сейчас починят.

>>Есть предположение, что моноидальные диаграммы могли бы быть полезными для изображения OIM из ISO 15926 (algebraic_brain может рассказать более подробно, поскольку это его мысль, которую я пока слабо понимаю) На самом деле, единственное мое преподложение по поводу применения моноидальных диаграмм относилось к пруф-ассистентам. Я пару раз говорил, что пока не вижу никакого прямого применения этой нотации к 15926, сети Петри там ближе. Сама теория категорий, безусловно, может быть применена в случае 15926, но не в целях построения моделера, а как альтернатива части 7 в целях проверки консистенстности. Например, если взять определения из части 7 вроде ENTITY A SUPERTYPE OF (X ANDOR ONEOF(Y, Z)) то это может быть переписано в виде A = (X + T)×(Y + Z + T), где "+" и "×"; - это, соответственно, категорные coproduct и product, а T - некоторый терминальный объект. Но это работа, честно говоря, скорее для тех, кто развивает стандарт. Что может действительно полезно здесь - это привитие теор-категорного мышления онтологам (и здесь моноидальные диаграммы действительно могут быть полезны, поскольку, пользуясь выражением justy_tylor, они действительно "сенсорно очевидны").

Смотрю я на эти формулы, в которых нужно вводить "некий терминальный объект" и много-много скобок, и все больше думаю про pointfree (http://www.haskell.org/haskellwiki/Pointfree) и concatenation languages (http://concatenative.org). И у меня ощущение, что в диаграммах как раз этот переход и делается: объекты эти там по факту есть, но для них не нужно придумывать специального имени. Ну, и скобок поменьше (ибо неявно присутствует стек). Ну, и я написал про интерес к теории категорий у тех, кто развивает стандарт -- они как раз и интересуются (хотя не слишком активно, как я понимаю: там никто в этом не разбирается).

"Терминальный объект" в распространенных системах типов обычно присутствует - это любой тип, который содержит всего лишь один инстанс (все такие типы должны быть изоморфны). По поводу конкатенативных: мне очень понравилось определение языка Joy как морфизма из синтаксического моноида в семантический. Кратко, красиво. Блеск.

Вот-вот, морфизмы: из синтаксического (форма) в семантический (содержание), это похоже на из геометрического (форма) в алгебру/логику (содержание). Я сейчас мимо всех этих теорий-определений иду, на чистой интуиции. Чего-чего, а интуиция у меня есть :) Я думаю, что можно было бы придумать concatenated language для ISO 15926 и его templates, и редактор сделать именно для него -- и работать с ним компиляторно/интерпретаторно, как с предусматривающим множество DSL базовым подъязыком системы типов. То есть взять не python, а Factor, и реализовать как DSL-15926-7 для DSL-15926-OIM. Должно получиться крайне красиво и компактно (особенно если учесть, что функциональные языки и логические все-таки родственники, а теория категорий к функциональным языкам тяготеет).

Что касается формулы A = (X + T)×(Y + Z + T) то ее можно воспринимать как обычную арифметическую, со сложением и умножением (только заменить надо T на единицу): A = (X + 1)×(Y + Z + 1) В частности, можно раскрывать скобки, и это будет иметь интуитивный смысл. A = X×Y + X×Z + X + Y + Z + 1 Т.е. сущность типа A может быть одновременно X и Y, одновременно X и Z, просто X, просто Y, просто Z. Единица в конце смущает, конечно, но это можно обработать.

Ваша идея мультипарадигмальности тоже очень четко ложится в теорию n-категорий. А именно, мы работаем с категорией Par парадигм и ищем удобные морфизмы из одной парадигмы в другую. Однако проблема в том, что часто такие морфизмы существуют лишь "с точностью до". Вот для того, чтобы выразить это "с точностью до" и вводятся n-категории. Даже я скажу так, наиболее интересные связи между парадигмами будут найдены лишь если воспринимать Par как 2-категорию (т.е. не менее чем 2). Иными словами, нужны будут преобразования между преобразованиями.

По повод Factor - надо посмотреть, подумать. В конце концов, я рассматриваю python лишь как "что-то, от чего можно отталкиваться", а не как окончательное решение.

Ну, у меня мысль про мультипарадигмальность как раз в другую сторону: я считаю, что удобных морфизмов из одной парадигмы в другую нет, и поэтому нужно использовать все парадигмы "винегретом", каждую для того, что она умеет делать лучше всего. То есть нельзя ограничиваться либо только логическим представлением (к чему постоянно призывает avlasov) или функциональным представлением (типа Haskell), а идти дальше -- Curry, или Factor, плюс идеи из проекта STEP (главная тамошняя идея -- иметь "детальки компилятора-интерпретатора изо всего во всё" и "детальки браузера-редактора всего", а дальше нужно только определить, что это за детальки). Так что я не про преобразования между преобразования. С другой стороны, ваши слова можно проинтерпретировать и так, что вы описываете как раз уровень ниже: там "сто цветов разных парадигм" попадают на вход "ста компиляторов" и уже в них каким-то (ленивым!) способом преобразуются в машинный язык, который по определению монопарадигмален. Так что ваша переформулировка, похоже, как раз для описания такой мегамодели ( терминах AtlanMod), или цепочки смыслов (в терминах Ian Piumarta) или набора морфизмов между разными представлениями в ваших терминах теории категорий, или уж не помню, что там у суперкомпиляторщиков на эту тему -- у них тоже достаточно развитый язык для описания длинных цепочек преобразований при компилировании/суперкомпилировании/оценке/исполнении.

Задача в том, чтобы это выразить в минимальном числе знаков текста и без введения каких-то дополнительных T или 1. Но не уверен, что прямо сейчас нужно бросаться решать эту задачу...

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

То, что Вы описали во втором абзаце - это тоже способ построения категории. Только морфизмом будет не прямое преобразование из А в В, а преобразование обоих А и В в некоторое С. Причем такая категория сразу же, без промедлений, будет 2-категорией (о чем я и предупреждал). :)

Я написал сразу же "не в целях построения моделера, а как альтернатива части 7 в целях проверки консистенстности". Те обсуждения по поводу ТК, которые Вы мне присылали, скорее в этом направлении идут. Это удобный математический способ проверки консистентности (и основное предназначение части 7 именно в этом).

Мне более подходящим кажется не разделение, а оценивающий подход. Есть случаи, когда выгоднее заплатить не-интуитивностью за новую степень абстракции, просто следует понимать цену. И как её можно снизить. Моделирование мыслительных процессов математиков (из http://ailev.livejournal.com/831024.html) очень привлекательно в этом ключе, прям зацепился. Про графическую нотацию понятно. Можно использовать даже несколько нотаций/view, совпадающих по геометрии, но с разными символами, в зависимости от цели применения.

Ну и начните проект моделирования на базе openmeta и тамошних людей (я вот никак не соберусь туда об этом постинг сделать, а ведь давно в плане!). Математиков и модельеров ведь там, по идее, хватает...

Я занимаюсь таким в отношении программистов и их языков. И, хотя в этом случае в качестве одного из источников информации используется самонаблюдение, ресурсов тратится много. Даже самим программированием, архитектурой и ведением проектов последнее время занимался только ради денег. Но сейчас сделал творческий отпуск. Можно что-то из этого вывести на рассмотрение в openmeta.

Так вынесите в openmeta, как минимум получите обратную связь (отсутствие каковой тоже будет обратной связью ;)