我如何 glue/identify 包含在 MMT 的两个结构中？

Question

我想在 MMT 中形式化形式语言及其语义，并定义两个语义的 语义等价 的一般概念。一个语法。准确地说，编码后者是一个 identification/glueing，我不知道如何在 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 ❙
❚

鉴于此，我想定义两个这种语义的等价性。到 one 语法。编码第一部分很容易，见下文；但我在编码后一个要求时遇到了问题。

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) ❙
❚

如何 glue/identify Syntax 包含在 sem1 和 sem2 中？

Answer 1

解决方案

在结构中使用定义的内含物：

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) ❙
❚

说明

为什么这有效的理论比上面的代码可能暗示的要深刻得多。这需要理解下面阐述的三个方面。我从 official MMT docs on implicit morphisms, structures, and includes and from personal communication with @Dennis Müller.

汇总了这些信息

结构引发理论态射

例如，理论 SemanticsEquivalence 中的 structure syn : ?Syntax = ❚ 有两个作用：首先，它将每个声明 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 被复制。
包含也引起理论态射

例如，对于 theory Semantics = include ?Syntax ❙ ... ❚，在 Semantics 中包含 Syntax 与具有空主体的结构具有相似的效果：每个声明 Syntax?d 都可以在 [=27 中访问=] 在相同的 URI 下（因此在某种意义上是一个副本），并且有一个诱导的态射 - 一个隐式的甚至 - Syntax -> Semantics 映射每个声明恒等：Syntax?d := Syntax?d.
包含，作为声明，也可以有定义

让我们通过一个例子来考虑这个问题。考虑我们有一个态射 m: Syntax -> Semantics' where 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。这正是我们想要的粘合。

我如何 glue/identify 包含在 MMT 的两个结构中？

How can I glue/identify inclusions in two structures in MMT?

dependent-type

theorem-proving

formal-methods

mmt

解决方案

说明