计算机科学中的Comonads理论_代写论文

计算机科学中的Comonads理论#
苏锦钿1，余珊珊2*
基金项目：2010年高校博士点科研基金新教师类（20100172120043）；华南理工大学中央高校基本科研业务费专项资金（2009ZM0158）;2011年国家自然科学基金-青年科学基金项目（61103038）作者简介：苏锦钿（1980-），男，讲师，主要研究方向：形式化方法及形式语义，构件技术，共代数与双代数. E-mail: SuJD@scut.edu.cn
（1. 华南理工大学计算机科学与工程学院； 2. 中山大学信息科学与技术学院） 5
摘要：作为monads的范畴对偶概念——comonads是在近十几年来才逐渐引起计算机科学工作者的关注与研究.Comonads可以给出各种上下文依赖计算的一种结构化描述,并结合共代数研究程序语言的操作语义和内涵语义.目前,comonads已在程序计算、形式语义、类型理论、模态逻辑、共代数和双代数等领域得到初步的应用.对comonads的范畴论定义、基本性质础、10 与共代数之间的关系等方面的最新研究成果进行介绍,以引起国内外相关研究领域的学者对计算机科学中的comonads理论的关注.
关键词：软件理论; monads; comonads; 范畴论; 共代数
中图分类号：TP301.2
15 Comonad Theory in Computer Science
SU Jindian1, YU Shanshan2
(1. School of Engineering and Science, South China University of Technology; 2. School of Information Science and Technology, Sun Yet-Sen University, Guangzhou 510275)
Abstract: Comonads, as the dual concepts of monads, have not be noticed by computer scientists 20 till the past few decades. Comonads can be used to offer a structural description for various context-dependent computations and analyze the operational semantics and intensional semantics of programming languages by incorporating coalgebras. Currently, comonads have been applied in many research fields, i.e. program computations, formal semantics, type theories, modal logics and coalgebras and bialgebras. The recent progress of comonad theory including its categorical 25 defniitions, basic properties, relations with coalgebras, is summarized for raising the attention of the relative researchers.
Key words: software theory; monads; comonads; category theory; coalgebras
0 引言 30
作为monads的范畴对偶概念,comonads(共模)理论是近十几年来才引起计算机科学工作者的关注与研究,并成为理论计算机科学中的一个研究热点.早期的研究主要集中在对comonads理论本身的完善,在实际软件开发及应用研究中的讨论并不多见.主要的原因有两方面:一是在形式语义研究中人们往往更关注程序计算的各种副作用,即外延语义(extensional semantics),而忽略计算的内部细节,即内涵语义(intensional semantics);二是缺乏直观有效的应35 用途径和有足够说服力的实例.在共代数方法[1](coalgebraic methods)出现以后,comonads与共代数(coalgebras)之间的有机结合使得comonads理论展现出强大的生命力和在形式语义、计算描述及类型理论等众多计算机科学领域中的广阔应用前景,特别是comonads所引入的程序设计方法、理解程序计算的新思路和对计算描述的高度抽象性等特点引起了研究人员的极大兴趣. 40
60年代初,P.J.Huber在研究homotopy理论时从triple的对偶角度出发,给出了cotriple的定义.随后,J.MBeck和M.Barr从纯范畴论的角度分析了cotriples的一些基本性质[2, 3]、triples

