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

Question

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

Answer 1

.mmt 文件被 MMT 转换成几个 OMDoc 文件，管理三个维度:

内容
旁白
关系

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

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

relational 只存储诸如“这个档案声明这个理论”、“这个理论包含那个理论”或者“这个观点把这个理论作为域，那个理论作为辅域”这样的信息.当 MMT 想知道存在哪些内容（并且不需要所有详细信息）时，MMT 可以“快速”查看它。如果它不存在，MMT 将需要查找 content 文件中的所有查询，这会慢很多。关于 relational，同样 ref 什么都不做。

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

现在 ref <URI> 所做的是将引用的理论“包含”到当前文档中，这样它将被包含在 narration-OMDoc-file — 而没有 在 content 维度中复制它。上面链接的教程文件偶尔会出于教学目的这样做。

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

What does the `ref` keyword in MMT do?

keyword

mmt