MMT 中的 `ref` 关键字有什么作用？答案

【问题标题】：What does the `ref` keyword in MMT do?MMT 中的 `ref` 关键字有什么作用？
【发布时间】：2020-10-11 23:48:18
【问题描述】：

MMT 中的ref 关键字有什么作用？我在MMT/LATIN2 archive in modal.mmt遇到它：

ref latin:/?DisjunctionHilbert2ND❚
ref latin:/?NegationHilbert2ND❚
ref latin:/?ImplicationHilbert2ND❚
ref latin:/?EquivalenceHilbert2ND❚

theory KripkeFrame : latin:/?TypedLogic =
  include ?Worlds❙
  accessible : tm W ⟶ tm W ⟶ prop❘ # 1 acc 2 prec 30❙
❚

【问题讨论】：

标签： keyword mmt

【解决方案1】：

.mmt 文件通过 MMT 转换为多个 OMDoc 文件，管理三个维度：

内容
旁白
关系

查看任何 MMT 存档中的相应文件夹。

content 包含诸如“这个理论包含这个常量，它有这个类型和这个定义”等信息。关于 content，ref 什么都不做全部。

relational 仅存储诸如“此档案声明此理论”、“此理论包含该理论”或“此视图将此理论作为域而该理论作为共域”之类的信息。当 MMT 想知道存在哪些内容（并且不需要所有细节）时，它可以“快速”地查看它。如果它不存在，MMT 将需要在 content 文件中查找所有查询，这会慢很多。关于关系，ref 什么都不做。

最后，还有旁白，其中包含在哪个 .mmt 文件中声明内容的方式（以及内容）。通常，每个 .mmt 文件只生成一个 narration-OMDoc 文件和几个 content-OMDoc 文件（每个理论一个）。 narration-OMDoc 还包含语义 cmets（以/t 开头）、分段以及声明理论的精确顺序等内容。 Narration-OMDoc 文件可以是例如在 MMT 服务器或 MathHub 上进行检查，它们类似于“活动文档”——一个很好的例子是：https://mmt.mathhub.info/?http://docs.omdoc.org/examples/tutorial/0-Tutorial.omdoc（注意所有的 cmets 和解释）

现在ref <URI> 所做的是将引用的理论“包含”到当前文档中，以便将其包含在 narration-OMDoc 文件中 - 而不将其复制到内容维度。上面链接的教程文件偶尔会出于教学目的这样做。

【讨论】：