按值调用程序设计语言中数据精化的范畴论建模

理论计算机科学电子笔记225（2009）281-302www.elsevier.com/locate/entcs按值调用程序设计语言中数据精化的公理化John Power约翰·鲍尔1，2巴斯大学计算机科学系地址：Claverton Down，Bath BA2 7AY，UK田中美纪3国立信息通信技术研究所东京都小金井区能井北町4-2-1邮编184-8795摘要本文给出了一个系统的范畴论公理系统，用于在按值调用程序设计语言中对数据精化进行建模。我们的值调用语言的主要例子是计算λ演算的扩展，如FPC和建模非确定性的语言，以及计算λ演算的一阶片段的扩展，如CPS语言。 我们给出了一个范畴论的解释基本设置，然后展示如何建模上下文，然后是任意类型和术语构造器，然后是签名，最后是数据细化。这扩展并澄清了Kinoshita和Power关键词：计算lambda演算，premonoidal范畴，数据精化，松散逻辑关系。1介绍有两种主要的范畴理论方法来建模数据细化。其中一个来自Tony HoareHoare[6]，然后Hoare和何继峰[7]（参见[16]标准分类理论术语的说明，参见[17]这些思想在实践中的应用），将数据精化组成的思想作为基本思想，即，如果M定义N，N定义P，则M定义P。然而，这种方法并不容易推广到更高阶的类型，例如在λ演算中，如[31]中所解释的（但1作者已获得EPSRC资助GR/M56333：编程语言的结构语法和语义和GR/586372/01：程序设计语言的语法理论2电子邮件：ajp@inf.ed.ac.uk3电子邮件：miki. nict.go.jp1571-0661/© 2008 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2008.12.081282J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281−→参见[23]，了解使用等同变压器的解决方案）。 另一种方法有很多来源，但Tennent [31]强烈提倡使用二元逻辑关系[21，19，4]来建模数据细化。二进制逻辑关系对数据抽象进行建模，非常适合高阶类型，但它们不组合。 因此，人们寻求一种共同的概括，对于更高阶的类型，它在组合下是封闭的。 这导致了一种观念，逻辑关系[24，15]和变体[14]。在这里，我们解释和发展的概念，松散的逻辑关系的设置调用的价值语言，但澄清和扩展的工作[15]的基础上。对于由签名λ生成的简单类型λ-演算，Hermida [4]证明了给出一个逻辑关系等价于给出一个从由λ的项模型所确定的Carnival闭范畴L到Rel 2的严格Carnival闭函子，Rel 2是一个对象是一对集合X和Y以及从X到Y的二元关系R的Carnival闭范畴。一个松散的逻辑关系是完全相同的，除了从L到Rel2的函子，虽然仍然需要严格地保持有限乘积，等价地，尊重上下文，不需要保持指数。[24]这是一个语法上的对应，但上面的定义是最紧凑的。对于按值调用语言，情况更加复杂。我们必须区分值和任意表达式。因此，不是考虑单个范畴L，而是考虑一对范畴L v和L e，前者用于对上下文中的值进行建模，后者用于对上下文中的任意表达式进行建模，以及对象函子L上的恒等式：L v它能让我们看到作为可能的表达。Carnival封闭性的概念必须相应地被推广，从而产生封闭Freyd-范畴的概念[30]，而松散逻辑关系的概念也可以而且必须相应地被推广[15]。值语言调用的一个主要例子是Moggi 但是还有许多其他的按值调用语言，例如FPC[3]，一些CPS语言[32]和具有非确定性的语言[1]。因此，我们应该系统地描述按值调用语言的数据细化，其中包括广泛的这些语言，这就是本文的主题。因此本文澄清并扩展了[15]的工作，其中注意力仅限于λc-演算。我们首先描述了调用值语言的模型。这需要小心。在第2节中，我们回顾了计算λ-演算，并展示了它的中心特征，即值和任意表达式之间的区别，是如何用范畴理论术语建模的，特别是用丰富于carnival闭范畴[→，Set]的范畴建模的，carnival闭范畴[→，Set ]是来自箭头范畴的函子的函子范畴 设置。一个[→，Set]-范畴正好由一对范畴A0和A1以及一个关于对象函子A的恒等式组成：A0−→A1。如上所述，上下文的概念是数据细化的基础，我们将在第三节中讨论简单类型的值调用语言中上下文的范畴论建模。 我们回顾了Freyd-范畴的概念，解释了为什么它是我们感兴趣的，并展示如何在这里使用它J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281283→→→→接下来是[15]中计算λ-演算建模的中心概括：我们必须展示如何建模任意类型和项构造函数，而不仅仅是λc-演算的构造函数。这就要求在小[，Set]-范畴的范畴[，Set]-Cat上有一个代数结构的概念，即等价的有限单子。 一旦人们理解了普通范畴的代数结构，就像在[ 16 ]中描述Hoare的数据精化方法时所用的那样，将其推广在上面谈到由签名生成的语言时，我们提出了一个问题，那就是如何给出签名概念的范畴论表述这是由有限单子T的T-草图的概念提供的。同样，一旦理解了对于范畴，对[，Set]-categories的扩展并不困难，但需要一点小心。在第5节中，我们还对T-草图的概念给出了一个比文献中的定义最后，我们到达数据细化的建模。 通过上述扩展 或者是对以前工作的改进，我们通常在[15]中推广松散逻辑关系的概念。在这样做时，我们给出了一个版本的基本引理，这是一个更直接的推广，其通常的提法比出现在[15]。我们还给出了一个条件，在这个条件下，松散的逻辑关系构成了我们所有的主要例子;人们可以立即看到，松散的逻辑关系也解释了高阶结构。在本文中，我们不解决[14]的主题表示独立性，但是[14]的技术基于[18]中的T-草图，扩展到本文的设置。 我们计划进行这一扩展，但目前还不完全清楚如何做目前还没有我们也不明确与逻辑的关系。在简单类型的λ-演算和类似语言的情况下，可以使用具有结构的fibrations [4];但在这里如何做到这一点还不清楚，因为我们不仅从逻辑关系推广到松散的逻辑关系，而且我们还推广到按值语言的调用，并且在这种情况下还没有开发出适当的纤维化概念：它可能很简单，但仍有待研究。2通过值语言建模调用我们在本文中的目标是为值调用编程语言建模数据细化。因此，为了具体起见，我们将介绍一个通过值语言调用的主要示例，并概述其模型的关键特征我们考虑计算λ-演算或λc-演算的一个版本[22]。λc演算有几个等价的公式。最初的公式包括类型构造函数TX和相关的项构造函数[e]和μ（e）。但它们是多余的，所以我们省略它们。λc-演算具有由下式给出的类型构造器：（一）其中B是基本类型。X：：= B |X1× X2|1 |X Y284J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281∗→⇒≡≡→−→−→↓ ↓↓≡ ↓∗ ↓ ↓↓↓−→ −→−→λc-演算的项由下式给出：(2)e：：= x |B |eJe |λx.e |∗|（e、e和J）|π i（e）其中x是变量，b是任意类型的基项，是1型的，πi对于i=1或2存在，所有都服从明显的类型。在λ c -演算的描述中经常会看到let构造函数，x=e in eJ是（λx.eJ）e的语法糖。它只在考虑微积分的一阶部分时起重要作用[27]，因此，为了简单起见，我们在这里省略了它。λc演算有两个谓词：存在性（用表示）和等价性（用表示）。. 的规则可以表述为，x，λx.e对于所有e，如果e则πi（e），对于（e，eJ）也是如此。 一个值是一个项e，使得e。 假设的规则是一个同余，允许变量在值上变化;还有基本结构和单位，产品和功能类型的规则它遵循的规则是，类型与上下文中的等价类一起形成一个类别，其中一个子类别由值确定使用[22]中λc-演算的原始公式，可以很简单地说明使这个公式与原始公式一致所需的推理规则：只需记住模型是相同的，我们使用上面详细介绍的语法糖。我们不会通过重复[22]的规则来扰乱我们的演示文稿。λc-演算代表了一个通过值编程语言调用的片段特别是，它被设计为模型ML的片段，但也是其他语言的片段，如FPC[3]或值语言的非确定性调用[1]。一阶片段是[32]的CPS演算的一部分，而CPS演算又是用于编译M L的Appel演算的类型化版本，如[ 32 ]中所解释的对于范畴论模型，关键的特征是有两个实体，表达式和值，因此，按照我们已经制定的方式来建模语言的最直接的方法是根据一对范畴L v和L e，以及对象包含函子L上的恒等式：L vL e.这需要对有限积的概念进行一些推广，以便对上下文和产品类型进行建模，并进一步服从模型X和Y的封闭性条件，我们将在后面的章节中解释。对我们来说，关键的一点是，基本信息，即， 范畴Lv和Le以及对象函子上的恒等式（它的忠实性是一种干扰）L：LvLe，正好相当于一个充实范畴的数据和公理：设[，Set]表示从Arrow范畴到Set的函子的函子范畴，并考虑它的Caribbean闭结构。[11]这是一个丰富的范畴的定义，命题2.1一个[→，Set]-范畴由范畴A0和A1以及对象函子A上的恒等式：A0−→A1组成。一个从A：A0−→A1到AJ：AJ0AJ1的[→，Set ] -函子由一对函子F0：A0组成AJ0和F1：A1AJ1使函子的平方可交换。一个从（F0，F1）到（G0，G1）的[，Set ] -自然变换由一个自然变换α：F0G0组成，其自然性扩展到A1.J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281285⊗⊗⊗−−⊗−→ −→ ⊗⊗⊗⊗⊗通过系统地使用这种观察和丰富范畴理论[11]，我们可以通过值语言来建模调用，例如计算λ演算[22]，扩展[3，1]以及其一阶片段的扩展，例如用于在[32，30]中建模延拓。我们将系统地展示如何对这些语言进行建模，然后最终展示如何将这种分析扩展到模型数据细化。3建模上下文我们对值调用语言和数据细化建模的核心是上下文建模。在给出数据精化的公理化解释时，我们希望数据精化尊重上下文，而不要求尊重任何其他结构。因此，我们需要特别注意建模上下文。这对于按值调用的语言来说是微妙的，需要Freyd-范畴的概念[30]。所以在这一节中，我们发展Freyd-范畴的机器我们必须首先回忆premonoidal范畴和严格premonoidal函子的定义，以及它们的对称性，如在[28]中介绍并在[1，26，32，30]中进一步premonoidal范畴是monoidal范畴概念的推广：它本质上是monoidal范畴，除了张量只需要是两个变量的函子而不一定是双函子，即，给定映射f：XXJ和g：YYJ，从X得到的两个明显的映射Y到XJ你可能会说。给定一个对称幺半群范畴C，如Set，和C的一个对象S，我们可以考虑具有与C相同的对象和D（X，XJ）=C（S X，S XJ）的范畴D，其复合由C的复合诱导。 这种结构可[22]这是一个很好的例子。范畴D不具有有限积或monoidal结构，如通常用于建模上下文，问题在于，尽管有明显的函子X和对于任意对象X和Y，它们不产生双函子。因此，我们需要一种精确的方式来阐明D结构的具体内容，从而能够解释其中的语境。定义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，下列图交换XYX）gXYJY<$Xg<$X）YJ<$XfYvfYJvYelfvYJ·沃尔夫vXJY）XJ YJXJgYXJ）YJ XJgXJ286J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281−→⇒−→−→⊗ ⊗−→⊗ ⊗ −→ ⊗ −→ ⊗一个自然变换α：G=H：CK称为中心变换，如果α的每个分支都是中心变换。定义3.3一个预幺半群范畴是一个二素范畴K，它有K的一个对象I，以及有分量（XY）Z的中心自然同构aX（YZ），l与分量XXI和r与分量X我X，服从两个方程：五边形表示a的相干性，三角形表示l和r相对于a的相干性（参见[11]对图表的明确描述）。命题3.4给定一个对称monoidal范畴C上的强monad T，T的Kleisli范畴Kl（T）是一个premonoidal范畴，函子J：C Kl（T）严格保持premonoidal结构：一个monoidal范畴如C平凡地是一个premonoidal范畴。莫吉Moggi证明了在Carbohydrate闭范畴上的强单子的Kleisli范畴提供了一个健全的完备类关于λc演算的模型[22]。 更具体地说，我们可以取C=Set或ω-cpo的范畴，它们都是carlington闭的;我们可以在它们上面取一个强单子，比如提升单子或用于建模边项、例外、延续等的单子。更具体地说，这篇论文[27]展示了每一个可数的Lawvere理论如何产生一个典型的premonoidal范畴，包括刚才引用的所有例子更一般地说，前么半群对偶的克莱斯利范畴[29]也提供了一类很好的前么半群范畴的例子，包括一类更自然的侧效应模型。在定义了premonoidal范畴的概念之后，我们需要一个辅助定义，即premonoidal范畴K的中心的定义，它被定义为K的子范畴，由K的所有对象和中心态射组成。这个概念是根本的Thielecke给定一个对称monoidal范畴上的强monad，基范畴C不必是Kl（T）的中心。 但是，模的条件是J：CKl（T）忠实，或等效地，单声道要求[22，28]，即，如果附加的单位是逐点单态的，它必是中心的一个子范畴。函子hX和kX保持中心映射。 所以我们有命题3.5 P r e m o n o i d a l 范 畴 的中心是monoidal范畴。由此我们可以推出预幺半群范畴的凝聚定理定理3.6在定义一个前么半群范畴时，从结构自然变换中建立的每一个图都是可交换的。证据 由于一个premonoidal范畴的中心是一个monoidal范畴，结构图是中心，结果立即从连贯性，J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281287→→⊗ ⊗ ⊗⊗−→⊗ −→⊗⊗−−→−→一个monoidal范畴，如Kelly对Mac Lane证明的改进Q我们主要感兴趣的所有premonoidal范畴在某种合理的意义上都是对称的，我们需要这种对称性来证明模型的可靠性 因此我们精确地定义了预么半群范畴的对称性概念。定义3.7预么半群范畴的对称性是具有分量c：X的中心自然同构YYX，满足两个条件 c2= 1和从（XY）Z到Z（XY）的两个明显映射相等.一个对称的premonoidal范畴是一个premonoidal范畴和一个对称。最后，我们需要另一个补充定义。 我们这里的关键概念是是Freyd-范畴，但我们需要premonoidal范畴和严格对称premonoidal函子的概念来定义它。定义3.8严格预幺半群函子是保持所有结构并将中心映射发送到中心映射的函子。类似地，可以将严格对称monoidal函子的定义推广到严格对称premonoidal函子。最后，我们能够定义Freyd-范畴的概念，这是本节的中心定义定义3.9一个Freyd-范畴由一个有有限乘积的范畴A0，一个对称的Premonoidal范畴A1，和一个关于对象的恒等式严格对称Premonoidal函子A：A0A1组成。严格Freyd-函子由一对严格保持所有Freyd-结构的给定一个有有限乘积的范畴C和一个强单子T，Kl（T）是一个Freyd-范畴。一个严格保持强单子和有限乘积的函子产生一个严格的Freyd-函子，但反之则不成立。从定义可以直接看出，Freyd-范畴是具有额外结构的[，Set]-范畴。在下一节中， 我们将明确的概念， [ ，集合]-范畴的代数结构，并应看到，一个Fryed-范畴可以 被这样看待。 但首先，我们发展了Freyd-范畴的概念， 自己的条件。注意，从A：A0−→A1到AJ：AJ0−→AJ1的严格Freyd-函子不需要将A1的每个中心映射都发送到AJ1的中心映射：中心性是一个前monoidal范畴中的映射的性质，而不是一个结构;所以我们没有明确要求它被保持。定义Freyd-范畴的关键原因正是为了避免Freyd-函子保持任意中心映射A0中的映射必然是A1中的中心映射，它们被发送到AJ0中的映射，因此被发送到AJ1中的中心映射，但是我们具体地不要求将任意的中心映射发送到中心映射。定义3.10A Freyd-类别A：A0如果对于每个对象X，函子A（X）：A01有一个右伴随。 严格闭Freyd-函子是严格保持所有闭结构的Freyd-函子288J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281−→× −−→∨→→→注意，如果A是闭的，那么通过取X为单位I，可以得出函子A：A1有一个右伴随，所以A1是 A0上的单子我们有时把Freyd范畴写成A1，因为结构的其余部分可能是隐式的：通常，它由A1的中心和包含给出给定一个具有有限乘积的范畴C和C上的一个强单子T，如果对于C的每个对象X，函子J（X）：CKl（T）有一个右伴随。[26]的一个主要定理的变体是定理3.11给出一个闭Freyd-范畴就是给出一个具有有限积的范畴C，以及C上的一个强单子T和所分配的Kleisli指数。给出一个严格闭Freyd-函子就是给出一个严格保持Kleisli指数的强单子的严格映射。从Moggi的结果可以得出在闭Freyd范畴中定义λc演算的模型的概念是例行公事：类型由A0的对象建模，等价于A1;乘积和指数类型分别由premonoidal和闭结构建模;对于配对，人们在建模（e，EJ）时进行系统选择，无论是从左向右还是相反。从左到右似乎普遍青睐[22，30，32]。4建模类型和术语构造函数在按值调用编程语言中，我们在上一节，但也有一个任意的类型和术语构造函数的集合，这些都受到方程式的影响。 例如，λc-演算和FPC都有指数类型，FPC有余积类型，而非确定性语言有一个项构造函数来模拟非确定性运算符[1]。 因此，我们寻求一个一般的范畴理论的模型类型和长期建设者的帐户。范畴[→，Set]-Cat上的代数结构或等价的无穷单子的概念为我们提供了这样一个统一的结构[，Set]-范畴的代数结构研究具有代数结构的集合[13，2]。人们早就知道，对于一个单排序签名，服从方程的每一类代数都是等价的 [20]在集合范畴上的有限单子的代数范畴; 术语因此，我们对[，Set]-范畴的代数结构的定义的特征在于将该定理从集合推广到[，Set]-范畴。[13]中有一篇文章解释了这一结果的更大的一般性，[25]中有一个关于具有结构的范畴的版本;但关于在这一一般性水平上的工作，请参见[26]。在普通泛代数中，代数是一个集合X和一个基本运算族σ：Xn→X，在导出运算之间服从方程。为了定义[→，Set]-范畴上的代数结构，我们当然必须用一个[→，Set]-范畴A来代替集合X。也可以用一个有限可表示的[→，Set]-范畴c来代替有限数n。J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281289→→→→→→→→→→→→→→→→−→Σ有限可表示[，Set]-范畴的定义提供了有限集合概念的定义推广，用于在此背景下对泛代数的标准范畴论处理[13]。但是定义是复杂的，所有的有限[，Set]-范畴都是有限可呈现的，而有限[，Set]-范畴是我们唯一需要的有限可呈现的[，Set]-范畴。所以我们在这里省略定义，请感兴趣的读者参考[12]。还必须将来自[，Set]-Cat（c，A）的函数推广到A的对象集合中，以允许来自[，集合]-Cat（c，A）到A0和A 0的箭头集合中，的1.这些都受制于衍生操作之间的等式。因此，我们提到的所有语言的模型，即， λ c-演算或其一阶片段通过各种类型和项构造子的扩展，具有结构和严格保持结构的函子的小[，Set ]-范畴的范畴等价于代数范畴T-Alg，对于无穷单子T在[→，设置]-猫。为了包括我们所有的例子，特别是那些涉及高阶结构的例子，无论是在λc-演算中显式地，还是在CPS-演算中隐式地，我们需要范畴[，Set]-Cat上的代数结构的非丰富版本：因此在基本层次上，我们需要考虑在[，Set ]中丰富的范畴，但是在人们可能称之为元层次的层次上，我们需要考虑在[，Set]上的非丰富结构。[→，设置]-猫。在计算细节时，研究Freyd等基本示例更容易-分类使用2-categories。在[，Set]-Cat作为2-范畴上的任何Cat-丰富代数结构平凡地产生在[，Set]-Cat作为普通范畴上的非丰富代数结构.因此，也许与直觉相反，[，Set]-Cat上的普通代数结构比[，Set]-Cat上的2-范畴代数结构要多。由于基本的例子是2-范畴的，并且用这些术语可以表达得更简单，我们将用2-范畴术语给出这一节的细节，并说明下面所有的内容都可以毫不费力地扩展到非丰富的代数结构。设C表示2-范畴[，Set]-Cat，设Cf是有限可表示的[，Set]-范畴的完全子2-范畴（我们只需要注意这些包括有限的这样），并设ob Cf表示该范畴的对象集合，即，[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19][10][11][10下面是[25]的工作的一个完全例行的变体，而[25]又是[13]的一个特例（另见[26]）。定义4.1 C上的签名是2-函子S：ob C fC，把ob C f看作离散的2-范畴.对任意c∈obCf，S（c）称为元的基本运算的[→，Set]-范畴C. 使用S，我们构造Sω：Cf−→C如下：S0=J， Cf在C的包含Sn+1=J+d∈obCfC（d，Sn（−））×S（d），290J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281ΣΣ.联系我们n nn定义σ0：S0−→S1被引入：J−→J+d∈ob CfC（d，S0（−））×S（d）σn=J+d∈obCfC（d，σn−1（−））×S（d）：Sn−→Sn+1S ω= colim n< ωSn。上极限的存在是因为C是余完备的，并且它是以C为基的函子范畴中的上极限。在许多有趣的情况下，每个σn都是单态的，所以Sω是Snn ω的并集。对于每个c，我们称Sω（c）为导出c元运算的[，Set]-范畴.签名通常伴随有导出操作之间的等式。所以我们说定义4.2带有签名S的代数理论的方程由2-函子E：ob Cf− →C和2-自然变换τ1，τ2：E−→Sω（K（−））给出，其中K：obCf−→Cf是包含。定义4.3C上的代数结构由签名S和方程（E，τ1，τ2）组成。我们通常用（S，E）表示代数结构，其中省略了τ1和τ2。现在我们定义一个给定代数结构的代数定义4.4给定一个签名S，一个S-代数由一个小[→，Set]-范畴A和一个[→，Set]-函子νc组成：C（c，A）−→C（S（c），A），对于每个c因此，S-代数由载体A和签名的基本运算的解释组成。这种解释规范地扩展到导出运算，给出一个Sω（K（−））-代数，如下所示：ν0：C（c，A）−→C（S0（c），A）是身份;利用C（-，A）向极限发送上极限的事实，给出νn+1：C（c，A）-→C（Sn+1（c），A），就是给出一个[→，Set]-函子C（c，A）-→C（c，A），我们将使其恒等，并且对于obCf中的每个d，给出一个[→，Set]-函子C（c，A）−→C（C（d，Sn（c）），C（S（d），A）），或者等价地，C（c，A）×C（d，Sn（c））−→C（S（d），A），它由下式归纳给出：C（c，A）×C（d，S（c））νn×）idC（S（c），A）×C（d，S（c））com）pC（d，A） ）νC（S（d），A）定义4.5给定代数结构（S，E），（S，E）-代数是满足方程的S-代数，即，一个S-代数（A，ν），使得同意.C（c，A）ν）ωC（τ1c，A））C（Sω（Kc），A））C（E（c），A）C（τ2c，A）J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281291YQ→→→→→→→→−→−→→- − −→→→−→CC给定（S，E）-代数（A，ν）和（B，δ），我们定义homcategory（S，E）C（A，B）{C（c，−）}c∈obCf）C（C（c，A），C（c，B））C（三）{C（S（c），−）}c∈obCfvcC（C（c，A），δc）vYC（C（S（c），A）， C（S（c）， B））QcC（νc， C（S（c），B））YC（C（c，A）， C（S（c）， B））.这与我们通常对代数同态概念的普遍代数理解一致，将其内化为C。 （S，E）中的箭头（S，E），Set]-函子F：AB，对于所有有限可表示的C，F vc（ ）= δ c（F）：C（c，A）C（S（c），B），即， a [，Set]-与所有c的所有基本c进制操作交换的函子。文[13]主要结果的一个特例是：定理4.6对于[，Set ] - Cat上的代数结构（S，E），[，Set]-范畴等价于（S，E）-Alg当且仅当存在[，Set]- Cat上的有限个2-单子T使得2-范畴等价于T-Alg。例4.7令2表示两个对象上的离散[，Set]-范畴;令0表示[，Set]-范畴，其中A0和A1都由箭头范畴给出，A是恒等函子;令Cone表示[，Set]-范畴，其中A0和A1都由两个对象及其上的锥给出，A是恒等函子;令Comp表示[，Set]-范畴，其中A0和A1都由一对对象、其上的一对锥和从一个顶点到另一个顶点的中介映射给出，与投影交换，A也是恒等函子。定义S：ob C f−→C，S（2）=Cone，S（Cone）=Comp，对于所有其他的c，S（c）是空的[→，Set]-范畴。一个S-代数是一个小[，Set]-范畴A， 一 函子φ：C（2，A）C（Cone，A）和函子φ：C（Cone，A）C（Comp，A）。函子φ是把一对物体带到它的极限锥上，函子φ是取一个圆锥体，极限圆锥体和唯一的比较图。所以我们添加方程如下：我们可以添加方程分解通过 S1（2）和 S1（Cone）分别，使得φ（x）：Cone−→A沿着包含2−→Cone限制到x，并且使得Cone将锥σ：Y−→x发送到以下形式的交换图：Yσ）xX.最后，我们添加一个通过S2（2）的因式分解方程，使得对于每个x：2−→A，我们有γφ（x）=idX。292J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281→→→→→−→→把这些放在一起，设E（2）是[，Set]-范畴，其中A0和A1都由Cone +0给出，A是单位元 ， 设E（Cone）有A0和A1都由Cone+Cone给出，A是单位元，设E（c）是所有其他c的空[，Set]-范畴，定义τ1和τ2以强制方程如上所述：在大多数分量上，τ的因子通过S1（c），但对于其中一个分量，我们需要通过S2（c）因子化。因此，对于任何x：2−→A，φ（x）是一个极限锥：给定任何锥σ：Y−→x，图φ（σ）提供一个比较映射;给定任何比较映射f：Y−→X，φ的函子性应用于箭头Yσ）xf idxv）v在C（Cone，A）中显示，X xφ（x）Yγσ）Xf idXV VX）Xγφ（x）=idX对易，所以f=γσ。一个（S，E）-代数就是一个小范畴A0，它具有指定的二元积，以及一个关于对象函子A的恒等式：A0A1。一个（S，E）-代数映射是一个[，Set]-函子，它将指定的二进制乘积发送到指定的二进制乘积。在上面观察到，我们考虑的所有有限可表示的[，Set]-范畴都有A0=A1，其中A是单位函子。 这不是巧合 事实上，人们可以用上述观察来证明定理4.8设T是Cat上的任意无穷单子。则存在[→，Set]-Cat上的无穷单子Tj，其中TJ-代数由一个T-代数（A0，a）和一个关于对象函子A的恒等式组成：A0−→A1。这一结果使我们能够扩展已知的例子范畴的代数结构给[，集]范畴的代数结构，提供我们唯一关心的是与结构上的A0。J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281293→→→→→→→−→→→→ → →→−→−→→−→一些具有代数结构的范畴的例子通常扩展了上面的例子，比如具有有限乘积的小范畴、具有有限余积的小范畴、小么半群范畴和小对称么半群范畴。如上所述，如果我们去掉Cat中的富集，我们就可以解释指数。代数结构（S，E）的另一个例子是，（S，E）-代数是一个小范畴，在它上面有一个单子。例如，对于内函子，如果c=1，则S（c）= 1，否则使其为空，没有方程。这给了我们Freyd-范畴和扩张的部分结构，例如FPC模型中的有限余积。 然而，所有的示范结构到目前为止都是在A0上构造，所以我们需要考虑A1上的非平凡结构。定理4.9在[，Set ] - Cat上存在一个代数结构，使得一个代数是一个小的premonoidal范畴A1和一个monoidal范畴A0，并且在对象严格premonoidal函子A上有一个恒等式：A0−→A1。证据 扩展例4.7的符号，令 表示[ ，集合]-类别 有两个物体，从第一个箭头到第二个箭头在A1中，A0是离散的。 回想一下，我们让0表示[，集合]-具有两个对象的类别，在A0和A1中从一个到另一个的箭头。 设1表示具有一个对象的离散[→，Set让 A：A0A1是任意的小[ ，集合]-类别。 后来那只猫-埃格里[ ，Set]-Cat（1，A）同构于A0。此外，类别的对象[，Set]-Cat（，A）是A1的箭头，箭头是A0中的一对箭头，它们与域和上域一起形成A1中的交换正方形。类别[，Set]-Cat（0，A）忠实地映射到[，Set]-Cat（，A），并由A0的箭头给出。所以如果我们把• S（1+ →）=→，• S（→+1）=→，并且• S（c）=0对于所有其他c，那么一个S-代数将由一个[，Set]-范畴A：A0A1，以及每个对象X的函子h X：A1A1和k X：A1A1的数据，以及A0中每个映射的相应数据组成，服从迫使A 0中每个映射为中心的自然条件。我们可以通过操作和方程来扩展S，以迫使上述数据给A1一个binoidal范畴的结构：我们需要确保两个函子的目标函数被很好地定义，并且按照binoidal定义的要求一致，并且保持组合和恒等式。因此，例如我们设E（2）= 1，定义τ1和τ2，使h X（Y）= k Y（X）;对于h X和k X的合成和恒等式也是如此;我们必须扩展签名S，并添加更多的方程，以给出预幺半群范畴的结构同构，但这些是沿着例4.7的思路给出的，扩展了幺半群范畴的代数结构。 这样，A0的图像被迫位于A 1的中心。然后，可以例行地将运算和方程添加到294J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281→→→→→→→→→给出凝聚结构同构a，l和r，使得A1是预幺半群. Q结合例4.7和定理4.9的构造，我们有推论4.10在[ ，集合]-猫， 是一个很小的Freyd类别。我们几乎完全用术语来表达这一节的技术细节 2-范畴的代数结构。闭Freyd-范畴不包括在其中，就像在Cat上的代数结构不能给出Carnival闭范畴一样，Cat被看作是2-范畴[13]：原因是闭结构是逆变的，而Cat-富集需要协变性，就像在上面的所有例子中一样。但是，正如Carnival闭范畴是由作为普通范畴的Cat上的代数结构给出的[13，25]，闭Freyd-范畴是由作为普通范畴的[，Set]-Cat上的代数结构给出的，参见[26]，这是一个例行的证明，尽管是Carnival范畴闭性证明的仔细扩展。总结一下，我们有推论4.11在[，Set]-Cat上存在代数结构，它被看作是一个普通范畴，对它来说一个代数是一个小的闭Freyd-范畴。这些结果提示我们考虑具有代数结构的[，Set]-范畴 作为提供按值调用语言的语义的一种方式。人们可以使用丰富范畴理论的结果来做到这一点。例如，[，Set]是一个[，Set]-范畴，并且在普通范畴论中扮演着与Set相似的角色，因此可以说是预层、自由余补等。此外，[，Set]-Cat是一个局部有限可表示的2-范畴，因此人们可以接触到2-单子的理论，特别是对只在相干同构之前保持结构的函子的处理。特别地，对于[，Set]-Cat上的任意单子T和任意[，Set]-范畴A，都有A上的自由T-代数。由于我们的各种语言的模型是采取T-代数，这一事实使我们能够给一个类别理论帐户的语言所产生的签名。我们将在下一节中对此进行阐述。5建模签名本文中的签名有两种不同的概念。我们在第4节中介绍了一个这样的概念，与相关文献一致。另一个，与不同的文学作品相一致，是由基本类型和表达式给出的，按值调用编程语言的精神第2节。在这一节中，我们用范畴论的术语解释了后一种意义上的签名、由签名生成的语言和模型的概念。这方面的关键概念是T-草图S，草图的理论Th（S），以及T-草图的模型，对于[→，Set]-Cat上的给定的有限单子T。编程语言可以通过签名自由地生成，即，基本数据类型和基本表达式。 关于这个概念的最新描述和使用，见[14]。 为一个范畴理论公式的概念的签名，我们给，任何有限J. 动力MTanaka/Electronic Notes in Theoretical Computer Science 225（2009）281295→→→→→S −→ SS→DS→SD→−→−→−→我[，Set]-Cat上的monadT，T-sketch的一个概念，我们将其与签名T的概念等同起来。 然后我们证明每个T-草图 生成自由模型i：Th（）。自由模型Th（）表示由签名Th（）生成的编程语言。我们首先需要一个补充定义。 虽然这是第一个定义， 这一节，它不被视为具有核心重要性，正如概念binoidal范畴的概念是对premonoidal范畴概念的补充就像在上一节中一样，领先的例子更容易用2-monads而不是普通的monads来表示：回想一下，[，Set]-Cat上的2-monads有底层的普通monads，所以充实相当于一个限制，但它包括了我们的领先例子。 所以为了方便我们表达自己根据2-monad：根据普通monad的例子的描述是例行的，但乏味。定义5.1给定[，Set]-Cat上的有限个2-monadT，一个图类型族是一个4-元组的小族（ci，di，ji：cidi，ki：diTci），其中ci和di是有限可表示的[，Set]-范畴，ji和ki都是[，Set]-函子，条件是下面的图交换：dki）TcCi我们通常会抑制ji和ki，让它们隐含在ci和di中，就像我们经常用对象集来指代一个类别，而其余