程序语言中的许多抽象数据类型包含了可递归定义的语法构造和可共递归定义的动态行为特征,因此单纯利用代数或共代数难以给出完整的描述.双代数是同一载体集上的代数和共代数对,提供了一种从范畴论的角度探讨抽象数据类型上的语法构造和动态行为关系及性质的可行途径.给出抽象数据类型的双代数结构,并利用代数函子对共代数函子的分配律描述了语法构造与动态行为之间的自然转换关系;利用分配律对共代数和代数函子进行函子化提升,给出一种构造初始代数(或终结共代数)上的共代数(或代数)结构,并将其提升为初始(或终结)λ-双代数的方法.在此基础上,进一步将函子化提升应用于各种递归(包括迭代和原始递归)及共递归函数(包括共迭代和原始共递归)的定义及计算中,并给出相应的计算定律.
Most of abstract data types in programming languages include both syntactive constructions and dynamic behaviors features which can be defined recursively or coreeursively respectively, so simply using algebras or coalgebras can not offer a comprehensive description. As a pair of algebras and coalgebras with the same carrier set, bialgebras provide a feasible way to discuss the relations and properties between syntactic constructions and dynamic behaviors of abstract data types from the perspective of categorical theory. Bialgebraic structures :for abstract data types are proposed in this paper and distributive laws of algebraic functors over coalgebraic functors are used to analyze the natural transformations between syntactic constructions and dynamic behaviors. Then, distributive laws are used to functorially lift coalgebraic and algebraic functors, which entail a way to build coalgebraic (or algebraic) structures on initial algebras (or final coalgebras) and lift them into initial (or final) λ-bialgebras. Finally, the applications of functorial lifting in the definitions and computations of various recursions (including iterations and primitive recursion) and corecursions (including coiterations and primitive corecursion) are discussed, as well as their corresponding computation laws.