Введение
Я пишу докторскую диссертацию по абстрактному дельта-моделированию (ADM), абстрактному алгебраическому описанию модификаций (известных как дельты ), способных воздействовать на продукты (как в «программных продуктах»). Это может быть использовано для организации набора связанных продуктов («линейка продуктов») в виде простого основного продукта и набора условно примененных дельт, и, таким образом, для более широкого повторного использования лежащих в основе артефактов.
Детали дельта-моделирования не очень важны для моего вопроса, но ADM служит хорошим примером для объяснения проблемы, поэтому я представлю наиболее важные концепции.
Фон
Основная интересная структура - дельтовидная мышца . Продукты приходят из универсального набора . Дельты происходят из моноиде с оператором композиции и нейтральный элемент . Оператор семантической оценки преобразует «синтаксическую» дельту в отношениекоторый решает , как может модифицировать продукт.
Вопрос
Поскольку ADM является абстрактной алгеброй, большая часть моей работы абстрагируется от конкретной природы продуктов и дельт, и ряд результатов доказывается без спуска на более конкретный уровень. Ожидается, что эти результаты будут перенесены в более конкретную область, но я еще не формализовал это.
Существуют примеры и тематические исследования, которые работают в конкретной области: объектно-ориентированный исходный код, код, натуральные числа, профили мобильных телефонов и т. д. Есть также несколько промежуточных этапов абстракции, таких как вложенные пары ключ-значение. Для каждого я переопределяю (или уточняю),
Я хотел бы сделать эту иерархию явной: (1) для большей ясности для читателя и (2) для формального обоснования использования результатов с более абстрактных уровней.
Мой вопрос: как мне формально организовать эти уровни абстракции?
Я надеюсь, что смогу рассуждать с простым уточнением отношения на дельтовидных мышцах. И я чувствую, что это можно определить, просто обратившись к подмножеству а также , Но я еще не уверен. Существуют ли подходы к проблеме, которую я описываю? Публикации, которые я должен прочитать?
Дельтовидная иерархия
Чтобы дать вам лучшее представление о том, что я имею в виду, вот иерархия дельтовидной абстракции, которую я имею в виду:
- Аннотация Дельтовидная оболочка : это основная дельтовидная оболочка, в которой продукты и дельты могут быть чем угодно. Большая часть теории основана на этом, и большинство результатов доказано на этом уровне.
- Реляционная дельтовидная мышца : здесь дельты - это отношения а также это тождественная функция.
- Функциональный дельтоид : здесь дельты являются функциональными (или «детерминированными»).
- Дельтовидная система с натуральным числом : Это самый простой конкретный дельтовидный отросток, созданный просто для иллюстрации уточнения дельтовидной мышцы. Здесь продукты натуральные числа и дельты простые числовые последовательности, представляющие полиномиальные операции.
- Вложенная пара ключ-значение Deltoid : промежуточный уровень абстракции для любой иерархии, в которой ключи отображаются на значения или вложенные иерархии. Deltas может выполнять модификации в этом «дереве» на любой глубине.
- ООП Deltoid : для абстрактных представлений объектно-ориентированных программ. Они в основном являются вложенными парами ключ-значение, потому что программы отображают имена модулей в наборы классов, которые отображают имена классов в наборы методов, которые отображают имена методов в реализации методов.
- ABS Deltoid : ABS - это реальный объектно-ориентированный язык программирования.
- Профиль телефона Deltoid : здесь продукт представляет собой плоскую привязку настроек (таких как громкость, яркость экрана и т. Д.) К значениям из соответствующего домена.
- ООП Deltoid : для абстрактных представлений объектно-ориентированных программ. Они в основном являются вложенными парами ключ-значение, потому что программы отображают имена модулей в наборы классов, которые отображают имена классов в наборы методов, которые отображают имена методов в реализации методов.
- Deltoid : продукты документы и дельты изменяют их, переопределяя макросы.
- Реляционная дельтовидная мышца : здесь дельты - это отношения а также это тождественная функция.
Ну, это должно дать вам четкое представление о том, что я имею в виду. Обратите внимание, кстати, что для любого дельтовидной мышцы, является моноидным гомоморфизмом из к принадлежность к соответствующему реляционной дельтовидной мышцы.
The actual hierarchy may be larger. It may also be differently organized, based on what kind of refinement theory I'll use. For example, if I go for a simple subset-relation on а также ABS Deltoid не подходит под Deltoid с вложенной парой ключ-значение, поскольку его продукты и дельты на самом деле представляют собой простой текст (исходный код). Но приведенная иерархия все еще может работать, если я использую гомоморфизмы.
источник
Ответы:
Я полагаю, что вам было бы полезно взглянуть на теорию абстрактной интерпретации, которая дает очень подробные ответы на похожие вопросы в несколько иной области анализа программ на основе решеток.
Мне кажется, что вы используете каркас, основанный на алгебрах. Я использую здесь слово алгебра в смысле универсальной алгебры, где я предполагаю, что ограничения на структуру алгебры задаются равенством между членами. Есть два разных смысла, в которых абстракции (или иерархии) входят в картину.
Эти два понятия тесно связаны, но различны.
Абстракция между двумя структурами
Понимание абстрактной интерпретации заключается в том, что полезно придавать структурам, которые вы рассматриваете, понятие порядка. Рассмотрим две структуры
Гомоморфизм в смысле универсальной алгебры будет выглядеть примерно так:
Мы можем рассматривать две структуры, представленные выше, как предварительно упорядоченные структуры
и гомоморфизм мы можем переписать, чтобы быть функцией, удовлетворяющей
Теперь предположим, что у вас есть другое доступное понятие аппроксимации, которое имеет смысл. Например, когда мы имеем дело с наборами состояний при верификации программы, включение подмножества имеет смысл для определенного приложения, или когда речь идет о формулах в автоматическом удержании, смысл имеет смысл. В целом, мы можем рассмотреть
Теперь вместо гомоморфизма мы можем иметь функцию абстракции
Функция абстракции делает явной идею о том, что если структураN это абстракция структуры над M затем оценивая термин в N не может дать более точные результаты (в отношении понятия приближения в N ), чем оценка того же термина в M а затем сопоставить его с N ,
Теперь мы можем спросить, нужно ли подходить к проблеме с точки зрения абстракции, а не уточнения. Смысл, мы не можем сказать, чтоM это уточнение N и сформулировать условия в терминах. Это именно то, что делает функция конкретизации .
Условия абстракции и конкретизации называются условиями устойчивости в абстрактной интерпретации. В особом случае этоα а также γ образуют связь Галуа, условия абстракции и конкретизации эквивалентны. В общем, они не эквивалентны.
Все, что мы сделали до сих пор, только формализует понятие абстракции между парой структур. То, что я сказал, можно изложить гораздо более кратко на языке теории категорий. Я избегал категорий из-за вашего комментария выше.
Абстракция Иерархии
Предположим, у нас есть структураM наделены предзаказом и некоторыми операциями. Мы можем рассмотреть все структурыN такой, что N это абстракция M в смысле выше. Если у нас есть этоN1 это абстракция N2 и оба являются абстракциями M У нас есть три элемента иерархии. Отношение «является абстракцией» позволяет нам определять предварительный порядок между структурами. Давайте назовем семейство структур, упорядоченных по абстракции, иерархией .
Если я рассмотрю ваш пример, похоже, что ваш абстрактный дельтоид может быть кандидатом на максимальный элемент в некоторой иерархии. Я не совсем уверен, потому что абстрактный дельтовидный отросток, по-видимому, является семейством дельтовидных отростков, а не конкретным дельтовидным отростком.
Теперь вы можете рассмотреть различные иерархии. Иерархия всех дельтовидных мышц. Под-иерархия, основанная на различных соображениях, которые у вас есть выше. Конкретным примером в контексте абстрактной интерпретации является иерархия полных решеток, которые находятся в связи Галуа с данной решеткой powerset, и субиерархии, состоящие только из дистрибутивных или только булевых решеток.
Как отмечает Мартин Бергер в комментариях, это понятие абстракции между иерархиями охватывается понятием соединений между категориями.
Категориальная перспектива
Был комментарий, запрашивающий дополнительные комментарии по категориям. Этого комментария больше нет, но я все равно отвечу.
Давайте сделаем шаг назад и посмотрим, что вы делаете при разработке дельтовидных мышц и что я описал выше, с более общей точки зрения. Мы заинтересованы в понимании существенной структуры сущностей, которыми мы манипулируем в контексте программного обеспечения, и отношений между этими сущностями.
Первое важное понимание состоит в том, что нас интересует не только набор элементов, но и операции, которые мы можем выполнять над этими элементами, и свойства этих операций. Эта интуиция определяет дизайн классов в объектно-ориентированном программировании и определение алгебраических структур. Вы уже сделали эту интуицию явной в определении дельтовидной мышцы, которая определила несколько интересных операций. В более общем смысле, это мыслительный процесс, лежащий в основе алгебраических описаний. Нам нужно определить, какие у нас операции и какими свойствами они обладают. Этот шаг говорит нам о структуре типов, с которой мы работаем.
Вторая реализация заключается в том, что нас интересует не только набор элементов, но и отношения абстракции. Самая простая формализация абстракции, которую я могу себе представить, - рассмотреть предварительно упорядоченное множество. Мы можем думать о предварительно упорядоченном множестве как о строгом обобщении множества о чем-то, что сопровождается понятием аппроксимации.
В идеале мы хотим работать в обстановке, в которой обе идеи являются первоклассными гражданами. Это означает, что нам нужна типизированная настройка, подобная настройке алгебры, а также настройка предзаказа, учитывающая приближение. Первым шагом в этом направлении является рассмотрение решетки. Решетка является концептуально интересной структурой, потому что мы можем определить ее двумя эквивалентными способами.
Решетка, таким образом, представляет собой математическую структуру, к которой можно подходить с точки зрения алгебры или аппроксимации. Недостатком здесь является то, что сами элементы решетки не обладают структурой типа, которая учитывается в приближении аппроксимации. То есть мы не можем сравнивать элементы, основываясь на понятии наличия более или менее структуры.
В контексте вашей проблемы вы можете рассматривать категории как естественное обобщение предзаказов, которые охватывают как понятие аппроксимации (в морфизмах), так и структуру типов в алгебраической среде. Настройка теории категорий позволяет нам обойтись без различных ненужных различий и сосредоточиться на структуре сущностей, которые вас интересуют, и приближении этой структуры. Универсальные свойства и присоединения дают вам очень мощный словарь и инструменты для понимания ландшафта структур, которые вас интересуют, и позволяют строго математически трактовать даже интуитивные понятия, такие как различные уровни абстракции.
Что касается моего комментария об абстрактных дельтоидах, то, похоже, вам нужна категория. Абстрактный дельтоид - это особая категория, аналогичная категории множеств. Есть другие категории, которые вы рассматриваете. Сначала я думал, что вы определяете дельтовидную мышцу, которая в смысле теории категорий будет конечным (или конечным) объектом.
Вы изучаете вопросы, на которые теория категорий дает очень удовлетворительные ответы. Я надеюсь, что вы сможете прийти к такому выводу самостоятельно.
Ссылки
источник
Вы работаете над своей докторской степенью. Говоря "Я не очень хорошо разбираюсь вX «Это не оправдание. И если вы хорошо, то сказать« мой советник не знает X «Это не оправдание.
Вы используете моноиды, где вы должны использовать категории. Ваши моноидальные операции предполагают, что вы можете комбинировать любыеδ вместе Но имеет ли это смысл, например, как бы вы сочинили «добавить пластиковый корпус» и «добавить металлический корпус»? Я полагаю, некоторые из вашихδ приводит к пустым отношениям, потому что они не имеют смысла. Вы должны с подозрением относиться к такого рода вещам.
Как заинтересованному наблюдателю кажется, что моноид должен быть категорией, поэтому мы можем составить дваδ только если им есть смысл составлять. Тогда ваша семантическая оценка - это просто функтор в категорию множеств и отношений. И тогда вы увидите, что есть много других категорий, которые вы можете использовать. Функциональные дельты будут соответствовать функтору, который отображается в категорию множеств и функций, дельтоид из натуральных чисел является функтором в моноид полиномов от натуральных чисел (рассматривается как категория) и т. Д.
Я не уверен, что вы хотите слишком серьезно формализовать мобильные телефоны LaTeX и Nokia в общей теории. Но, конечно, ваша теория должна быть применима к таким примерам (только не зацикливайтесь, когда обнаруживаете, что мобильные телефоны на самом деле не имеют четко определенной семантики).
Вы действительно обманываете себя, настаивая на предопределенной технологии (вашим консультантом?), Судя по всему.
источник