程序语言中的共归纳数据类型及其应用

归纳数据类型利用代数方法从构造的角度归纳地描述数据类型的有限语法结构,但在描述动态行为方面存在一定的不足。作为归纳数据类型的范畴对偶概念,共归纳数据类型利用共代数方法从观察的角度共归纳地描述了数据类型的动态行为。首先,从范畴论和代数的角度给出程序语言中的归纳数据类型定义,并分析了相应的递归操作;接着,利用共代数给出共归纳数据类型的范畴论定义,并根据共归纳数据类型的终结性分析了相应的共递归操作;最后,指出如何利用无双代数及分配律将归纳与共归纳数据类型有机地融合起来,探讨数据类型的语法构造与动态行为关系。     

计算机科学中的共代数方法的研究综述

代数理论已经在抽象数据类型、程序语义等计算机科学领域有了广泛的应用,而代数的对偶概念--共代数,则直到20世纪90年代中后期才被越来越多的计算机学者关注.代数从"构造"的角度研究数据类型,而共代数则从"观察"的角度考察系统及其性质.共代数方法对研究基于状态的系统有独特的优越性,可以对系统的行为等价、不确定性等从数学上进行深入的探讨.目前,共代数理论已经逐步应用在自动机理论、并发程序的语义、面向对象程序的规范等领域.对共代数的基本概念、范畴理论基础、共代数逻辑及应用等方面的最新研究成果进行了介绍,以引起国内相关研究领域的学者对计算机科学中的共代数方法的关注.     

程序语言中共归纳数据类型的一种fibrations方法

范畴论与共代数是程序语言中共归纳数据类型研究的传统方法,这些方法在语义行为分析与共归纳规则描述等方面存在一定的不足。针对以上问题,提出了一种fibrations方法以对共归纳数据类型的语义行为与共归纳规则进行研究。该方法系统分析了fibration上共归纳数据类型的重索引函子、对偶重索引函子与真值函子等基本逻辑结构,应用等式函子与商函子等工具建立共归纳数据类型与其语义行为在程序逻辑上的对应关系,深入分析共归纳数据类型的语义行为;并以基范畴上自函子及其在全范畴上保持等式的提升为工具构造共递归操作,抽象描述共归纳数据类型具有普适意义的共归纳规则;最后通过实例分析简要介绍了fibrations方法的应用。     

程序语言中基于Fibrations理论的索引共归纳数据类型

传统范畴论与共代数等方法在分析语义行为与描述共归纳规则方面存在不足,应用Fibrations理论对程序语言中索引共归纳数据类型(indexed co-inductive data type,ICDT)进行了研究。通过基变换构造索引Fibration,建立索引Fibration的等式函子与商函子等工具,应用伴随性质与保持等式的提升深入分析ICDT的语义行为;以此为基础,构造ICDT上参数化的共递归操作,在Fibrations理论框架内抽象描述具有普适意义的共归纳规则,并以实例分析简要介绍Fibrations理论在ICDT中的应用。与传统研究方法相比,Fibrations理论具有简洁的描述性与灵活的扩展性,可以精确分析ICDT的语义行为,具有高度的抽象性且不依赖特定的计算环境,描述了ICDT具有普适意义的共归纳规则。     

基于Fibrations理论的共享系统数据模型

传统共享系统数据模型的建模方法在语义性质分析和语义行为描述方面存在不足,针对以上问题提出了一种基于Fibrations理论的共享系统数据模型。主要工作体现在两个方面:首先,应用真值函子、保持真值的提升与内涵函子并结合代数方法精确分析了语义性质,应用等式函子、保持等式的提升及商函子并结合共代数方法形式化描述了语义行为;其次,在Fibrations理论框架内构造复杂归纳与共归纳数据结构上参数化的递归与共递归操作,抽象描述具有普适意义的归纳与共归纳规则,结合实例简要介绍了Fibrations理论的应用。相对于范畴论等传统方法,简洁描述与灵活扩展的Fibrations理论对共享系统数据模型的语义性质和语义行为进行了精确分析与形式化描述,抽象描述了复杂数据结构具有普适性的归纳与共归纳规则。     

抽象数据类型的双代数结构及其计算

程序语言中的许多抽象数据类型包含了可递归定义的语法构造和可共递归定义的动态行为特征,因此单纯利用代数或共代数难以给出完整的描述.双代数是同一载体集上的代数和共代数对,提供了一种从范畴论的角度探讨抽象数据类型上的语法构造和动态行为关系及性质的可行途径.给出抽象数据类型的双代数结构,并利用代数函子对共代数函子的分配律描述了语法构造与动态行为之间的自然转换关系;利用分配律对共代数和代数函子进行函子化提升,给出一种构造初始代数(或终结共代数)上的共代数(或代数)结构,并将其提升为初始(或终结)λ-双代数的方法.在此基础上,进一步将函子化提升应用于各种递归(包括迭代和原始递归)及共递归函数(包括共迭代和原始共递归)的定义及计算中,并给出相应的计算定律.     

