dependent-type - 如何在 MMT 中粘合/识别两种结构中的夹杂物？

Question

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

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

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 ?

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 汇总了这些信息以及与 @Dennis Müller 的个人交流.

结构诱导理论态射
例如，structure syn : ?Syntax = ❚内论SemanticsEquivalence有两个作用:第一，它复制每个声明 Syntax?d声明 SemanticsEquivalence?syn/d哪里syn/d只是副本的“复杂”名称。其次，该结构还引入了一个理论态射Syntax -> SemanticsEquivalence映射每个声明 Syntax?d到副本 SemanticsEquivalence?syn/d .
结构的这种行为在这里可能看起来有点简单，但这只是因为结构 syn有一个空的 body 。如果你有

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 ❙ ... ❚包含 Syntax内Semantics具有与空体结构类似的效果:每个声明 Syntax?d可在 Semantics 内访问在相同的 URI 下(因此在某种意义上是一个副本)，并且存在诱导态射——甚至是隐式的——Syntax -> Semantics映射每个声明身份-like:Syntax?d := Syntax?d .

包含，作为声明，也可能有一个定义
让我们通过一个例子来考虑这一点。考虑我们有一个态射 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 .这恰好实现了我们想要的粘合。