Взгляд между теориями, включая общую теорию в ММТ

У меня есть две теории B и C, каждая из которых включает общую теорию A. Моя цель — указать представление BC: B → C удобным способом, без предоставления отображений для всех констант в A.

fixmeta ur:?LF ❚

theory A =
    a : type ❙
❚

theory B =
    include ?A ❙
    b : type ❙
❚

theory C =
    include ?A ❙
    c : type ❙
❚

view BC : ?B → ?C =
    // do I need to map all constants of A here? ❙
    b = c ❙
❚

В настоящее время БК не тотальный, т.е. константа a из A не имеет отображения.

Я хотел бы не заботиться об A при определении BC и просто сопоставлять каждую константу в A из B с идентичной константой в A из C.

Это возможно? Существует ли какой-то вид идентичности от A до A, который можно просто включить в BC?


syntax mmt
person mctinn    schedule 26.10.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Решение.

view BC : ?B → ?C =
    include ?A ❙
    b = c ❙
❚

Объяснение. Синтаксис include ?A ❙ в ваших теориях B и C, кроме всего прочего, также действует как обычное объявление точно так же, как объявления констант являются объявлениями. Чтобы представления были действительными, все неопределенные объявления теории предметной области должны быть сопоставлены с чем-то. В частности, объявления включения должны быть сопоставлены с морфизмами, которые описывают действие морфизма, которое должно быть унаследовано и применено к включенной части домена.

Следовательно, вы можете добиться отображения всех объявлений в A на себя, отобразив include ?A на морфизм тождества на A, который точно представляет желаемое отображение. В поверхностном синтаксисе MMT это может быть достигнуто с помощью include ?A ❘ = IDENTITY ?A или, что то же самое, с помощью синтаксического сахара include ?A.

В общем, если у вас есть представление v: B → C, а B включает A, то v должен отображать include ?A в морфизм A → C. Выше мы сопоставили его с морфизмом A → A (а именно тождеством), который также является морфизмом вида A → C, поскольку А содержится в С.

См. вторую ссылку ниже о склеивании включений в структуры для примера, где назначенный морфизм не тождественен.

Дополнительные ссылки.

person ComFreek    schedule 26.10.2020