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

编程问答 2022-06-09

问题描述

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

解决方法

MTP将

.mmt文件转换为多个OMDoc文件，从而控制三个尺寸：

  • 内容
  • 旁白
  • 关系

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

内容包含诸如“该理论包含此常数，具有这种类型和定义”的信息，等等。对于 content ，ref确实一点都没有。

关系仅存储诸如“此档案库声明了该理论”，“该理论包括该理论”或“该视图以该理论为域而该理论为共域”之类的信息。 MMT可以在想要知道存在什么内容（并且不需要所有详细信息）时“快速”查看它。如果不存在，则MMT需要在 content 文件中查找所有查询，这会慢很多。关于关系，ref再也不执行任何操作。

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

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

keywordmmt