和cotriples间的分配律[4]、cotriples间的组合关系及在Topose范畴中的应用[5].这些研究奠定了comonads的数学理论基础.此后,在90年代中后期共代数方法出现以后,一些计算机科学工作者逐渐发现comonads能够与共代数有机地结合起来,并在系统的动态行为、形式语义和计45 算的结构化描述研究等方面有着独特的优势,能够为这些研究建立良好的基于范畴论的理论基础,并从数学的角度对其性质进行描述和研究.更重要的是,利用comonads与其他函子(特别是monads)间合适的分配律可以将计算机科学中许多重要的基础理论,如代数与共代数、初始语义与终结语义、归纳与共归纳、指称语义与操作语义、等式(簇)与共等式(共簇)等,有机地融合在一起,形成新的交叉点和研究思路. 50 因此，本文从范畴论定义、基本范畴论性质和与共代数之间的关系等几方面对计算机科学中的comonads进行介绍.第1节介绍comonads的范畴论定义,并结合几个典型的例子进行说明;第2节综述comonads理论的基本范畴论性质;第3节介绍comonads与共代数之间的关系;第4节总结全文.
1 Comonads的范畴论定义 55
与monads类似,comonads是以范畴论为数学理论基础,可以利用范畴论中的对象、射、函子和自然转换等概念进行抽象描述和定义.下面分别给出comonads的范畴论定义和coKleisli定义.
定义1. 范畴上的comonad定义为一个三元组(D,,),其中D:为上的自函子, :DId和:DD2均为自然转换,且满足以下的图表交换: 60 DDDIdDDD2DDId D3D2D2DDD 图1. Comonads的一致性性质 Figure 1. Coherence properties of comonads
上述等式(1) D。=D。=IdD和(2)D。=D。称为comonads的一致性性质.和分别称为comonad (D,,)的共单位元(counit)和共乘(comultiplication)操作,可看成是函子D上的65 额外结构.D。=IdD和D。=IdD分别称为comonad (D,,)的左、右共单位元定律.显然,范畴上的一个comonad (D,,)就是([,],Id,])中的一个comonoid,即comonads是comonoids的一种抽象.
以某个笛卡尔封闭范畴(如集合范畴Set或完全偏序范畴CPO)为例,下面给出一些典型的comonads例子. 70
(1) 标识comonad,记为(Id,,)或D=Id.
即函子D为标识函子Id.对于任意的对象X,共单位元X=IdX:XX,共乘X=IdX:XX.显然,范畴上的任意一个标识函子都是一个标识comonad.
(2) 积comonad,记为(Id×A,,)或D=Id×A
其中A为范畴上的某个固定对象.对于任意的对象X,共单位元X=1:XAX,共乘75 X=IdXA,2:XA (XA)A.若DX=X.X×A,其中表示最大固定点,则称该积comonad为流comonad. 积comonad与指数monad T=IdA在笛卡尔封闭范畴中的curry操作下是一一对应的,虽然两者表达了不同的含义,但都可以用于描述依赖于环境的计算.指数monad表示计算中需要类型为A的输入参数,而积comonad则表示在计算的上下文环境中包含类型为A的元素. 80
在共归纳数据类型研究中,积comonad或流comonad可用于表示某个参数化数据类型

