![](https://csdnimg.cn/release/download_crawler_static/88627038/bg5.jpg)
J.
动力
MTanaka/Electronic Notes in Theoretical Computer Science 225
(
2009
)
281
通过系统地使用这种观察和丰富范畴理论[11],我们可以通过值语言来建模调
用,例如计算λ演算[22],扩展[3,1]以及其一阶片段的扩展,例如用于在[32,30]
中建模延拓。我们将系统地展示如何对这些语言进行建模,然后最终展示如何将这
种分析扩展到模型数据细化。
3
建模上下文
我们对值调用语言和数据细化建模的核心是上下文建模。在给出数据精化的公理化
解释时,我们希望数据精化尊重上下文,而不要求尊重任何其他结构。因此,我们
需要特别注意建模上下文。这对于按值调用的语言来说是微妙的,需要Freyd-范畴
的概念[30]。所以在这一节中,我们发展
Freyd
-范畴的机器
我们必须首先回忆premonoidal范畴和严格premonoidal函子的定义,以及它
们的对称性,如在[28]中介绍并在[1,26,32,30]中进一步premonoidal范畴
是monoidal范畴概念的推广:它本质上是monoidal范畴,除了张量只需要是两
个变量的函子而不一定是双函子,即,给定映射
f
:
X X
J
和
g
:
Y Y
J
,
从X得
到的两个明显的映射 Y到X
J
你
可能 会说。
给定一个对称幺半群范畴C,如Set,和C的一个对象S,我们可以考虑具有与C相
同的对象和D(X
,
X
J
)=C(S X
,
S X
J
)的范畴D,其复合由C的复合诱导。 这种
结构可 [22]这是一个很好的例子。范畴
D
不具有有限积或monoidal结构,如通常用
于建模上下文,问题在于,尽管有明显的函子
X
和
对于
任意对象X和Y,它们不产生双函子。因此,我们需要一种精确的方式
来阐明D结构的具体内容,从而能够解释其中的语境。
定义3.1一个
二型范畴
是一个范畴
K
,对于
K
的每个对象
X
,函子
h
X
:
K
−→
K
和
k
X
:
K
−→
K
使得对于
K
的每个对象对(
X
,
Y
),
h
X
Y
=
k
Y
X
。关节值表示
为
X
Y
。
定义
3.2
Binoidal范畴
K
中的箭头
f
:
X
−→
X
J
是
中心的,
如果对于每个箭头
g
:
Y
−→
Y
J
,
下列图交换