Как склеить/выявить включения в двух структурах в ММТ?

Я хочу формализовать формальные языки и их семантику в MMT и определить общее понятие семантики. эквивалентность двух семантик относительно. один синтаксис. Именно кодирование последнего оказывается идентификацией/склеиванием, что я понятия не имею, как это сделать в ММТ. Далее позвольте мне подробнее остановиться на моей конкретной настройке формализации.

Ниже приведена упрощенная формализация, показывающая мой подход. Основываясь на теории Meta, объединяющей как логическую структуру LF, так и некоторую логику, я начинаю с Syntax определения общего понятия выражений и типизации. Затем в Semantics я определяю сверху семантику, здесь для простоты только дедуктивную семантику, т.е. отношение выводимости.

theory Meta : http://cds.omdoc.org/urtheories?LF=  
  // some logic giving us a type `prop` of propositions,
  // a notion of derivability ⊦, biimplication ⇔ etc. ❙
  include ?Logic ❙
❙

theory Syntax : ?Meta =
  // type for expressions ❙
  expr: type ❙

  // a typing relation
  typing_rel: expr ⟶ expr ⟶ prop ❙

  // ... ❙
❚

theory Semantics : ?Meta=
  include ?Syntax ❙

  // a deductive semantics: "derivable e" says e is a theorem ❙
  derivable: expr ⟶ prop ❙
❚

Учитывая это, я хочу определить эквивалентность двух таких семантик относительно. к одному синтаксису. Кодировать первую часть легко, см. ниже; но у меня возникли проблемы с кодировкой последнего требования.

theory SemanticsEquivalence : ?Meta =
  structure syn : ?Syntax ❚

  // how can I force sem1|?Syntax = sem2|?Syntax = syn ❙
  structure sem1 : ?Semantics = ❚
  structure sem2 : ?Semantics = ❚

  is_equivalent: {e: syn/expr} ⊦ (sem1/derivable e) ⇔ (sem2/derivable e) ❙
❚

Как склеить/обозначить включения Syntax как в sem1, так и в sem2?


dependent-type theorem-proving formal-methods mmt
person ComFreek    schedule 27.07.2020    source источник
comment
мета-примечание: MMT — это формальная система, разработанная в исследовательская группа kwarc. Мы изучаем, можем ли мы использовать StackOverflow для вопросов по этому поводу, отсюда и тег mmt.   -  person ComFreek    schedule 27.07.2020

Ответы (1)


arrow_upward
2
arrow_downward

Решение

Используйте определенные включения в структурах:

theory SemanticsEquivalence : ?Meta =
  structure syn : ?Syntax = ❚
    
  structure sem1 : ?Semantics =
    include ?Syntax ❘ = ?SemanticsEquivalence?syn ❙
  ❚
  structure sem2 : ?Semantics =
    include ?Syntax ❘ = ?SemanticsEquivalence?syn ❙
  ❚

  is_equivalent: {e: syn/expr} ⊦ (sem1/derivable e) ⇔ (sem2/derivable e) ❙
❚

Объяснение

Теория того, почему это работает, гораздо глубже, чем можно предположить из приведенного выше кода. Это требует понимания трех аспектов, подробно описанных ниже. Я собрал эту информацию из официальных документов MMT по неявным морфизмам, структурам и включениям и из личного общения с @Dennis Müller.

  1. Структуры индуцируют морфизмы теории

    Например, structure syn : ?Syntax = ❚ в теории SemanticsEquivalence имеет два эффекта: во-первых, он копирует каждое объявление Syntax?d в объявление SemanticsEquivalence?syn/d, где syn/d — просто сложное имя копии. Во-вторых, структура также индуцирует морфизм теории Syntax -> SemanticsEquivalence, который отображает каждое объявление Syntax?d в копию SemanticsEquivalence?syn/d.

    Такое поведение структур может показаться здесь несколько упрощенным, но это только потому, что структура syn имеет пустое тело. Если бы вместо этого

    theory SemanticsEquivalence : ?Meta =
  otherExpr: type ❙
  structure syn : ?Syntax =
    expr = otherExpr ❙
  ❚
❚

    тогда морфизм индуцированной теории содержал бы отображения Syntax?expr := SemanticsEquivalence?otherExpr, Syntax?typing_rel := SemanticsEquivalence?syn/typing_rel, т.е. копировалось только Syntax?typing_rel.

  2. Включения также индуцируют теоретические морфизмы

    Например, с theory Semantics = include ?Syntax ❙ ... ❚ включение Syntax в Semantics имеет тот же эффект, что и структуры с пустым телом: каждое объявление Syntax?d доступно в Semantics по одному и тому же URI (таким образом, в некотором смысле копия), и существует индуцированный морфизм — неявный. четный — Syntax -> Semantics, который сопоставляет каждое объявление с идентификатором: Syntax?d := Syntax?d.

  3. Включения, как и объявления, также могут иметь определение

    Рассмотрим это на примере. Предположим, у нас есть морфизм m: Syntax -> Semantics', где theory Semantics' = include ?Syntax ❘ = m ❙ ... ❚. Теперь включение Syntax больше не индуцирует тривиальный тождественный морфизм, а вместо этого принимает m. Например, если в части ... упоминается объявление Syntax?d, на самом деле берется m(Syntax?d).

    Давайте смешаем это понимание с предыдущими. Рассмотрим следующий код:

    theory SemanticsEquivalence : ?Meta =
  structure syn : ?Syntax = ❚

  structure sem1 : ?Semantics =
    include ?Syntax ❘ = ?SemanticsEquivalence?syn
  ❚

  // other structure... ❙
❚

    На первый взгляд, syn индуцирует морфизм Syntax -> SemanticsEquivalence, доступный через ?SemanticsEquivalence?syn. Более того, из первого и второго выводов мы знаем, что включение Syntax в структуру — это особый вид морфизма, а именно Syntax -> SemanticsEquivalence — обратите внимание на кодовый домен! Наконец, благодаря третьему выводу мы можем определить это включение с помощью подходящего морфизма, а именно с помощью ?SemanticsEquivalence?syn. И это обеспечивает именно то склеивание, которое мы хотели.

person ComFreek    schedule 27.07.2020