理论之间的观点都包括MMT中的通用理论

如何解决理论之间的观点都包括MMT中的通用理论

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

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映射）。

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

解决方法

解决方案。

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中。

有关以下示例的第二个参考：胶合结构中的夹杂物，其中分配的形态是不是身份的示例。

更多参考。