时间戳

首页 > 解决方案 > MMT 中的 `ref` 关键字有什么作用？

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

问题描述

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

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

标签： keywordmmt

解决方案

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

  • 内容
  • 旁白
  • 关系

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

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

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

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

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

推荐阅读