问题描述
我有两个理论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中。
有关以下示例的第二个参考:胶合结构中的夹杂物,其中分配的形态是不是身份的示例。
更多参考。