归纳数据类型的范畴论方法

归纳数据类型是类型论研究的重要分支,传统的数理逻辑或代数方法侧重于描述归纳数据类型的有限语法构造,在语义性质与归纳规则的分析与设计方面存在一定的不足.基于范畴论的方法,在集合范畴的框架内给出谓词的形式化定义,分析谓词范畴与代数范畴的构成与性质,并探讨集合范畴上自函子到谓词范畴上自函子的提升,最后利用伴随函子及其伴随性质深入分析了归纳数据类型具有普适意义的归纳规则.     

一种基于共代数的面向对象形式语义

针对面向对象方法的数学理论基础相对薄弱的问题,利用共代数方法从范畴论及观察的角度研究面向对象的形式语义及行为关系。首先,给出类和对象的共代数描述,其中抽象类定义成一个类规范,类定义为满足类规范的共代数,类的各个对象则看成共代数状态空间上的元素,并分别利用强Monads理论和断言给出方法的行为的参数化描述和语义约束;接着,利用共代数互模拟探讨了不同对象在强Monads下的行为等价关系;最后用实例说明如何通过PVS工具证明类规范的一致性及对象的行为关系。     

子共代数与共同余共关系

共代数方法是近几年来理论计算机科学的研究热点之一,在并行计算模型、自动机及面向对象技术的理论基础方面有着广泛的应用.以范畴理论为工具讨论子共代数的性质,特别是集合范畴上的子共代数的性质,证明了集合范畴上的子共代数都是正则子共代数.进一步利用共同余共关系与子共代数之间的对应,给出了集合范畴上共生成子共代数的一种构造方式.     

类型化π演算的双代数语义

证明互模拟同余通常冗长且易出错.双代数为解决该问题提供统一的框架:若行为函子保持弱回拉,共代数范畴到基范畴的忘却函子有右伴函子,则最大共代数互模拟同余.但已有双代数理论建模类型化π演算存在以下困难:行为函子不保持弱回拉,进程互模拟与共代数互模拟不一致.为解决以上两个问题,用稠密拓扑导出布尔范畴作为语义范畴,令行为函子保持弱回拉;定义一类行为函子,使最大进程互模拟与最大共代数互模拟一致,而迟语义和早语义对应的行为函子属于该类函子.进而给出π演算最大进程互模拟同余的双代数模型,为进一步应用双代数框架对其他复杂演算建模奠定了理论基础.     

Presenting functors on many-sorted varieties and applications

This paper studies several applications of the notion of a presentation of a functor by operations and equations. We show that the technically straightforward generalisation of this notion from the one-sorted to the many-sorted case has several interesting consequences. First, it can be applied to give equational logic for the binding algebras modelling abstract syntax. Second, it provides a categorical approach to algebraic semantics of first-order logic. Third, this notion links the uniform treatment of logics for coalgebras of an arbitrary type T with concrete syntax and proof systems. Analysing the many-sorted case is essential for modular completeness proofs of coalgebraic logics.     

Coalgebras in functional programming and type theory

This is a survey article on the use of coalgebras in functional programming and type theory. It presents the basic theory underlying the implementation of coinductive types, families and predicates. It gives an overview of the application of corecursive methods to the study of general recursion, formal power series, tabulations of functions on inductive data. It also sketches some advanced topics in the study of the solutions to non-guarded corecursive equations and the design of non-standard type theory.     

Generalised folds for nested datatypes

Nested datatypes generalise regular datatypes in much the same way that context-free languages generalise regular ones. Although the categorical semantics of nested types turns out to be similar to the regular case, the fold functions are more limited because they can only describe natural transformations. Practical considerations therefore dictate the introduction of a generalised fold function in which this limitation can be overcome. In the paper we show how to construct generalised folds systematically for each nested datatype, and show that they possess a uniqueness property analogous to that of ordinary folds. As a consequence, generalised folds satisfy fusion properties similar to those developed for regular datatypes. Such properties form the core of an effective calculational theory of inductive datatypes. Received September 1998 / Accepted in revised form July 1999     

Recursive coalgebras from comonads

The concept of recursive coalgebra of a functor was introduced in the 1970s by Osius in his work on categorical set theory to discuss the relationship between wellfounded induction and recursively specified functions. In this paper, we motivate the use of recursive coalgebras as a paradigm of structured recursion in programming semantics, list some basic facts about recursive coalgebras and, centrally, give new conditions for the recursiveness of a coalgebra based on comonads, comonad-coalgebras and distributive laws of functors over comonads. We also present an alternative construction using countable products instead of cofree comonads.