《从余模到余代数：探索Lawvere理论生成的comonads的新结构与张量积》

理论计算机科学电子笔记106（2004）297-314www.elsevier.com/locate/entcs从余模到余代数：状态与数组John Power约翰·鲍尔1，2苏格兰爱丁堡大学信息学系Olha Shkaravska Olha Shkaravska3，4德国慕尼黑路德维希-马克西米利安大学信息学院TCS摘要我们调查的概念，一个（可数）Lawvere理论，一个明显的对偶模型的概念。通过把余模范畴中的遗忘函子取到Set上，每一个（可数）Lawvere理论都生成一个Set上的余模。但是，虽然Lawvere理论等价于Set上的无穷单子，并且该结果扩展到更高的基数，但对于comonads没有这样的结果，这不仅仅是因为大小的原因：这主要是因为，虽然Set是carnival封闭的，但Setop不是。所以每个在Set上有秩的单子都在Set上生成一个comonad，但反之亦然。我们的主要例子是可数的Lawvere理论的整体状态：其范畴的余模是类别的数组，产生一个精确的关系之间的整体状态和数组。从任意的comonads限制到由Lawvere理论生成的comonads，研究新的和有趣的结构，特别是张量积。关键词：Lawvere理论，（余）模型，（余）代数，（余）单子，范畴等价，整体状态，数组。1这项工作得到了EPSRC基金GR/N64571、EPSRC基金GR/586372/01和AIST Japan的支持2电子邮件地址：mailto:ajp@inf.ed.ac.uk3这项工作得到监测和报告小组项目（IST-2001-33149）的支持，该项目由欧盟委员会根据FET全球计算主动倡议提供资金4Email：mailto：shkarav@ tc s.i nf orm at ik. uni-mue nc h e n.de1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.041298J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297VVVVV−→1介绍给出一个Lawvere理论L等价于给出集合[1]上的一个无穷单子T。 更一般地说，对于任何局部有限可表示的类别， 作为一个对称monoidal闭范畴，我们可以定义一个LawvereV-理论L的概念，并证明给出一个LawvereV-理论等价于给出[16 ]第16话：一个V的单子T 人们可以常规地将这种等价性扩展到高等基数，特别是定义了可数LawvereV-理论的概念，对于任何V是局部可数可表示为对称monoidal闭范畴，并证明了给出可数LawvereV-理论等价于给出V上可数秩的V-单子T 在特定情况下，是Carnival闭范畴ωCpo，有被证明是至关重要的，在给一个统一的理论，如何结合计算效果[9，10]。形式上，我们可以通过放弃尺寸条件[4]来进一步扩展结果：对于任意对称monoidal，闭范畴V，给出一个广义的LawvereV-理论等价于给出一个任意单子。虽然优雅，结果是有限的实用价值，因为人们可以不再自由地考虑理论的总和，或张量或理论，或类似的[8]。 所以，形式上，所有的V-单子都可以是其特点是丰富了Lawvere任意基数理论的概念但实际上，在存在大小限制的情况下，结果最令人感兴趣。对于余代数的工作者来说，一个直接的问题是：当一个monad被一个comonad取代时正如上文所述，图，答案并不简单：所有上述结果都依赖于对称monoidal闭，但即使Setop具有有限乘积结构，即，集合的有限余积结构不是封闭的。因此，上述结果的最实质部分是不成立的.这种崩溃进一步表明了许多最近的结果，给出了余代数的语法，例如[5，6]，因为语法总是基于某种比用有限余积结构代替有限积结构的常规方法复杂得多的东西。但这并不意味着这里没有什么有趣的东西要说：虽然在余积和基于有限余积的理论的自然概念之间不存在等价，但存在一个推定等价的方向，包括大量的例子，并支持一个数学理论体系。定义一个与Lawvere理论的概念相对应的对偶是微不足道的。一个Lawvere理论由一个小范畴L和一个在对象上保持同一性的严格有限积函子J：N atopL组成，其中N at是有限集范畴的骨架。N atop可以刻画为在1上有有限乘积的自由范畴。因此，Lawvere余理论的一个明显定义是一个小范畴C，它具有有限余，J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297299−−→−→积和一个在对象上保持同一性的严格有限余积函子J：N at−→C，因为N at是在1上有有限余积的自由范畴。但是，作出这样的定义是多余的，因为要给一个Lawvereco-theory然后将完全等价于给出Lawvere理论，简单地通过应用（）op。因此，我们将不正式定义一个Lawvere共理论的概念，而是使用Lawvere理论的标准定义，定义一个在某种意义上与模型范畴的通常定义对偶的共模型范畴。对于任意有限积范畴C，一个Lawvere理论L是有限积保持函子M：LC。因此，我们定义一个Lawvere理论L在范畴C中的余模，其有限余积为：有限余积保持函子M：LopC.因此，把所有的自然变换作为箭头，我们有范畴Comod（L，C），根据定义，它同构于Mod（L，Cop）op，参见[13]。设C为Set，Comod（L，Set）包含在函子范畴[Lop，Set]中有一个右伴随，这不是完全明显的，但却是真的，因此从Comod（L，Set）到Set的健忘函子是余单进的：这是第2节的主要结果。这个结果丰富并扩展到其他基范畴，如偏序集和猫，并从有限性推广到可数性，推广到ωCpo。因此，Lawvere理论产生集合上的comonads。推广到一个固定的正则基数，可以得出每个秩在Set上的单子T都导出一个余单子：给定T，设L是相应的广义Lawvere理论，并考虑从Comod（L，Set）到Set的遗忘函子生成的余单子。从余代数的角度来看，出现了几个问题：是否有计算兴趣的从一个在Set上有秩的单子构造一个在Set上的comonad，是否会在单子和comonad之间产生一个有趣的关系？是否有关于余模范畴的有趣构造或结果，它们不一般地或可能不以同样的方式保持余代数范畴？这些结果在多大程度上从集合扩展到其他自然基范畴？这些是我们希望探讨的一些问题，答案通常是肯定的。我们领先的例子一类的余模是，数组，与单子之间的关系，为全球的状态和comonad的数组是由上述建设：我们分析了可数Lawvere理论，因此单子，为全球的状态在第3节，我们分析了数组在第4节。 当然，数组的概念已经存在了几十年，参见实例[3，14]。给定一个位置的有限集合Loc和一个值的可数集合V，一个（Loc，V）-数组可以公理化为一个集合A和函数sel：A×Loc−→V300J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297和upd：A×Loc×V−→A满足四个公理模式，我们在第4节中列出，参见[7，17]。数组自然地形成一个范畴（Loc，V）-Array，并且可以很容易地检查到（Loc，V）-Array是可数Lawvere理论LLoc，V的全局状态的余模的范畴：我们在第3节中描述LLoc，V，并在第4节中给出与数组的关系的证明。证明的技术核心是在Loc有一个元素的情况下重新表述和推广了Hofmann和Pierce的一个结果[7]。限制注意力从任意comonads到那些产生于协同模型的Lawvere理论，使我们能够挖掘到现存的身体知识的边缘。特别是，我们可以说的总和，尤其是张量积的理论[9，10]。求和得到诱导的共单子的乘积。的张量积具有万有性质Comod（L<$LJ，C）<$Comod（L，Comod（LJ，C））这是一个真正的理论上的构造，而不是在余代数上的构造：它涉及L在余模（LJ，C）中的余模，这不等价于一个余代数提升到另一个余代数的范畴，参见[9，10]。我们在第五节中简要地概述一下情况。对于进一步的工作，我们应该非常希望能够对那些由comodel类别产生的comonad进行分类，至少在Set上是这样。但这看起来是个非常棘手的问题。人们能够现实地寻求的最好的可能是关于表示的条件，其中一些在第2节中是隐含的。我们还想更多地探索这个例子，因为它从全局状态/数组扩展到了变量 。 我 们 希 望 通 过 限 制 于 由 comodels 生 成 的 那 些 ， 来 探 索 更 多 可 以 在comonads上进行的构造的意义。2从余模到余代数在这一节中，我们定义了Lawvere理论的余模概念，并证明了Lawvere理论的集合中的余模范畴是集合上的余模范畴。这一节的结果例行地丰富到那些局部有限地可表示为Carnival闭范畴的范畴，并且可以被推广也经常在大小方面，特别是可数Lawvere理论的概念，这是[9，10]的焦点，并且为了解释ωCpo而需要。但是，为了简化说明，在本节中，我们将把注意力限制在Lawvere理论的通常概念上，即，其中对象是自然数，对应于集合上的无穷单子。J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297301−→×−−→设Nat表示由自然数给定的集合的全子范畴。因此，它包含一个对象n，每个自然数，映射都是这些自然数之间的函数。范畴Nat有由自然数之和给出的有限余积。定义2.1一个Lawvere理论由一个具有有限积的范畴L和一个在对象上同一的严格有限积保持函子组成J：N atop−→L.范畴C中的L的有限积模型是从L到C的有限积保持函子。范畴C中L的具有有限余积的余模是从Lop到C的有限余积保持函子。L在范畴C中的有限积模型形成范畴Mod（L，C），其箭头由所有自然变换给出。 L在范畴C中的余模与有限余积形成范畴Comod（L，C），其箭头由所有自然变换给出。因此，几乎根据定义，对于任何具有有限余积的范畴C，我们有：Comod（L，C）n=Mod（L，C op）op给定一个Lawvere理论L，遗忘函子U：Mod（L，Set）设置有一个左伴随，显示Mod（L，Set）作为集合上的有限一元。这个结果例行地从Set推广到任意局部有限可表示范畴C。但是Setop不是局部可表示的，所以我们需要更细致地证明从Comod（L，Set）到Set的遗忘函子有一个右伴随，或者等价地证明从Mod（L，Setop）到Setop的遗忘函子有一个左伴随，参见[12，13]。定理2.2对任何Lawvere理论L，U：Comod（L，Set）−→Set有一个右伴随，显示Comod（L，Set）作为集合上的余单进。证据右伴随存在的断言等价于Comod（L，Set）包含到[Lop，Set]中有右伴随的断言。 对于这一点，关键点是，对于任何自然数n，函子n：设置Set将集合X发送到X的副本的n重余积，并且 它保持了ω-上链的极限。给 定 一 个 函 子 H ： Lop−→Set ， 存 在 一 个 标 准 映 射 φn ： n×H1−→H（n×1）。L中f：n−→1形式的映射由H 发送到函数Hf：H1−→H（n×1）。所以我们需要沿φn拉回Hf。我们需要对L中的所有映射同时这样做，得到一个极限H11和一个函数σ1：H11−→H 1。一般来说，H1不会延伸到302J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297−→有限余积保持函子，因为n×σ1：n×H11−→n×H 1但是我们可以继续归纳地建立一个长度为ω的上链：在定义H21时，我们还必须考虑L中的等式，即，给定f：n−→ 1和gi：ni−→ 1，其中1 ≤i≤n，必须考虑f（g1，···，gn）。但是在定义了H21之后，扩展到所有n是例行的。 在极限中，Hω是函子的，因为可以通过使用由n×σk给出的上链的极限性质来定义H ω f。证明Hω是右伴随是常规的。对于共单子性，验证贝克单子性定理的对偶的条件是常规的，即，U是同构，分裂均衡器提升了[1]。Q注意，这里使用的中心点是Set的carnival闭性：我们使用了这样一个事实，即n的张量与X具有以下普适性质：一种产品。由此可见，我们可以将这个结果推广到诸如Poset、Cat和ωCpo的范畴，并且它也推广到受大小约束的Carnival闭范畴中的富集，包括诸如Poset、ωCpo和Cat的范畴。我们在此仅作评论，不作进一步探讨对我们来说，一类余模型的主要例子是数组的概念，如第4节所研究的。因此，我们在这里不想多举例子。但是，为了让我们对这里所涉及的comonads有一个概念，我们举两个例子。例2.3考虑由一个n元运算生成的Lawvere理论Ln，即，由映射n自由生成的1. 集合Ln的一个余模由集合X和一个函数X−→A ×X其中A的基数为n。正如我们将在下一节中概述的那样，从n的有限性进行概括是直截了当的。例2.4考虑由B个一元运算产生的Lawvere理论LB由B映射1−→ 1自由生成。集合中的LB余模由集合X和函数XX−→XB上面的例子特别简单，因为它们不涉及非平凡方程. 但他们确实给出了一个概念，我们的主要例子在第4节。注意，似乎没有办法包括涉及powerset的示例J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297303ℵℵℵ1opℵ×3全球状态的可数Lawvere理论在前一节中，我们开始发展一个律维理论的余模的概念及其导出的余模。为了说明的简单，我们使用了通常的Lawvere理论的概念，同时指出更大的普遍性是可能的。事实上，我们的主要例子是一个可数的Lawvere理论，而不是一个普通的理论;因此，我们在这里首先简要说明上面的主要定义是如何从有限性扩展到可数性的。在本节中，我们定义并研究了全局状态的可数Lawvere理论。可数的Lawvere理论隐含在[15]中，但是那篇论文没有明确提到Lawvere理论的任何概念，从那篇论文中的解释到理论并不是完全微不足道的，并且描述可数的Lawvere理论的论文并没有详细包含这个例子[9，10]。设1表示由可数集给出的Set因此，在等价的情况下，它包含一个对象n来表示每个自然数，以及一个对象0来表示一个可数集。第1类有可数余积。定义3.1可数Lawvere理论由具有可数乘积的范畴L和保持函子J的关于对象的恒等式严格可数乘积组成：可数范畴C中L的一个模型乘积是从L到C的可数乘积保持函子。范畴C中L的可数乘积模型构成范畴Mod（L，C），其箭头由所有自然变换给出。我们假设给定一个位置的有限集合Loc和一个值的可数集合V我们将Loc等同于由其基数给出的自然数，将V等同于0。当我们写乘积X Y时，我们指的是集合的乘积，而不是可数Lawvere理论L中的乘积，后者由集合的余积给 出 。 给 定 L 中 的 一 个 映 射 ， 比 如 f ： Y−→YJ ， 当 我 们 写 X×f ：X×Y−→X×YJ时，我们指的是L中由f的X个副本的乘积给出的映射。这是一个特别方便的符号但它需要相当的小心：有一种明显的方法，使用对称性来定义f×X，但×甚至不是monoidal，即，给定g：X−→XJ，304J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297×1ℵ1f：Y−→YJ，图X×YX×f）X×YJg×Yvg×YJvXJ×Y）XJ YJXJ×f不需要对易，除非f或g之一位于op的像中，参见[11]。 如果有任何疑问，通常有助于考虑图对Set中的模型的意义，因为×被模型发送到指数[15]。定义3.2全局态的可数Lawvere理论LLoc，V是由映射l：V−→Locu：1−→Loc×V以下列图表的可交换性为准。首先，我们有如下四个交互图：1u）Loc×Vt位置×lV V位置（位置×位置δ其中δ：Loc−→Loc×Loc和t：Loc−→1是图1中的对角和终端映射（因此必须颠倒才能被认为是图1中的映射），V×VV×）lV×Locl×Lo）cLoc×Locδ δV VV） LocLJ. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297305×=×21u）Loc×VLoc×V×）uLoc×V×Loc×Vu Loc×s ×VvLoc×V1000×1000×1000× 1000（vLoc×Loc×V×V位置×π1δ ×V ×V和Vl ）LocLoc×）uLoc×Loc×VV×uvδ×VvV×Loc ×V）LocVLoc×δ抑制两个同构。我们也有如下三个换向图V×VV×）lV×Loc=）Loc×VLoc×）lLoc×LocS sV VV×VV×lLoc×LocvV×LocV）Loc×Vv）Loc Loc ）Loc Loc×l其中s表示对称性，Loc2表示Loc的不同元素的有序对的集合，其中未标记的映射都由相同的正则映射给出，306J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297× ××21u）Loc×VLoc×V×）uLoc×V×Loc×Vu sV VLoc×VLoc×V ×uvLoc×V×Loc×VvLoc×V ×Loc ×V2×V×V其中s再次表示对称性，并且无标号映射再次由相同的正则映射给出，并且Vl）LocLoc×）uLoc×Loc×VV×u=V VV×Loc×V=Loc×V×LocvLoc×V ×Vv）Loc V Loc）LocVLoc×V×l其中，同样，未标号映射由相同的正则映射给出命题3.3图解1吨）\\\l在L通勤。t\ \vLocJ. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297307−→S证据使用第一个公理的两个应用和第二个公理的一个应用。Q下面的定理，以稍微不同但等价的术语陈述，是[15]的第一个主要定理定理3.4对任何具有可数乘积和可数余积的范畴C，遗忘函子U：Mod（LLoc，V，C）−→ C表现范畴Mod（LLoc ， V，C）为C上的单子，具有单子（S<$−），其中S是集合VLoc，S<$X是X的S个副本的余积。我们在这里不重复证明，但我们做了一些评论，以便于我们在下一节中与数组进行比较。 首先观察到这个结果对任意具有可数乘积和可数余积的范畴C成立。因此，它对Setop和Set同样适用：我们需要前者来处理数组。定理3.4允许我们解释为什么我们称LLoc，V为整体状态的可数Lawvere理论。取C=Set，导出的单子是全局状态或边对象的单子[15]。考虑1上的自由代数。它的形式为A =（SS，lookup，update），并键入lookup：|一|V −→|一|Loc更新：|一| −→ |一|Loc×V。 函数lookup发送一个计算c∈|一|V 对于计算cJ∈|一|Loc由CJ（loc）（σ）令v=sel（σ，loc）inc（v）（σ）其中sel（σ，loc）=σ（loc）在状态σ中查找loc。类似地，函数update发送计算c∈|一|对于计算cJ∈|一|Loc×V由下式给出：其中upd（σ，loc，v）用v更新位置loc中的状态σ。左伴随的结构一般由以下命题给出Sition，cf [15].命题3.5遗忘函子U的左伴随：Mod（LLoc，V，C）−→C将C的对象X与映射一起发送给对象（SX）Su：（S<$X）S−→（（S<$X）S）Loc×V由函数的组成决定Loc×V ×VLoc −→VLoc给定（loc，v，σ），通过将其在loc处的值替换为v和l：（（S<$X）S）V−→（（S<$X）S）Loc308J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297−→由函数的组成决定Loc×VLoc −→V ×VLoc即，给定（loc，σ），在σ：Loc V中“查找”loc以确定其值，并且通过到VLoc的投影给出。对于任何可数的Lawvere理论，人们都可以例行地给出一种等式语言，对于这种语言，语言的无穷项之间的等式对应于理论中的交换图。因此，为了与下一节中的数组进行进一步比较，定义LLoc，V中的七个交换图可以用等式表示为以下七个公理，分别涉及无穷表达式：(i) lloc（（uloc，v（a））v）=a(ii) lloc（（lloc（（avvJ）v））vJ）=lloc（（avv）v）(iii) uloc，v（uloc，vJ（a））=uloc，vJ（a）(iv) uloc，v（lloc（（av）v））=uloc，v（av）(v) lloc（（llocJ（（avvJ）vJ））v）=llocJ（（lloc（（avvJ）v））vJ）其中loc=/locJ(vi) uloc，v（ulocJ，vJ（a））=ulocJ，vJ（uloc，v（a））其中locj=locJ(vii) uloc，v（llocJ（（avJ）vJ））=llocJ（（uloc，v（avJ））vJ）其中loc locJ.4阵列在本节中，我们定义并研究数组范畴的结构，特别是证明对于给定的有限集Loc和可数集V的（Loc，V）-数组范畴等价于我们在前一节中为全局状态定义的可数Lawvere理论LLoc，V的在给出数组的公理化定义时，我们遵循并温和地推广了[3，7，14，17]中的数组方法定义4.1给定位置的有限集合Loc和值的集合V，（Loc，V）-数组由集合A和函数组成sel：A×Loc−→V和upd：A×Loc×V−→A受以下四个图的交换性的限制：J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297309A×Loc×V）A×Loc×V×LocπVupd×LocV VV（selA×Loc其中，无标号映射由对角线δLoc确定：Loc−→Loc×Loc和对称性，A×Loc）A × Loc × A × LocπAA×Loc ×selV V（UPDA×Loc×V其中，无标号映射由对角线δA×Loc确定：A×Loc−→A×Loc×A×Loc和对称性，A×Loc×V×V）A×Loc×V×Loc×Vupd×Loc×V）A×Loc×VA×Loc ×t ×VvUPDvA×Loc ×V）AUPD其中，无标号映射由对角δLoc给出：Loc−→Loc×Loc310J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297−→以及对称性，以及A×Loc2×V×V）A×Loc×V×Loc×Vupd×Loc ×VvA×Loc×V×Loc×VA×svA×Loc×V×Loc×Vupd×Loc ×VvA×Loc×VUPDvA×Loc ×Vv）Aupd其中两个未标号的映射是相同的，都是由Loc2正则包含到Loc×Loc中确定的，其中s表示Loc×V的正则对称性。这些公理同样可以写成项与项之间的方程。映射sel和upd是函数，所以这四个公理可以表示如下：对于Loc中的loc和locJ，对于V中的v和vJ，以及对于A中的a，(i) sel（upd（a，loc，v），loc）=v(ii) upd（a，loc，sel（a，loc））=a(iii) upd（upd（a，loc，v），loc，vJ）=upd（a，loc，vJ）(iv) upd（upd（a，loc，v），locJ，vJ）=upd（upd（a，locJ，vJ），loc，v）其中locLOC J有一个明显的概念，从（A，sel，upd）到（AJ，selJ，updJ）的数组映射，即函数h：A AJ，它使明显的两个图互换。这就产生了一个类别（Loc，V）-Array。数组的定义和我们在第3节中描述的Lawvere理论LLoc，V之间的关系并不完全是微不足道的。最明显的不同之处是前者有四个公理，而后者有七个，其次最明显的不同之处是，如果考虑u和l的n，很明显u匹配upd，但l不匹配sel。另一方面，四个数组公理与四个全局状态公理非常相似，并且给出一个函数sel：A×Loc−→V等价于给出一个J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297311VLoc×RAasV（a）=（第1（a）条，. ，seln（a）），upd（a，−）函数selJ：A×Loc−→A×V服从公理A×Locsel）J\\A×VA×Locsel）J\\A×V\πA\πVπA\v一选择\vV因此，先验地，有充分的理由希望阵列是可数Lawvere理论的全局状态的余模。我们继续给出一种方法来证明这一点，在途中展示一些副结果。命题4.2从Set到（Loc，V）的函子-数组发送一个集合R到VLoc×R的结构图VLoc×R ×Loc −→V和VLoc×R ×Loc ×V −→VLoc ×R由评价和更新给出的，是范畴的等价证据证明命题陈述中给出的结构映射满足我们的数组公理是很简单的。对于逆，首先观察到，对于任何数组（A，sel，upd），存在一个规范函数upd：A×VLoc−→A由一系列Loc给出的upd的许多应用：将Loc ={1，. ，n}upd（a，v1，. ，vn）=updn（updn−1（.. . ），vn，n）现在，给定一个数组（A，upd，sel），定义RA为所有函数的集合，VLoctoA的形式upd（a，−）：VLoc−→A这是一个平凡的集合。 我们需要从集合VLoc×RA到A，并证明i.这涉及到UPD和SEL。Weedefineabubijection：A−→.使用公理1可以证明SEL和UPD受到尊重。Q这个命题实质上是对[7]中一个结果的重新表述和推广，它实质上相当于Loc是一个单元素集的情况。它也与[15]中定理3.4的证明具有显著的而非巧合的相似性：对于该证明，我们需要在u上构造一个基本上与我们在这里所做的相同的312J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297−×−−→−→Loc我们还需要对L进行这样的构造，但是这里，我们根据SEL而不是SELJ的公式使其隐含，如以下结果所示。命题4.3对于任何非空集X，函子−×X：设置−→设置是余单子的，余单子由（−）X× X给出。证据函子X有一个由（）X给出的右伴随。由于X是非空的，它也反映同构。 这是例行检查它保留了均衡器。因此，根据Beck的一元性定理的对偶Q结合这两个命题，我们可以得出本节的主要结果。定理4.4从（Loc，V）-数组到集合的遗忘函子是集合上的余单子，余单子由（−）V×V Loc给出。范畴Setop有可数乘积和可数余积，乘积由Set的余积给出，余积由Set的乘积给出。因此，结合定理3.4和定理4.4，我们得到以下结果。推论4.5设LLoc，V是整体态的可数Lawvere理论。所以Comod（LLoc，V，Set）等价于（Loc，V）-Array。5结构：sum和tensor最后，在这一节中，我们非常简单地描述了一些理论价值，这些价值来自于从Set上的任意comonads到由comodels生成的comonads的限制。我们把数组的例子作为最好的例子，我们认为全局状态和数组之间的关系本质上是有趣的。但在抽象的技术层面上，我们可以说得更多Lawvere理论的和与张量积的概念已经存在了几十年，但最近的解释和参考文献出现在[9，10]中。命题5.1Lawvere理论L和Lj的和L + LJ的特征在于普适性质，即在任何具有有限乘积的范畴C中给出一个L + LJ的模型等价于给出一个L的模型和一个Lj的模型，当沿着J：N限制在opL和JJ：N限制在opJ是相等的。J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297313⊗这种普遍属性可以用comonads 来描述。由此可以立即得出结论，Lawvere理论的总和对应于由每个理论生成的comonads的乘积。张量更有趣：它产生的构造在考虑comonads时似乎不是一个自然的构造。命题5.2Lawvere理论的张量积L LJMod（L，Mod（LJ，C））Mod（L<$LJ，C）对于任何C类有限产品。这就产生了以下关于共模型的结果。推论5.3Lawvere理论的张量积L<$Lj的Comod（L，Comod（LJ，C））<$Comod（L<$LJ，C）对于任何有有限余积的C类注意，这涉及到在范畴Comod（LJ，C）中而不是在C中取L的模型。一般来说，这种提升不是由分配律给出的，comonads：参见[9，10]对双重情况的分析。因此，相对于余代数的已知工作，这似乎是关于余模型的一个真正的新构造。我们还没有探讨它的意义。引用[1] Barr，M.，和C. Wells，[2] 布莱克威尔河，通用汽车陈文辉，二维单子理论，中国科学院学报，2001，（4）：117 -118[3] 柯林斯·G和D. Syme，“有限映射理论”，Proc.8th高阶逻辑定理证明及其应用国际研讨会，编辑。E.T. Schubert，P.J. Windley and J. Alves-Foss，Lecture Notes in ComputerScience971，Springer-Verlag，1995.[4] Dubuc，E.，145，Springer-Verlag，1970.[5] 加尼，N.，C. Luth ，F.de Marchi和A.J.Power，Algebras，Coalgebras，Monads andComonads ， Proc.CMCS 2001 ， Electronic Notes in Theoretical Computer Science44（2001），网址：http://www.elsevier.com/locate/entcs/volume44.html的网站 。[6] 加 尼 ， N. ， C. Luth ， F.de Marchi 和 A.J.Power ， Dualising Initial Algebras ，Mathematical Structures in Computer Science13（2003），349[7] 霍 夫 曼 ， M. ， 和 B.C. Pierce ， Positive Subtyping ， Information and Computation126（1996），11-33.[8] Hyland，M.，P.B.莱维Plotkin and A.J. Power，314J. 鲍尔，澳-地Shkaravska/电子笔记理论计算机科学106（2004）297[9] Hyland ， M. ， G.D. Plotkin 和 A.J.Power ， 李 嘉 图 Baeza- Yates ， Ugo Montanari andNicola Santoro，Kluwer，2002.[10] Hyland，M.，G.D. Plotkin和A.J. Power，组合效应：总和和张量，理论计算机科学，即将出版。[11] Hyland，M.，和A.J.Power，PPDP 2000，ACM，2000年。[12] 凯利，通用汽车，自由代数、自由幺半群、上极限、相关层等的transfinite构造的统一处理，Bull.Austral.Math.Soc.22（1980），1[13] 凯利，通用汽车，《丰富范畴理论的基本概念》，剑桥大学出版社，1982年。[14] Oles，F.，“类型代数，函子范畴和块结构”，语义学中的代数方法，编辑。MauriceNivat和John C. Reynolds，Cambridge University Press，1985.[15] Plotkin，G. D.，和A. J. Power，[16] 鲍尔，AJ “Enriched Lawvere Theories”, Theory and Applications[17] Stump，A.，C.W.巴雷特，D.L.李国忠，“一种新的矩阵理论与方法”，国立成功大学计算机科学研究所硕士论文，2001年。