A∞(例如流、数组或树),而X和X分别用于对A∞中的元素进行观察或遍历;在计算的结构描述中,积comonad常用于对包含元素类型为A的计算环境进行封装. 例子1. 流计算中的参数化流StrA=νX.X×A可表示成一个流comonad: DX=A∞, X=head: A∞ A,X=tails:A∞(A∞)∞.其中,(相当于流上的head函数)给出了流的当前位置上的值,即头元85 素.而(相当于tails函数)给出一个包含某个给定流的所有尾部的序列.这里的tails函数实际上就是函数式编程中的一个共迭代.
(3) 指数comonad,记为(XS,,)或D=IdS.
其中(S,e,m)是范畴上的一个独异点(monoid),e:1S为单位元,m:SSS为满足组合律的二元操作符. 90 共单位元X=applyX, S。IdXS, e。!:XS,!SXIdXS×1,SXIdeXS×S,applyXSX. 共乘X=curry(curry(υX)):XS(XS)S,其中X=applyX,S。IdXS,m。as:XS×S×SasXS×(S×S) ,SXIdmXS×S ,applyXSX. 克雷化操作curry将每一个射f :XZY映射为curry(f ):XYZ.射applyX, S:XSSX满足对于任意一个射f :XSY,都有唯一的射curry( f ):XYS与之对应,且有f =applyX, S。 curry( f ) 95 IdS.as=1。1,2。1, 2:(XY)ZX(YZ)为一个表示结合律的自然同构射.!:X1表示任意元素X到单元素集1={*}的映射. 指数comonad表示一个从独异点(S,e,m)到状态空间X的函数f :SX,给出该函数中S的单位元所对应的值,给出了一个在函数f :SX作用下由S中各个元素对应的值所构成的序列,并包含S中的某个元素用于指定值在该序列中的位置.在笛卡尔封闭范畴中,指数100 comonad D=IdS与积monad T=Id×S存在一一对应关系.例如,M.Kick在文献[6]就是利用该对应关系将积monad对comonad的分配律映射为一个comonad对另一个指数comonad的分配律. 例子2. 假设(S,e,m)为自然数独异点(Nat,0,+),则指数comonad D=IdS表示自然数Nat与X之间的一个函数关系,即构成了一个有序的状态空间DX=(x0,x1,…,xn),则X(x0,x1,…,xn)=x0, X((x0,x1,…,xn),i, j)=X((x0,x1,…,xn), i+ j)=xi+j-1.例如,X((x0,x1,…,xn),2, 3)=x4. 105
(4) 共状态comonad(也称array comonad[38]),记为(XSS,,)或D=IdSS.
其中S为范畴上的一个对象.共单位元X=applyX,S:XSSX,共乘X=(1,applyXS)IdS, IdS:XS S(XSS)SS. 1,applyXY:XXYY为射applyX, Y :XYYX的逆. 共状态comonad表示计算的上下文环境是由一个从S到X的函数f :SX以及另一个参数S所构成,给出该参数S在函数f中所对应的值. 110 例子3. 若将一个流A∞表示成一个数组ANat的形式,则利用curry是自然同构射的性质可将两个流之间的计算函数StrFun:ANatANat表示成一个共状态comonad DA=ANat×Nat,使得对于函数f :NatA、(a0,a1,…,an)ANat和nNat,有: A((a0,a1,…,an),n)=f (n),即( f, n)f (n), A((a0,a1,…,an),n)=A(( f , m),n),即(f, n)  f (λm.(f, m),n). 115 与monads的Kleisli三元组定义类似，comonads也有另一种等价的定义,称为coKleisli三元组或共三元组(cotriple).
定义2. 范畴上的一个coKleisli三元组表示为(D,,–D),其中D:||||为中对象间的函数关系,使得对于对象X||有X :DXX,对于射f :DXY有f D:DXDY,且满足以下等式: (1) (X)D =IdDX; 120 (2) 对于射f :DXY,有f D;Y=f ; (3) 对于两个射f :DXY和g:DYZ,有: f D;g D=( f D;g)D.
coKleisli三元组(D,,–D)和comonad (D,,)之间存在一一对应关系:给定一个coKleisli三元组(D,,–D),对应的comonad为(D,,),其中D是由函数D到自函子的扩展,即对f :XY有

Df =(X ; f )D,且X=(IdDX)D.相反地,给定一个comonad (D,,),对应的coKleisli三元组为125 (D,,–D),其中D是将函子限制为对象间的函数关系,并且对于f :DXY,有f D:DX DY.即D是对函数的一种提升,将f :DXX提升为IdDX=f D:DXDX,将f :DXY提升为f D: DXDY.f :DXY和g:DYZ之间的coKleisli复合g。D f :DXZ定义为:g。D f =g。Df。X. 由任意一个coKleisli三元组(D,, –D)可以确定一个范畴coKl(D),称为coKleisli范畴.
定义3. 给定范畴中的一个coKleisli三元组(D,,–D),对应的coKleisli范畴coKl(D)为: 130
(1) coKl(D)中的对象就是的对象;
(2) coKl(D)中对象X到Y的射为中形如f :DXY的射; (3) coKl(D)中X上的标识射为X:DXX; (4) coKl(D)中射f :DXY与g:DYZ之间的组合为g。f D:DXZ.
对于由中对象的标识函子构成的范畴Id,容易证明存在一个从Id到coKl(D)的包含135 函子J,且J定义在映射上,使得对于f :XY有Jf =df f。X=Y。Df :DXY.则函子J存在一个左伴随U:coKl(D),使得UX=DX,且若k:DXY,则Uk=kD:DXDY,其中kD将k:DXY提升为kD:DXDY. Comonads的范畴论定义和coKleisli三元组定义各有优势.一般情况下,在研究comonads的范畴论性质、与monads间的对偶性及分配律、comonads共代数、形式语义和模态逻辑时140 往往使用前者;而在函数式程序语言、计算描述及内涵语义研究时往往使用后者.例如,一个包含某种上下文环境的函数式程序可看成是coKleisli范畴中的一个射,而程序间的组合关系就变成了coKleisli范畴中射之间的组合.
学术论文网Tag：代写硕士论文代写论文代写MBA论文代写博士论文

搜索

热门标签:

计算机科学中的Comonads理论