计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2015年
6期
8-11
,共4页
归纳数据类型%范畴论%谓词范畴%提升%伴随函子
歸納數據類型%範疇論%謂詞範疇%提升%伴隨函子
귀납수거류형%범주론%위사범주%제승%반수함자
Inductive data types%Category theory%Predicate category%Lift%Adjoint functor
归纳数据类型是类型论研究的重要分支,传统的数理逻辑或代数方法侧重于描述归纳数据类型的有限语法构造,在语义性质与归纳规则的分析与设计方面存在一定的不足.基于范畴论的方法,在集合范畴的框架内给出谓词的形式化定义,分析谓词范畴与代数范畴的构成与性质,并探讨集合范畴上自函子到谓词范畴上自函子的提升,最后利用伴随函子及其伴随性质深入分析了归纳数据类型具有普适意义的归纳规则.
歸納數據類型是類型論研究的重要分支,傳統的數理邏輯或代數方法側重于描述歸納數據類型的有限語法構造,在語義性質與歸納規則的分析與設計方麵存在一定的不足.基于範疇論的方法,在集閤範疇的框架內給齣謂詞的形式化定義,分析謂詞範疇與代數範疇的構成與性質,併探討集閤範疇上自函子到謂詞範疇上自函子的提升,最後利用伴隨函子及其伴隨性質深入分析瞭歸納數據類型具有普適意義的歸納規則.
귀납수거류형시류형론연구적중요분지,전통적수리라집혹대수방법측중우묘술귀납수거류형적유한어법구조,재어의성질여귀납규칙적분석여설계방면존재일정적불족.기우범주론적방법,재집합범주적광가내급출위사적형식화정의,분석위사범주여대수범주적구성여성질,병탐토집합범주상자함자도위사범주상자함자적제승,최후이용반수함자급기반수성질심입분석료귀납수거류형구유보괄의의적귀납규칙.
