代数运算理论：范畴C上的单子T模型化计算语义，等价定理支持公理定义

332−→理论计算机科学电子笔记45（2001）网址：http://www.elsevier.nl/locate/entcs/volume45.html14页代数运算Gordon Plotkin和John Power1爱丁堡大学计算机科学基础实验室King摘要给定一个具有有限乘积的范畴C和C上的一个强单子T，我们研究了如下形式的ObC-索引运算族的公理：α x：（T x）nTx为添加到计算λ -演算的代数运算提供了定义语义。我们回忆起一个定义，我们在其他地方给出了大步长和小步操作语义的充分性结果，我们证明了它等价于代数运算的一系列其他可能的自然定义我们概述了例子和非例子，我们表明，我们的定义是等价的一个调用的名称语言与效果了。1介绍Eugenio Moggi在[6，8]中引入了这样一种思想，即通过在Kleisli范畴中为具有有限乘积的基范畴C上的适当强单子统一建模，为诸如非确定性、概率非确定性、副效应和例外等计算效应给出统一的范畴他通过发展计算λ-演算或λc-演算来支持这一结构，λ-演算提供了一个健全而完整的模型类。计算λ-演算与简单类型λ-演算基本相同，除了使在计算和数值之间仔细系统的区分。然而，它不包含操作，而操作对于任何编程语言都是必不可少的.因此，在这里，在开始解决这个问题时，我们为代数运算提供了一个统一的语义，由等价定理支持，以表明公理的定义性。1这项工作得到了EPSRC基金GR/L 89532的支持：电子数据库。2000年1月，出版社dbyElsevierScienceB。 V. 在CC BY-NC-ND许可下开放访问。情节与权力333我们在这里区分代数运算和任意运算。在某种意义上，我们将精确地说，前者是通常运算的一种自然概括，从Set到具有有限乘积的任意范畴C 泛代数关键是，αx：（T x）n−→Tx是Kleisli范畴中的参数自然的强单子TC，正如定义2.1中所精确描述的那样：在这种情况下，我们说单子T支持操作;领先的例子类有T被生成的操作受到方程伴随他们。 示例 这些操作中的一个是用于非确定性和概率非确定性的操作，以及用于引发异常的操作。一个非示例由处理异常的操作给出。在另一篇论文[11]中，我们给出了上述定义，并给出了计算λ-演算的语法对应，证明了小步长和大步长操作语义的充分性结果。但是，这样的结果本身就为精确选择适当的语义公理留下了一定的空间因此，在本文中，我们证明了一系列等价结果，我们相信这些结果为公理的特定选择提供了强有力的证据，即上述Kleisli范畴中的参数自然性。我们最深刻的结果本质上是关于有限单子和Lawvere理论之间的对应关系从集合到具有有限乘积C和C上的强单子T的范畴的推广：这个结果将代数运算刻画为类属效应。 我们的分析的一般性略大于在[12]中对丰富的Lawvere理论的研究中：后者要求C局部有限地可表示为一个闭范畴，这对我们所有的主要例子都不是真的。Moggi在[7]中给出了一个运算概念的语义表述，并基于他的计算元语言进行了分析，但他只要求C中运算的自然性，我们不知道有什么方法可以提供如此普遍的运算语义。我们的各种表征结果似乎也没有扩展到这种普遍性。显然，进一步的工作是考虑如何模拟其他操作，如处理异常的操作。这可能涉及到超越单子，正如莫吉向我们建议的那样;一种可能性是在二分体的方向[13]。我们用一个强单子T来表述我们的论文，T是一个具有有限乘积C的范畴。我们同样可以按照[1]的精神用封闭的Freyd-范畴来表述它，[1]为我们分析有限非决定论提供了一个主要的例子。该文件的组织如下。在第2节中，我们回顾了[11]中给出的代数运算的定义，并展示了它的一些简单的重新表述。在第3节中，我们在C是闭的假设下，根据扩充给出了这些陈述的直接等价版本。在第4节中，我们给出了一个更实质性的概念，在操作方面，情节与权力334×−→−×−→×Homs，无论是当C是封闭的，更一般地当C是不封闭的。在第5节中，我们给出了我们认为是本文最深刻的结果，这是一个一般效应的公式，概括了对Lawvere理论的研究。最后，在第6节中，我们用范畴T-Alg上的运算来描述代数运算，因为这给出了如何将具有计算效应的按名称调用语言纳入图像的指示。我们在第7节中给出了结论和未来可能的发展方向。2代数运算与简单等价在这一节中，我们给出了代数运算的定义在[11]中。在那篇论文中，我们给出了计算λ-演算的定义和一个句法对应物，并证明了后者的小步骤和大步骤操作语义的充分性结果。这些结果并没有孤立出代数运算概念的定义公理。因此，在本节中，我们从几个简单的等价结果开始，稍后我们将在这些结果的基础上进行构建。我们假设我们有一个范畴C，它有有限个乘积，以及C上的一个强单子，它有Kleisli指数，即，使得对于C的所有对象x和z，函子CT（x，z）：Cop Set是可表示的。我们一般不取C是闭的：对于后面的一些结果，我们将需要假定它，但我们特别不想一般地假定它，而且对于本节的任何结果，我们也不要求它给定一个映射f：yxTz在C中，我们表示f，即，复合y×Txst由f†：y×Tx−→Tz。T（y×x）Tf T 2zµz 齐兹定义2.1代数运算是一个ObC-索引映射族αx：（T x）n−→Tx使得对于C中的每个映射f：y×x−→Tz，f<$·（y×πi）y×（T x）ny×αx❄i=1 （Tz）nαz❄yTxTzf†上下班情节与权力335××−→对于一些代数运算的例子，对于C=Set，让T是具有二元选择运算的非空有限幂集单子[9，1];或者，让T是具有概率选择运算的概率非确定性单子[2，3];或者让T是具有打印运算的打印单子观察后一个例子中的非交换性。当然，我们可以从集合推广到诸如ω-cpo的范畴我们也可以考虑这些的组合，例如对内部和外部选择操作进行这些例子中有几个在[11]中详细处理。定义的相干条件有几个等价的公式。以最大化的方式分解它，我们有命题2.2ObC-指标映射族αx：（T x）n−→Tx是代数运算当且仅当(i) α在C中是自然的(ii) α尊重st，因为st·（y×πi）y×（T x）ny×αx❄i=1 （T（y×x））nαy×x❄通勤yTxT（yx）st(iii) α尊重µ，因为（T2x）nnx（T x）nαTxαx❄❄T2 x双 Tx µx上下班证据从我们对定义的表述中可以立即清楚地看出，命题的条件隐含了定义的连贯性要求。 反之，为了证明C中的自然性，设y = 1，给定一个映射g：xz在C中，将其与η z合成，并应用定义的一致性条件对于关于st的相干性，取µ情节与权力336−→- −→−→i=1n（Tf）n- -f：y×x−→Tz为ηy×x。对于μ的相干性，设y= 1，f为idTx。✷关于定义的连贯性条件，还有其他有趣的分解。在上面，我们取T为C上的闭函子。 但人们也经常把正则函子J的右伴随记为T：C CT，因为右伴随在对象上的行为精确地由T在对象上的行为给出。有了这种重载的符号，我们有函子（T）n：CT C和T：CT C，我们可以说它们之间的自然变换，我们有下面的命题。命题2.3ObC-指标映射族αx：（T x）n−→Tx是一个代数运算当且仅当α在CT中是自然的且α关于st。在另一个方向上，正如我们将在下面进一步研究的那样，有时将相干条件的μ部分与其余部分分开是方便的。我们可以通过下面的一些技术性结果来做到这一点命题2.4一个ObC索引的家族αx：（T x）n−→Tx形成代数运算当且仅当α尊重μ，并且对于每个映射，f：y×x−→z在C中，图y×（Tx）ny× αx❄n·（y×πi）nn（T（y×x））（Tz）αz❄y×TxT（y×x）Tzst Tf上下班3如果C是封闭的，则对于我们更深刻的结果，似乎最好首先假设C是封闭的，用这些术语解释结果，然后放弃封闭性条件，解释如何在没有本质变化的情况下重新表达结果。所以对于本节的结果，我们假设C是闭的。设C的封闭结构表示为[、].给定C上的一个单子，给出T的一个强度等价于给出T在C中的一个富集：给定一个强度，人们有一个富集Tx，y：[x，y]−→[T x，Ty]情节与权力337−→--由转置给出[x，y]×TxstT（[x，y]×x）如果T是一个丰富的，那么我们就有一个由以下转置给出的强度：x[y，x×y]Ty，x×y[Ty，T（x×y）]验证强度公理等价于富集公理是例行的。因此，给定C上的一个强单子，单子T在C中是丰富的，函子（−）n：C−→C也是如此。范畴CT也在C中规范地获得了一个充实，即CT的母集CT（x，y）提升为C的一个homobject：C的对象[x，Ty]作为一个homobject，应用函子C（1，−）：C−→Set给它母集CT（x，y）;复合CT（y，z）×CT（x，y）−→CT（x，z）电梯到C[y，Tz]×[x，Ty]−→[x，Tz]通过取转置并应用两次评估图以及每个强度和乘法一次来确定;以及类别提升的恒等式和公理。正则函子J：C CT成为一个C-丰富函子，具有一个C-丰富右伴随.封闭性条件对我们的主要优点是，它允许我们省去自然性的参数化，或者等价地省去关于强度的相干性，如下所示。命题3.1如果C是闭的，则一个ObC-指标族αx：（T x）n−→Tx形成代数运算当且仅当（ ）n[T x，μz]Tx，Tz[x，Tz][（Tx）n，（Tz）n][T x，µz]·Tx，Tz❄[（T x）n，αz]❄[T x，Tz]<$[（T x）n，Tz] [αx，Tz]上下班图中左边的垂直图正是C-富右伴随T：CT−→C到Homs上的典型C-富函子J：C−→CT的行为，并且顶部水平映射正好是Homs上C-富函子（T−）n：CT−→C的所以情节与权力338−→×−→- --−→−→−这个命题中的一致性条件正是α从C-丰富函子（T−）n形成C-丰富自然变换的陈述： CT−→C到富C函子T：CT−→C。证据 给定一个映射f：yXTz在C中，映射的转置给出了从y到[x，Tz]的映射。用这个映射预先构成这里的连贯性条件，然后把两边转置，就得到了定义的连贯性条件。反之，给定一个映射g：y[x，Tz]，取它的转置，使用定义的相干条件，再转置回来，表明上面的平方与g交换。所以根据米田引理，我们完成了✷如果C是闭的，通过修改命题2.4，同样的论证可以用来给出代数运算这产生命题3.2如果C是闭的，则一个ObC-指标族αx：（T x）n−→Tx形成代数运算当且仅当α尊重μ，（ ）nTx，z[x，z][（Tx）n，（Tz）n]Tx，z❄[（T x）n，αz]❄[T x，Tz][（T x）n，Tz][αx，Tz]上下班这个命题说，如果C是闭的，则代数运算恰好是从C-丰富函子（T）的C -丰富自然变换）n：CC到C-丰富函子T：CC是相对于μ而言的一致性。4代数运算作为Homs上的运算到目前为止，在我们对代数运算概念的各种表述中，我们总是有一个ObC-索引族αx：（T x）n−→Tx并认为它的等价条件下，它可能被称为一个代数运算。在计算中，这相当于考虑表达式上的运算符。但是还有另一种方法，在这种方法中，范畴CT的箭头可以被看作是原始的，把它们看作是程序。这是[9]中有限非决定论语义学的重新表述[1]的基本思想。因此，我们应该重新表述代数运算的概念，情节与权力339-−→本协议的第3.1章让我们这样做为了解释相干条件的原因，我们将从假设C是封闭的来表达结果开始;之后我们将放弃封闭性假设，看看如何使用参数化的自然性来重新表达结果我们首先需要解释一个充实版本的米田引理[4]。如果D是一个小的C-富集范畴，那么Dop也可以被看作是一个C-富集范畴.我们在这里不假设C是完全的，但是如果我们这样做了，那么我们将有一个C-丰富的函子范畴[Dop，C]和一个C-丰富的Yoneda嵌入YD：D−→[Dop，C]C-丰富Yoneda嵌入YD是C-丰富函子，并且在强意义下是完全忠实的，D（x，y）−→[Dop，C]（D（−，x），D（−，y））是范畴C中的同构：所有细节见[4]。通过应用函子C（1，）：C Set，可以导出一个从D中x到y的映射集合到C-富集函子D（−，x）：Dop−→C到C-富集函子D（−，y）：Dop− →C的C-富集自然变换集合的双射。这就是我们需要的结果，只是我们不想假设C是完整的，我们感兴趣的C-丰富范畴是CT形式的，所以一般来说不小。这些都不是主要问题，尽管它们稍微超出了[4]中丰富范畴论的标准表述的范围：人们可以将C嵌入到更大的论域CJ中，就像人们可以将必要时将集合J放入一个更大的宇宙中，以及所需的数学对于丰富的分析出现在[4]。 我们仍然有合理的称为D到[Dop，C]的Yoneda嵌入，这两个范畴都被认为是CJ-丰富的而不是C-丰富的，并且它仍然完全忠实于CJ-丰富的函子。然而，我们可以更直接地公式化我们需要的结果，而无需参考CJ，只需陈述丰富Yoneda引理的限制形式：令F unC（Dop，C）表示从Dop到C的C-丰富函子的（可能很大的）范畴，D−→F unC（Dop，C）的米田嵌入是完全忠实的。我们在这里和下一节都使用后一种说法。现在我们来看一下本节的主要结果，假设C是闭的。定理4.1若C是闭的，给出一个代数运算等价于给出一个ObCop×ObC映射ay，x：[y，Tx]n−→[y，Tx]即在y中作为Cop的对象是C-自然的，在x中作为情节与权力340i=1×i=1×⇒opCT，即，使得[y，Tx]n×[yJ，y]ay，x×[yJ，y]❄n=p·（πi×[yJ，y]）n[yJ，Tx]nayJ，x❄[y，Tx][yJ，y][yJ，Tx]comp和[x，Tz]×[y，Tx]n[x，Tz]×ay，x❄K·（[x，Tz]×πi）<$n[y，Tz]nay，z❄[x，Tz][y，Tx][y，Tz]组分K其中comp是C的富C组成，compK是富C Kleisli组成。证据首先观察[y，Tx]n同构于[y，（Tx）n]。现在，从我们的米田引理的C-丰富版本可以得出，给出数据和命题的第一个公理等价于给出一个ObC-索引族α：（T x）n−→Tx通过进一步应用我们的米田引理的C-丰富版本，因此，命题的第二个条件等价于命题3.1的连贯性条件。✷如前所述，即使没有C是闭的条件，我们仍然可以本质上陈述这个结果。原因有二。首先，在本文中，我们假设Kleisli指数的存在，这是建立λ项模型所必需的。但是我们上面使用的C的闭合结构的大多数例子都是[y，Tx]的形式，它同样可以表示为克莱斯利指数y x。克莱斯利指数通常扩展到函子− −：CTT−→C第二，在上面，我们使用了一个形式为[yJ，y]的构造，其中没有T保护第二个对象。但是我们可以用普通的米田引理来代替它，用映射来表达定理的第一个条件。f：w×yJ−→y。总结一下，我们有情节与权力341××nji=1⇒ × ⇒⇒−→ ⇒ −-−→推论4.2给出代数运算等价于给出ObCop ObC映射ay，x：（y<$x）n−→（y<$x）在C中，使得对于C中的每个映射f：w×yJ-→y，（f x）nwyJ（yx）×w×yay，x×f（（w×yJ）n×w×yJev·（aw×yJ，x×w×yJ）❄（yx）×y❄阿克斯EV上下班，图表（x<$z）×（y<$x）n（x<$z）×ay，x❄K·（（x<$z）×πi）<$n（y）nay，z❄（x z）（y x） （y z）组分K其中compK是Kleisli组合的规范内化。5代数运算作为类属效应在本节中，我们将C-丰富Yoneda引理的公式化应用于完全不同项的代数运算，再次作为CT中的映射，即，在一般效应方面 注意，如果C有一个n重余积n为1，则函子（T−）n：CT −→C同构于函子n<$−：CTC. 如果C是闭的，则函子n正则地充实为C-丰富函子，并且该C-丰富函子恰好是可表示的C-函子CT（n，）：CTC，其中CT被认为是C-富集范畴。因此，通过命题3.1和我们的米田引理的C-丰富版本，我们立即有定理5.1如果C是闭的，C-丰富的Yoneda嵌入在CT和代数运算中诱导映射1-→n之间αx：（T x）n−→Tx这 个 结 果 本 质 上 只 是 一 个 例 子 ， 它 是 用 Lawvere 理 论 的 运 算 对Lawvere理论中的映射进行识别的一个丰富版本。注意，它遵循没有数学理由限制×情节与权力342不−→∨−∨∨注意自然数n的arityn的代数运算。在这种情况下，我们也可以说代数运算的形式是：αx：（a<$−）−→（b<$−）对于C中的任何对象a和b。 比如说，我们可以把一个账户我们可以用它来模拟涉及状态的操作。对于C的特定选择，例如C=P oset，可以考虑更多的奇异点，例如谢尔宾斯基空间。再一次，通过使用参数化，我们可以避免这里对C的封闭性假设，从而产生更强的陈述定理5.2− C −：Cop×CT−→C在其第一个变量中的泛函性导致从C T中的映射集1 n到代数运算集的双射αx：（T x）n−→Tx我们认为这是该文件最深刻的结果。这一结果表明，给出一个代数运算等价于给出一个一般结果，即，类型为运算量的常数。例如，给一个强单子T一个二元非确定性算子等价于给一个2型常数，给这个算子一个方程等价于给这个常数满足的方程。这里的主要例子是T是非空的有限幂集单子或幂域。给定一个非确定性运算符，常数由true假，并且给定常数c，运算符由M N = if c then M else N给出。两个元素集正好有三个非空的有限子集，相应地，在非空的有限幂集单子上正好有三个代数运算，它们由两个投影和选择给出。这个结果与丰富的Lawvere理论[12]的联系如下。如果C是局部有限可表示为闭范畴的，则可以定义C上的无限C-丰富单子的概念和C-丰富Lawvere理论的概念，并证明这两者是等价的，推广了在C=Set的情况下通常的等价性。给定一个无穷富C单子T，相应的富C Lawvere理论由CT的由有限可表示对象确定的全子C范畴其中包括1的所有有限余积。因此，我们的结果在这里完全涉及地图的Lawvere理论与代数运算，推广Lawvere的原始想法。当然，在本文中，我们没有对范畴C或单子T作有限性假设，但我们的结果在本质上是相同的。定理5.2毫不费力地扩展到可表示的对象a和b的情形;人们只需要对构造（T）n作适当的精化，以说明a和b是C的对象而不是有限数。这很容易通过检查[12]的工作来实现，在一个特殊的情况下，它似乎提供了与国家有关的一些操作的说明情节与权力343−→−→就像莫吉建议的那样。6代数运算与代数范畴最后，在这一节中，我们讨论了代数运算的概念，在代数范畴T-Alg上。由单子T诱导的T-Alg上的comonad的co-Kleisli范畴被用来对具有效应的按名称调用语言进行建模，因此这个公式为我们提供了一个指示，说明如何将我们的分析推广到按名称调用计算，或者可能推广到按值调用和按名称调用的某种组合，参见[5]。如果C是封闭的，并且有均衡器，推广Lawvere，前一节的结果同样可以表示为代数运算和运算α（A，a）：U（A，a）n−→U（A，a）自然在（A，a）中，其中U：T-AlgC是C-丰富的遗忘函子：为了使T-Alg在C中丰富，在C中需要均衡器.我们再次利用我们的Yoneda引理的C-丰富版本证明了这个结果，并观察到正则C-丰富函子I：CT−→T-Alg是完全忠实的。形式上，结果是定理6.1如果C是闭的且有均衡器，则C-富集Yoneda嵌入诱导C-T中的映射1n自然变换之间的双射α：（U −）n−→ U −。结合定理5.1，我们有推论6.2若C是闭的且有均衡器，则给出一个代数运算αx：（T x）n−→Tx相当于将富含碳元素的自然转化为α：（U −）n−→ U。我们也可以给出这个结果的参数化版本，如果C既不是封闭的，也不是完全的，沿着上一节中的CT它产生定理6.3给出一个代数运算αx：（T x）n−→Tx等价于给出一个Ob（T-Alg）-指标映射族α（A，a）：U（A，a）n−→U（A，a）使得对于每个映射f：x×U（A，a）−→U（B，b）情节与权力344×××-−→的交换性x×TAx×Tfx×T Bx× a❄x×b❄表示交换性xAxBx×ff·（x×πi）x×U（A，a）nx×α（A，a）❄i=1 U（B，b）nα（B，b）❄x U（A，a）<$U（B，b）F7结论和进一步工作对于一些最后的评论，我们注意到，在文献中很少注意到我们在这里大量使用文[11]的主要结果都没有使用它，尽管它们确实要求CT中的自然性。 因此，很自然地要问为什么会这样。对于后一点，在[11]中，我们几乎专门讨论闭项，这意味着代数运算的参数化自然性不会出现，因为我们没有任何参数。关于为什么参数化的自然性在过去似乎没有得到太多的讨论，观察到对于C=Set，每个单子都有唯一的强度，所以α的参数化自然性等价于α的普通自然性。更一般地，如果函子C（1，）：C Set是忠实的，即，如果1是C中的生成元，则参数化自然性再次等价于α的普通自然性。这对于P oset和ω-cpo's范畴是正确的，它们是这方面研究范畴的主要例子。我们有区别的原因是因为我们没有假设1是一个生成器，允许我们包括例如toposes或Cat的例子。当然，在将来，我们希望处理其他非代数的操作，例如处理异常的操作。本文的方法似乎不太可能直接延伸。欧金尼奥·莫吉（EugenioMoggi）建议我们超越单子。我们还想扩展这项工作，并将其与解决统一计算帐户的其他方面的工作相情节与权力345的影响。我们在这里特别注意到Paul Levy引用[1] 安德森，S.O.， 和A. J. 幂 ，有限非决定论的一种有代表性的方法，理论计算。Sci. 177（1997）3-25。[2] 琼斯角，澳-地“Probabilistic论文，爱丁堡大学，报告ECS-LFCS-90-105，1990年。[3] 琼斯角，澳-地和G. D. Plotkin，A ProbabilityPowerdomain ofEvaluations，Proc. LICS 4（1989）186[4] 凯莉， 通用汽车，“基本 概念 的 《丰富范畴理论》，[5] Levy，P.B.，按推值调用：一个包含的范例，[6] Moggi，E.，《计算代数演算和单子》，Proc. LICS 89（1989）14-23。[7] Moggi，E.， An abstract view of programming languages，University ofEdinburgh，Report ECS-LFCS-90-113，1989.[8] Moggi，E.，计算和单子的概念，Inf.和Comp.93（1991）55-92。[9] Plotkin，G. D.， A Powerdomain Construction，SIAM J. Comput. 5（1976）452[10] Plotkin，G. D.，[11]Plotkin，G. D.， 和A. J. 《 代数学的权力与权威》，Proc. FOSSACS2001（待发表）。[12] 鲍尔，AJ丰富的Lawvere理论，范畴的理论和应用（2000）83[13] 鲍尔，AJ 和E. P. Robinson，Modularity and Dyads，“Proc. MFPS15”Electronic Notes in Thoeret.比较科学1999年20日