Bialgebraic Structures for Abstract Data Types and Their Computations

Most of abstract data types in programming languages include both syntactive constructions and dynamic behaviors features which can be defined recursively or corecursively 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.