归纳数据类型的范畴论方法-论文.pdf

《归纳数据类型的范畴论方法-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第42卷第6期计算机科学Vo1．42No。62015年6月ComputerScienceJune2015归纳数据类型的范畴论方法苗德成奚建清苏锦钿。(韶关学院数学与信息科学学院韶关512005)(华南理工大学计算机科学与工程学院广州510640)。摘要归纳数据类型是类型论研究的重要分支，传统的数理逻辑或代数方法侧重于描述归纳数据类型的有限语法构造，在语义性质与归纳规则的分析与设计方面存在一定的不足。基于范畴论的方法，在集合范畴的框架内给出谓词的形式化定义，分析谓词范畴与代数范畴的构成与性质，并探讨集合范畴上自函子到谓词范畴上自函子的提升，最后利用伴随函子及其伴随性

2、质深入分析了归纳数据类型具有普适意义的归纳规则。关键词归纳数据类型，范畴论，谓词范畴，提升，伴随函子中图法分类号TP301．2文献标识码ADOI10．I1896／j．issn．1002—137X2015．6．002CategoryTheoreticalMethodofInductiveDataTypesMIAODe-chengXIJian-qing。SUJin-dian2(SchoolofMathandInformation，ShaoguanUniversity，Shaoguan512005，China)(SchoolofComputerScienceandEng

3、ineering，SouthChinaUniversityofTechnology，Guangzhou510640，China)ZAbstractInductivedatatypesareimportantresearchbranchoftypetheory，andtraditionalmethodsincludingmathe—maticallogicandalgebrafocusondescribingfinitesyntaxconstructionforinductivedatatypes，resultinginsomedeft—cienciesforana

4、lyzinganddesigningsemanticspropertiesandinductiverules．Thispaperprovidedformaldefinitionofpredicateintheframeworkofsetcategorybycategorytheoreticalmethods，analyzedtheconstructionandpropertiesofpredicatecategoryandalgebracategory，andprobedliftingofendofunctorsfromsetcategorytOpredicate

5、category，andatlastdeeplyresearcheduniversalinductiverulesofinductivedatatypesbyadjointfunctoranditsadjointproperties。KeywordsInductivedatatypes，Categorytheory，Predicatecategory，Lift，Adjointfunctor谓词的形式化定义，对谓词范畴和代数范畴进行描述与证明，1引言并分析相应的折叠操作；第3节探讨集合范畴到谓词范畴自程序语言的数据类型可以递归定义。递归数据类型是类函子的提升；第4节

6、通过对代数范畴间一对伴随函子的研究型表达式的同构解，而作为类型同构表达式最小解的归纳数深入分析归纳数据类型具有普适意义的归纳规则；第5节分据类型(InductiveDataTypes)是一类重要的递归数据类型，析当前归纳数据类型研究领域的一些相关工作；最后总结全在程序语言中有许多应用，如描述流、表、树及带环无限循环文并给出后续研究工作。图等复杂的数据结构，支持协同进程演算及控制过程等。2谓词范畴与代数范畴传统归纳数据类型的研究以数理逻辑或代数方法为主El-3]，侧重于描述归纳数据类型的有限语法构造，将归纳数折叠操作_厂oz对归纳数据类型的递归操作建立语义模据类型及

7、操作封装在∑_代数结构内，但在语义性质与归纳规型，谓词描述归纳数据类型的语义性质，下面给出谓词的形式则描述等方面仍存在一定的不足。范畴论在形式语言建模理化定义。本文假定读者具备函子、自然转换与伴随等概念的论、形式语义学和程序设计方法等计算机科学基础研究领域范畴论基础，记ObjC为范畴C的对象集，MotC为范畴C有着广泛的应用，为理解计算机体系结构、软件规范和程序间的态射集。联系提供一种通用的理论工具、思维方法和研究手段。基于定义1设Set为集合范畴，VX∈ObjSet，X上的一个范畴论的观点，归纳数据类型抽象为函子的初始代数，由初始谓词是一个二元组(X，P>，即P

8、：X—S。