带固定参数的 Monadic 递归.pdf

《带固定参数的 Monadic 递归.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、华南理工大学学报（自然科学版）第４２卷第７期JournalofSouthChinaUniversityofTechnologyVol．４２No．７２０１４年７月（NaturalScienceEdition）July２０１４文章编号：１０００-５６５Ｘ（２０１４）０７-００３３-０７倡带固定参数的Ｍｏｎａｄｉｃ递归１２苏锦钿余珊珊（１．华南理工大学计算机科学与工程学院，广东广州５１０６４０；２．广东药学院医药信息工程学院，广东广州５１０００６）摘要：针对归纳数据类型上的递归操作可能包含固定参数且产生计算副

2、作用的问题，结合函数式程序语言中的ｍｏｎａｄｓ及范畴论中的伴随关系给出ｍｏｎａｄｉｃ强归纳数据类型的定义及ｍｏｎａｄｉｃ强初始性的证明；在此基础上，进一步提出一种带固定参数且产生计算副作用的递归操作的定义，证明了它比一般的递归具有更好的抽象性和封装性，同时分析了相应的范畴论性质和计算律．关键词：递归；归纳数据类型；初始代数；ｍｏｎａｄ；范畴论；程序语言中图分类号：ＴＰ３０１．２ｄｏｉ：１０．３９６９／ｊ．ｉｓｓｎ．１０００-５６５Ｘ．２０１４．０７．００６［１］作为归纳数据类型上最重要的一种计算模强共归

3、纳数据类型上的纯函数，没有考虑计算过程［２］式，递归操作ｆｏｌｄ在程序设计、推理、转换和优化中可能产生的副作用．［１２］等方面具有广泛的应用，并构成其他各种复杂的递Ｆｏｋｋｉｎｇａ结合ｍｏｎａｄｓ及集合范畴上的正则归计算的基础，如原始递归、Ｃｏｕｒｓｅ-ｏｆ-Ｖａｌｕｅ迭代、函子提出任意数据类型上的ｍｏｎａｄｉｃ射和ｆｏｌｄ．Ｈｕ带参数的递归和累积递归等．但ｆｏｌｄ一方面要求计等［１３］进一步将Ｆｏｋｋｉｎｇａ的研究扩展到任意ｍｏｎａｄｓ算源中的元素必须具备相应的代数结构，无法包含［１４］上．Ｍｅｉｊｅ

4、ｒ等则从函数式程序语言实现的角度探额外的参数用于作为计算的输入；另一方面只适合［１５］讨ｍｏｎａｄｉｃｆｏｌｄ的应用．Ｐａｒｄｏ也结合ｍｏｎａｄｓ给出于描述计算过程中所产生的确定性结果，无法包含包含计算副作用的ｍｏｎａｄｉｃ共递归和ｈｙｌｏｍｏｒｐｈｉｓｍ其他各种计算副作用（如偏序、非确定性、异常、连的定义．在Ｐａｒｄｏ和Ｍｅｉｊｅｒ的研究基础上，Ｇｈａｎｉ续、交互式输入、交互式输出等）．针对上述问题，［１６］等探讨了所有归纳数据类型上的ｂｕｉｌｄ结合子及Ｃｏｃｋｅｔｔ等最早在文献［３-４］中利用笛卡尔

5、封闭范畴其参数的归纳和ｍｏｎａｄｉｃ构造．这些研究均没有考上的强函子提出了强范畴数据类型的概念，使得强虑带参数且包含计算副作用的递归，也没有分析相归纳数据类型上的ｆｏｌｄ可包含额外的参数，并将其应的范畴论性质及其代数计算律．作为函数式程序语言Ｃｈａｒｉｔｙ的基础．随后，Ｐａｒ-ｄｏ［５-７］进一步对强归纳数据类型上带固定参数和累因此，文中在上述研究的基础上，结合范畴论中积参数的递归操作ｐｆｏｌｄ和ａｆｏｌｄ的范畴论性质及其的ｍｏｎａｄｓ及伴随概念给出ｍｏｎａｄｉｃ强归纳数据类计算律进行了分析．笔者在前期

6、工作中也分析了强型的定义及其ｍｏｎａｄｉｃ强初始性的证明，并分析了共归纳数据类型上带固定参数的共递归及其计算其上带固定参数且包含计算副作用的递归操作的定［８-９］［１０］律，并将其扩展到ｈｙｌｏｍｏｒｈｐｉｓｍ中，同时还从义、性质及计算律，从而将Ｃｏｃｋｅｔｔ和Ｐａｒｄｏ等对强归双代数的角度探讨了归纳与共归纳数据类型、递归纳数据类型及Ｆｏｋｋｉｎｇａ、Ｈｕ和Ｍｅｉｊｅｒ等对ｍｏｎａｄｉｃ递［１１］与共递归间的关系．上述研究都是针对强归纳或归的研究融合在一起．收稿日期：２０１４-０３-１４倡基金项目：国家

7、自然科学基金资助项目（６１１０３０３８）；华南理工大学中央高校基本科研业务费专项资金资助项目（２０１３ＺＺ００５５）作者简介：苏锦钿（１９８０-），男，博士，副教授，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究．Ｅ-ｍａｉｌ：ＳｕＪＤ＠ｓｃｕｔ．ｅｄｕ．ｃｎ３４华南理工大学学报（自然科学版）第４２卷X，YY，X１归纳数据类型和ＭｏｎａｄｓｌｓF＝F枙ｓｎｄ，ｆｓｔ枛礋ｒｓF礋枙ｓｎｄ，ｆｓｔ枛：X×FY→F（X×Y）．容易验证若F和G都是强函子，则FG也是强函１．１代数和归纳数据类型X，Y

8、X，YGX，Y子，且存在相应的右强度ｒｓFG＝FｒｓG礋ｒｓF：FGX×下面首先给出代数的范畴论定义．X，YX，YX，GYY痴FG（X×Y）和左强度ｌｓFG＝FｌｓG礋ｌｓF：X×定义１给定范畴C和自函子F：C→C，F－代数FGY痴FG（X×Y）．定义为二元组（X，αX：FX→X），其中X称为该F－代Ｋｏｃｋ在文献［２０］中证明了分配范畴C上的定数的载体，αX称为该F－代数的基调．任意两个F－义２中的代数函子都是强函子．代数（X，αX）和（