理论计算机科学电子笔记40（2001）：计算λ演算的类模型

理论计算机科学电子笔记40（2001）网址：http://www.elsevier.nl/locate/entcs/volume40.html14页计算λ演算约翰·鲍尔1爱丁堡大学信息学系计算机科学基础实验室国王摘要我们考虑几个不同的声音和完整的类的模型的计算演算，解释定义，并概述为什么人们可能会感兴趣的各种类。 我们首先考虑闭范畴类，它是闭范畴概念的自然和直接的推广。然后，我们考虑封闭范畴，这是基于索引的类别，这是密切相关的现代编译技术。最后，我们考虑了一类Carnival闭范畴与一个-丰富单子。 后一类具有最发达的抽象理论，人们可以采用这种理论，并且可以按照麦克·莱恩的精神，通过这种理论，人们可以省去关于力量的连贯性细节1介绍计算λ-演算，或λc-演算，由Moggi在[13]中引入，是按值调用编程语言（如ML）的自然片段。它的模型被定义为λc-模型，它由一个具有有限乘积的范畴C和C上的一个强单子T组成，使得T具有Kleisli指数。一种是通过Kl（T）中的映射来模拟上下文中的项，Kl（T）是T的Kleisli范畴。λc-模型类是可靠的和完备的，但它不是微积分唯一可靠的和完备的模型类，考虑一些替代方案是有好处的。其中有些等价于λc-模型类，并有非平凡的证明，而有些则不是.在这里，我们考虑几个健全的和完整的类模型的λc演算和概述的一些原因，人们可能希望考虑他们。具体地说，一些健全的和完整的模型类由下式给出：(i) λc模型(ii) 闭Freyd-范畴1本工作由EPSRC资助GR/M56333：编程语言的结构：语法和语义2000年1月，出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-ND许可证。功率2⊗⊗→→(iii) 闭κ-范畴，以及(iv) Carnival封闭了范畴C和C上的一个富C单子。与λc-模型相反，闭Freyd-范畴[20]为λc-演算提供了一类直接的模型。我们的意思是，在一个闭Freyd范畴中，上下文Γ中X类型的项被从Γ的语义到X的语义的映射所建模，而在λc-模型中，它被从Γ的语义到执行一个操作的结果（即应用一个单子）到X的语义的映射所建模。例如，闭Freyd-范畴的观点允许人们给出λc-演算的Henkin模型[12]的自然概念，这可以在数据精化的研究中加以利用[9]。闭κ-范畴[19，20，10]具有不同的特征。它们由带有额外数据和公理的索引类别给出。索引类别的基本类别是其中一个模型上下文和值，而一个模型在纤维中的计算。这种观点与函数式编程语言的现代编译技术[1]有更直接的联系，并建议将λc-演算分解为κ-演算[6，20，10]和thunks。笛卡尔闭范畴C与C-丰富单子一起消除了对强度的需要。这在证明抽象的数学结果时很方便，因为它是丰富范畴[8]的大量文献的一个实例，允许使用大量研究的小C-丰富范畴的2-范畴C-Cat这允许容易地证明计算效应之间的关系，例如在将连续看作连续的一部分时：人们可以考虑从连续的单子到连续的单子的C当与[4]和[3]中开发的公理域理论相结合时，这允许在模型中考虑递归。更重要的是，它也是最适合对与计算结果相关的操作进行建模的一类模型[15]。Freyd-范畴的概念推广了有限积范畴的概念.定义是微妙的，由附属定义组成。首先，一个premonoidal范畴[18]是一个monoidal范畴，除了张量只需要分别是两个变量的函子，而不一定是双函子：给定映射f：AAJ和g：BBJ，明显的两个地图从一B至AJBJ可能会改变。 这种结构在计算效应存在的情况下自然出现，其中这两个映射之间的差异从灵敏度到评估顺序。给premonoidal范畴加上一个对称性，就像给monoidal范畴加上一个对称性一样，这是例行的。如果一个函子的目标函数是集合上的恒等函数，则称该函子是对象上的恒等函数。在这些定义下，Freyd范畴由一个对称premonoidal范畴K、一个有限积范畴C和一个对象上同一的严格对称premonoidal函子功率3−→−→J：C K。 闭Freyd-范畴形成了Carnival闭范畴概念的直接推广。在κ-范畴中，上下文Γ中的X类型项在隐式依赖于Γ的范畴中由形式为1M（X）的箭头建模，更准确地说，在M（Γ）上的索引范畴的纤维中由从1到M（X）的箭头建模。一个κ-范畴有一个弱的一阶约束概念，相当于断言沿着投影的重索引有一个左伴随：在Mac Lane的书[11]的精神中，[19]和[20]中缺少但在[10]中得到纠正的相干细节在编程术语中，这对应于绑定标识符但不产生第一个类函数的形式。这使得它适合于编译，因为人们可以将基本类别的对象视为堆栈[1，20]，并对序列进行添加将λc-演算用一个范畴闭范畴C与一个C-丰富的单子T一起建模，本质上与在λc-模型中建模是一样的：给出单子的丰富性等价于给出强度。然而，这类模型与其他模型并不等价，因为我们假设C是carbohydrate闭的，而其他类的情况并非如此。然而，它仍然通过Moggi的观察[14]提供了一个健全和完整的模型类这种观点的一个好处是C-Cat是一个研究得很好的2-范畴[8]，特别是C-Cat中单子的2-范畴已经经历了广泛的研究[21]。人们可以通过消除涉及强度的连贯性细节来利用这个抽象理论[11]。该文件的组织如下。在第2节中，我们给出了λc-演算的一个版本：为了方便起见，我们没有使用Moggi在[13]中的原始版本，而是使用了一个更少重复的版本。在第三节中，我们给出了Freyd-范畴的概念，并将λc-演算的模型定义为闭Freyd-范畴.在第4节中，我们定义了κ-范畴，解释了它们与前面的概念的关系，并解释了它们如何引起λc-演算的分解这与当前的编译技术有关。 最后，在第5节中，我们给出了一个健全的和完整的类模型方面丰富的类别，并概述了抽象的数学使用的观点。2计算λ-演算在本节中，我们给出了计算λ-演算或λc-演算的一个版本，并回顾了Moggiλc-演算有几个等价公式我们将不使用原来的公式，而使用一个等效的版本。这个版本的λc-演算具有由下式给出的类型构造函数：X：：= B |X1× X2|1 |X Y功率4⇒→↓ ≡≡−→↓↓≡ ↓ ∗ ↓ ↓↓↓其中，B是基类型，而X是 Y，而不是XY，将用于 表示指数。我们不断言类型构造函数TX的存在：这个公式等价于原来的公式，因为TX可以被定义为1X。λc-演算的项由下式给出：e：：= x |B |eJe |λx.e |∗|（e、e和J）|π i（e）其中x是变量，b是任意类型的基项，k是类型1，πi存在于i= 1或2时，都服从明显类型。同样，这与最初的表述不同，因为我们没有显式地有let构造函数或构造[e]或μ（e）。同样，这两个公式是等价的，因为我们可以考虑让ej中的x = e作为（λx.eJ）e的语法糖，[e]作为（λx）.e的语法糖，其中x是类型1，而μ（e）作为e（λ x）的语法糖。我们使用这个公式，因为它具有较少的数据，允许更容易的证明。此外，它更直接地是典型的按值调用语言的一个片段：上述类型构造函数和项构造函数（可能除了πλc-演算有两个谓词：存在（用表示）和等价（用表示）。规则可以表示为，x，λx.e对于所有e，如果e则πi（e），对于（e，eJ）也是如此。一个值是一个项e，使得e。 有两类规则。 第一个类说这是一个同余，允许变量在值上取值。第二类是基本结构和单元、产品和功能类型的规则。从这两个谓词的规则可以看出，类型与等价类一起形成一个类别，一个子类别由值确定。使用[13]中λc-演算的原始公式，可以很简单地说明使这个公式与原始公式一致所需的推理规则：只需记住模型是相同的，我们使用上面详细介绍的语法糖λc-演算表示值编程语言调用的一个片段.特别是，它被设计用于对ML的片段进行建模，但也是其他语言的片段，例如[3]中引入的理想化语言FPC。对于范畴论模型，关键特征是有两个实体，表达式和值。因此，按照我们已经公式化的方式对语言建模的最直接的方法是根据一对范畴V和E，以及一个对象上的同一包含函子J：V E。 这这一思路直接导致了闭Freyd范畴的概念，我们将在下一节中研究它。但第一个健全的和完整的一类模型的λc演算是由莫吉在[13]。对于Moggi，λc-模型由具有有限乘积的范畴C和C上的强单子T组成，使得T具有Kleisli指数，即，对于每对对象X和Y，函子C（−×X，TY）：Cop−→Set功率5−×⇒⇒−→ ⊗⊗⊗⊗⊗⇒−→−→⊗⊗ ⊗ −→ ⊗ ⊗ −→⊗是可代表的。 换句话说，存在一个物体XY，使得C（ZX，TY）同构于C（Z，XY）对所有Z，自然在Z中。 一上下文T中的类型X的项由T的Kleisli范畴中的映射建模，即，通过C中从M（r）到TM（X）的映射，其中M（）表示语义操作。3关闭Freyd-类别在本节中，我们定义并解释了闭Freyd-范畴的概念，并给出了它对λc-演算的观点的指示我们首先回顾[18]中介绍的和[17]中进一步研究的premonoidal范畴和严格premonoidal函子的定义及其对称性。我们用它们来定义Freyd-范畴的概念。premonoidal 范畴是monoidal 范畴概念的推广：它本质上是monoidal范畴，除了张量只需要是两个变量的函子而不一定是双函子，即， 给定映射f：X−→Y和fJ：XJYJ，从X得到的两个明显的映射XJ到YYJ可能会更好。为了使premonoidal范畴的概念精确，我们需要一些辅助定义。定义3.1一个二型范畴是一个范畴K，对于K的每个对象X，函子hX：K−→K和kX：K−→K使得对于K的每个对象对（X，Y），hX Y=kY X。关节值表示为XY。定义3.2Binoidal范畴K中的箭头f：X−→XJ是中心的，如果对于每个箭头g：Y−→YJ，下列图交换XYXgXYJYXgXYJXfY❄fYJ❄Yelf❄YJ·沃尔夫❄XJYXJYJXJgX XJYJXJgXJ一个自然变换α：G=H：CK称为中心变换，如果α的每个分支都是中心变换。定义3.3一个预么半群范畴是一个二元范畴K，它有K的一个对象I，以及有分量（X）的中心自然同构aY）的Z X（YZ），l与分量XXI，和r与分量X I X，服从两个方程：五边形表示a的相干性，三角形表示l和r关于a的相干性（参见[8]对图表的明确描述）。功率6−→−→⊗⊗⊗⊗⊗ −→⊗−→⊗−−→−→命题3.4给定一个对称monoidal范畴C上的强monad T，T的Kleisli范畴Kl（ T ） 是 一 个 premonoidal 范 畴 ， 其 中 函 数 J ： C Kl （ T ） 严 格 保 持premonoidal结构：一个monoidal范畴如C平凡地是一个premonoidal范畴。所以每个λc-模型都产生一个premonoidal范畴。定义3.5给定一个预幺半群范畴K，K的中心，记作Z（K），是K的子范畴，由K的所有对象和中心态射组成。给定一个对称monoidal范畴上的强monad，C不必是Kl（T）的中心。 但是，模的条件是J：CKl（T）是忠实的，或者等价地，单声道要求[13，18]，即，如果附加的单位是逐点单态的，它必是中心的一个子范畴。函子hX和kX保持中心映射。 所以我们有命题3.6一个premonoidal范畴的中心是一个monoidal范畴。这个命题使我们能够证明前monoidal范畴的一个凝聚结果，直接推广了monoidal范畴通常的凝聚结果详情见[18]。定义3.7预么半群范畴的对称性是具有分量c的中心自然同构：XYYX，满足两个条件c2= 1和来自（X）的两个显映射相等Y）的Z到Z（XY）。一个对称的premonoidal范畴是一个premonoidal范畴和一个对称。对称的premonoidal范畴是我们主要感兴趣的范畴，而且似乎也是指称语义学主要感兴趣的范畴。定义3.8严格预幺半群函子是保持所有结构并将中心映射发送到中心映射的函子。类似 地， 可以 将严 格对 称monoidal 函子 的定 义推 广到严 格对 称premonoidal函子。定义3.9一个Freyd-范畴由一个具有有限乘积的范畴C，一个对称的Premonoidal范畴K，和一个关于对象的恒等式严格对称的Premonoidal函子J：C K组成。 严格Freyd-函子由一对严格保持所有Freyd-结构的函子定义3.10A Freyd-类别J：CK是闭的，如果对于每个对象X，函子J（X）：CK有一个右伴随。严格闭Freyd-函子是严格保持所有闭结构的Freyd-函子功率7−→►×►注意，它遵循函子J：C K有一个右伴随，K是C上单子的Kleisli范畴。 我们有时把Freyd范畴写成K，因为结构的其余部分通常是隐式的：通常，它由Z（K）和包含给出。[17]的一个主要定理的变体是定理3.11给出一个闭Frequency-category是指给出一个具有有限积的范畴C，以及C上的一个强单子T和指定的Kleisli指数。 给出一个严格闭的Frequency-functor就是给出一个严格保持Kleisli指数的强单子的严格映射。给定一个有有限乘积的范畴C和一个强单子T，Kl（T）是一个Freyd-范畴。然而，虽然一个保持强单子和有限乘积的函子产生一个严格的Freyd-函子，但反过来就不成立了。从Moggi的结果可以得出说明我们在第2节中描述的λc-演算如何直接在一个闭Freyd-范畴中建模是例行公事：闭Freyd-范畴定义的结构几乎完全反映了演算定义的结构。需要注意的一点是，人们必须决定如何对（e，eJ）建模，因为原则上有两种可能性，人们必须任意选择。 所以我们选择对Γ（e，eJ）建模：XY由复合M（Γ）−→M（Γ）×M（Γ）−→M（X）×M（Γ）−→M（X）×M（Y）用Freyd结构给出的明显的映射。λ-项和应用直接使用封闭结构建模这种λc演算模型的表述有几种用途。它提供了一个直接的模型类，在这个意义上，一个术语在上下文Γt：X由Freyd-范畴中从M（Γ）到M（X）的映射建模。这与博弈模型给出的计算现象的模型类别非常吻合，如[2]和[7]中所解释的。这个公式也可以用来将Henkin模型[12]的概念从简单类型的λ-演算推广到λc-演算。对于简单类型的λ-演算，有命题3.12如果L是由λ-演算的一个签名自由生成的Carnival闭范畴，那么给出一个Henkin模型等价于给出一个有限积保持函子H：L −→ Set使得诱导函数H（σ<$τ）−→（H（σ）<$H（τ））是内射的。这个命题的一个变体已经被用于分析简单类型λ演算的数据精化：人们需要将逻辑关系的概念放松为松散逻辑关系的概念，以便允许数据精化的组合[16]，而这种放松正是命题3.12的意义。使用Freyd范畴的概念，我们可以从功率8⇒ −→⇒−→简单地将λ-演算类型化为λc-演算如下。定义 3.13 如果L是由λ c-演算的符号自由生成的闭Freyd -范畴，则Henkin模型是从L到由包含J：Set −→ Set p给出的Freyd -范畴的Freyd-函子，使得诱导函数H（σ τ）（H（σ）H（τ））是单射的，其中集合p是 小集合和部分函数范畴。这一概念的二进制版本，即用一对集合系统地替换一个集合，已经被用来解释λc-演算的数据精化[9]。我们在上面观察到，Freyd-函子不能用λc-模型的结构来表示。所以这提供了一个例子，说明把闭Freyd-范畴作为λc-演算的模型的价值。4闭κ-范畴在本节中，我们介绍κ-范畴，如[19]中所定义的，并在[20]特别是[10]中进行了修改和稍微更正，并提出了使用封闭κ-范畴作为λc-演算模型的想法。在[19]中已经证明了Freyd-范畴等价于κ-范畴：我们在这里回忆一下构造。 扩展这个等价性是很常见的，我们可以看到闭Freyd-范畴等价于闭κ-范畴，这表明后者为λc-演算提供了一个可靠而完备的模型类[20]。给定一个小范畴C，从Cop到Cat的函子称为索引范畴，两个索引范畴之间的自然变换称为 索引函子索引自然转换的概念也是可以定义的。定义4.1一个κ-范畴由一个具有有限乘积的小范畴C和一个索引范畴H组成：Cop−→Cat，使得• 对于C的每个对象A，ObHA=ObC，并且对于每个箭头f：A−→B，C，函子Hf：HB−→HA是一个对象上的恒等式函子• 对于每一个三元对象，有一个同构κ：HA×B（1，Hπ D）−→HA（B，D）自然存在于A和D中。• 从H1（1，D）到H1×1（1，D）的两个函数，一个由重标化给出，另一个由κ给出，是相等的.从定义中观察到，对于C中的每个投影π：B×A−→B，函子Hπ：HB−→HB×A在对象上有一个左伴随L，由下式给出A× −。我们将与这些映射相关的同构表示为：κ：HB×A（D，DJ）= HB（D×A，DJ）.定义4.2Aκ-范畴H：Cop Cat是闭的，如果对每个对象A对于C，每个对象都有一个从A到它的类属映射，即，对于每个对象B功率9−→−→−→ ⊗−→−→在C中，存在一个对象[A，B]和一个映射apply：A−→B在H[A，B]中，使得对于每个对象X和每个映射f：A−→B在HX中，存在一个唯一的映射λf：X−→[A，B]在C中，使得Hλf（apply）=f。为了了解Freyd-范畴是如何产生κ-范畴的，我们从前者构造了后者。这需要一些补充定义。定义4.3一个预么半群范畴K中的一个comm由K的一个对象A和中心映射δ组成：A和V：A我在做通常的结合性和单位图可以互换。在预幺半群范畴K中，从A到B的可交换映射是一个中心映射f：AB，与commoduliplications和commoduli的。给定一个预幺半群范畴K，K中的余映射和余映射构成一个范畴Comon（K），其合成由K的合成给出。此外，任何严格预幺半群函子H：K−→L提升为函子Comon（H）：Comon（K）−→Comon（L）。简 单 地 说 ， 任 何 commonadA 产 生 一 个 commonad−A ， 而 任 何commonad映射f：A−→B产生一个从Kl（−A）到Kl（− B）的函子，Kl（− A）是commonad−A的Kleisli范畴，Kl（−B）是对象上的恒等式。所以我们有一个函子simple（K）：Comon（K）op−→Cat。给定一个具有有限乘积的范畴C，C的每个对象A都有一个唯一的组合结构，由对角线和到终端对象的唯一映射给出。所以Comon（C）同构于C。因此，给定一个Freyd-范畴J：C−→K，我们有一个函子，通过将simple（K）与yJ从C=Comon（C）tooComon（K）导出的函子进行复合得到：我们将这个复合函子记为s（J）：Cop−→Cat。定理4.4 [19]对任意自由范畴J：CK，标函子s（J）：C opCat是κ-范畴，并且每个κ-范畴唯一地从自由范畴产生直到凝聚同构。推论4.5对任何闭Fredom-范畴J，κ-范畴s（J）是闭的，对任何闭κ-范畴H，存在一个闭Fredom-范畴J，直到凝聚同构为止唯一，使得s（J）同构于H。这一结果意味着闭κ-范畴为λc-演算提供了一个可靠而完备的模型。基本类别中的有限产品展示了如何对产品类型进行建模;封闭结构的定义展示了如何对高阶类型进行建模。上下文Γ中的X型项由M（Γ）上的纤维中从1到M（X）的映射来建模闭κ-范畴定义的结构展示了如何对项构造子进行建模。为了对（e，eJ）进行建模，按照第3节的说明，从Freyd-结构到κ-结构进行了明显的修改。使用索引类别对简单类型的λ演算进行建模功率10×· ··×λ-演算的不同特征，用Carnival闭范畴对其进行建模类似地，在这里，用闭κ-范畴对λc-演算建模突出了它与闭Freyd-范畴所突出的那些不同的特征。对于κ-category，我们可以将基本category视为提供堆栈。我们可以看到，κ-范畴的定义产生了一种语法，这种语法与最近在函数式编程语言的编译器技术中使用的一类密切相关的语法集非常相似[1]。因此，κ-范畴和围绕它们的结果为当前的编译器工作提供了语义支持，并建议对λc-演算进行分解，由于它与长谷川的概念[6]的关系，我们可以称之为κ-演算[20]由于λc-模型等价于闭κ-范畴，因此相应地，λc-演算的项是通过在κ-演算中添加thunks来给出的。κ-演算的谓词和规则可以从λc-演算的一阶片段的谓词和规则导出。κ-演算的计算判断具有以下形式：x1：C1，.，x n：C n，AcM：B其中A是一个类型，被理解为M运行之前的堆栈类型，B是M运行之后的堆栈类型。价值判断的形式是x1：C1，.，x n：C nV：B计算判断表示C1Cn上纤维中从A到B的态射。值判断以通常的方式表示基中的态射。语法和关键类型规则如下：V：CΓ，Acpush（V）：C×AΓ，x：C，AcM：BΓ，C×Acκx.M：BΓ，AcM：BΓ，BcN：CΓ，AcM;N：C添加thunks可以恢复与λc-演算等价的演算所需的打字是Γ，AcM：BΓmkthunkM：[A→B]A×[A→B]capply：B所以push（V）可以理解为将一个值压入栈中（栈顶写在左边），而κx.M则弹出一个值并将其绑定到M中的x。符号;由M（Γ）上的索引范畴的纤维中的复合来建模。 这里的想法是，最近推送的值由κ弹出，并且在添加封闭性假设后，apply打开由mkthunk创建的闭包。关于这个演算的更多分析，参见[20]和[10]。5丰富的类别在本节中，我们将概述最后一类λc演算模型功率11⇒ ×⇒⇒ −→⇒对于任何卡氏闭（或更一般的对称么半群闭）范畴C，我们可以称之为C-范畴。其思想是，一个C-范畴有一个C的homobject，而不是像通常的范畴定义中那样有homset。形式上，定义如下。定义5.1AC-D类包括• 一个集合ObD，其中的元素被称为D的对象，• 对于D的每对对象（A，B），C的对象D（A，B）• 对于每个三元组（A，B，E），一个映射：D（B，E）×D（A，B）−→D（A，E）• 对于每个对象A，映射jA：1-→D（A，A）服从方程以迫使comp与由jA主要的例子有C=Set，在这种情况下，C-范畴在通常情况下就是一个局部小范畴。指称语义学中其他主要关注的例子有C=Poset或ω-cpo的范畴，或预层范畴，或更一般的topos。也可以考虑C=Cat。定义5.2C-函子H：D−→E由以下组成：• 函数ObH：ObD−→ObE，我们通常将其转换为H• 对于D的每一对对象（A，B），有一个映射H（A，B）：D（A，B）−→E（HA，HB）服从公理，即H保持合成和恒等式。C-自然变换的概念也可以用类似的方法来实现。(see[8]的细节），从而产生了C-monad和C-Kleisli范畴的概念。这是最优雅地被视为一个例子街的分析单子它是民间传说，也是作为一种（很）特殊的个案出现的主要结果 [5]我们有定理5.3给出范畴C上的一个强单子等价于给出C上的一个C-单子。证据给定C上的一个强单子T，我们需要定义C中的映射的形式为（AB）、（TATB）。 为了做到这一点，根据米田引理，它给出了一个自然的函数族，C（X，A<$B）−→C（X，TA<$TB）但C（X，AB）同构于C（XA，B），对于C（X，TA）也是如此TB）。因此，强度的数据给出了这样的函数，而公理则给出了充实函子的公理。逆构式也使用米田引理，但使用B中的自然性而不是X中的自然性。这是一个繁琐的计算，涉及嵌套应用米田引理，以验证公理的强度匹配那些丰富。✷功率12−→−→从莫吉的观察可以得出，在toposes上的强单子一个可靠且完备的λc-模型类，Carnival闭范畴C的类与一个C-单子一起给出另一个可靠且完备的λc-模型类，尽管它与我们迄今为止所考虑的那些不等价。在这样的结构中，λc演算的建模似乎并不直接告诉我们很多关于λc演算的新东西：我们只是在λc模型中复制了通常的建模。有一个张量C-范畴的既定概念[8]可以提供洞察力：C上的C-单子T的形式为Kl（T）的所有C-范畴都是张量的，并且张量模型类型的乘积。然而，这种观点确实允许相关兴趣的抽象数学结果。例如，从这一特性可以直接得出，集合上的任何单子都有一个强度：给出一个强度就等于给出一个丰富度，而集合上的单子是平凡而唯一的。在Set上丰富。类似地，它也立即得出，P oset上的任何单子或ω-cpo的范畴至多有一个强度，因此，一旦找到一个，就不必再 事实上，在Cat上至多也有一个单子的丰富，但这个事实并不是微不足道的。Street例如，它显示定理5.4给定范畴C上的C-单子S和T，若给出一个C-函子H：K1（S）K1（T）与C上的标准C-函子交换，等价于给出一个从S到T的C-单子态射。解开这个结果，从张量的定义[8]可以得出，定理中的任何C-函子都保持张量，因此，给出这样一个C-函子等价于给出一个严格的Freyd-函子。C-monad态射的概念综合起来，我们得出结论，推论5.5给定一个范畴C上的强单子S和T，给出一个与C的正则函子可交换的严格Fredom函子H：Kl（S）Kl（T）等价于给出从S到T的强单子的态射。有趣的一个原因是，如果我们把S看作是一个偏序单子，那么我们需要一个从Kl（S）到Kl（T）的严格Freyd-函子，以便把递归的考虑纳入λc-演算，模型是根据强单子T来取的。功率13但是，这一部分的健全和完整的模型尚未得到充分利用。它当然为与计算效应相关的代数运算建模提供了基础[15]，但事实上，它可能在运算和方程方面，或者甚至在运算和观测方面，6结论Eugenio Moggi在[13]中引入了计算λ-演算，或λc-演算他给出了一个健全的和完整的一类模型的λc-演算的基础上，一个范畴C的有限产品和一个强单子T在C上，使T有克莱斯利指数;然后他模拟了λc-演算的克莱斯利范畴Kl（T）的T。在这里，我们给出了λc-演算的另外三个可靠而完备的模型类，其中一些等价于莫吉提出的模型类，另一个不等价。对于不同的目的，似乎最好使用不同的类;每个类都以不同的方式自然地推广到其他类。例如，封闭的Freyd-范畴[18，19]提供了直接的模型.相反，闭κ-范畴[19，10]自然地在依赖类型理论的方向上推广。当人们想要将λc-演算的建模扩展到与计算结果相关的代数运算建模时，使用丰富范畴似乎是最自然的[15]，例如非确定性或。引用[1] R. Douence和P. Fradet，函数式语言实现的分类第一部分：按值调用，INRIA研究报告第2783号，1996年。[2] M. Fiore和K. Honda，Recursive Types in Games：Axiomatics andProcess Representation，Proc LICS98（1998）345[3] M.菲奥雷和动力局Plotkin，em计算充分域理论模型的公理化，ProcLICS94（1994）92[4] M. Fiore，G. D. 杨文，等，公理化域理论中的完全立方集，北京：科学出版社，1997年，第268[5] R. 戈 登 和 AJ 权力， 丰 富 通 过 变 化 ， J。 纯 粹 应 用 代 数 120（1997）167-185.[6] M.陈文，《计算机科学与工程》，第一卷，第二卷，第一章，第一章，第二卷，第二章，第三章，第四章，第五章，第五章，第六章，第五章，第五章，第六章，第五章，第五章，第六章，第六章，第五章，第六章，第五章，第六章，第六章，第五章，第六章，第六章，第五章功率14[7] K. Honda和N.陈文龙，基于博弈论的数值计算方法研究，[8] 通用汽车Kelly，[9] Y. Kinoshita和A. J. Power，按值调用语言的数据细化，[10] P.B. Levy，A.J. Power，and H. Thielecke，在按值调用编程语言中建模环境（已提交）。[11] Saunders Mac Lane，[12] J. Mitchell，“Foundations for Programming Languages”，Foundations of Computing Series，MIT Press（1996）。[13] E. Moggi，计算λ演算和Monads，Proc LICS89（1989）14[14] E. Moggi ， Notions of computation and Monads ， Information andComputation93（1991）55[15] G.D.陈文辉，代数运算的基本原理，[16] G.D. Plotkin ， A.J. 动 力 D.T.Sannella 和 R.D.Tennent ， Lax logicalrelations，计算机科学笔记1853（2000）85[17] A.J. Power，Premonoidal categories as categories with algebraicstructure，Theoretical Computer Science（即将出版）。[18] A. J. Power和E. P. Robinson，Premonoidal范畴和计算概念，计算机科学中的数学结构7（1997）453-468。[19] A.J. Power和H.陈文辉，环境、延续语意与索引分类，[20] A.J. Power和H. 陈文辉，“计算机科学与应用”，国立台湾大学[21] 张文，单元的形式理论，《纯应用代数学》，2001年，第2期，第10卷，第11期，第11页。（1972）149