两种理论之间的观点，包括 MMT 中的共同理论

Question

我有两个理论 B 和 C，都包括一个共同的理论 A。我的目标是以一种方便的方式指定一个视图 BC: B → C，而无需为所有对象提供映射A.

中的常量

fixmeta ur:?LF ❚

theory A =
    a : type ❙
❚

theory B =
    include ?A ❙
    b : type ❙
❚

theory C =
    include ?A ❙
    c : type ❙
❚

view BC : ?B → ?C =
    // do I need to map all constants of A here? ❙
    b = c ❙
❚

目前，BC 不是总计，例如来自 A 的常量 a 没有映射。

我想在定义 BC 时不必关心 A，只需将 A 中的每个常量从 B 映射到 A 中从 C 的相同常量。

这可能吗？是否存在某种可以包含在 BC 中的从 A 到 A 的身份视图？

Answer 1

解决方案。

view BC : ?B → ?C =
    include ?A ❙
    b = c ❙
❚

解释。你的理论B和C中的语法include ?A ❙，除此之外，还充当普通声明，就像常量声明是声明一样.为了使视图有效，领域理论的所有未定义声明都需要映射到某物。特别是，include 声明需要映射到态射，它描述了为域的包含部分继承和应用的态射动作。

因此，您可以通过将 include ?A 映射到 A 上的恒等态射来实现将 A 中的所有声明映射到它们自身，这恰好表示了所需的映射。在 MMT 表面句法中，这可以通过 include ?A ❘ = IDENTITY ?A 或等效地通过语法糖 include ?A.

来实现

一般来说，如果你有一个视图 v: B → C 并且 B 包含 A，那么 v 必须映射 include ?A 到态射 A → C。上面，我们将它映射到一个态射 A → A（即恒等式），它也是一个形式为 A → C 的态射，因为 A 包含在 C.

中

请参阅下面关于在结构中粘合包含的第二个参考，其中分配的态射是不是恒等式的示例。

进一步参考。

Official documentation on includes and implicit morphisms

两种理论之间的观点，包括 MMT 中的共同理论

View between theories both including a common theory in MMT

syntax

mmt