Fibrations理论在索引归纳数据类型不确定语义中的应用

应用Fibrations理论对索引归纳数据类型的不确定语义计算进行了研究。论证了索引范畴的构造,提出了索引Fibration及其真值函子与内涵函子,建立了索引范畴上自函子的一种保持真值的提升,提出了部分F-代数的定义,并应用折叠函数等工具抽象描述了索引归纳数据类型不确定语义计算,辅以实例进行了简要分析,最后通过相关工作的论述指出了Fibrations理论研究方法的优势。     

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

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

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

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

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

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

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

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

计算机科学中的范畴数据类型的研究综述

范畴数据类型是指以范畴论为数学理论基础研究数据类型的描述、计算、语义和应用。早期的范畴数据类型研究以归纳数据类型为主,采用代数从归纳的角度研究有限数据类型的构造语义和递归性质。近年来,归纳数据类型的对偶概念——共归纳数据类型逐渐引起计算机科学工作者的关注与研究,他们采用共代数从观察的角度研究无限数据类型的行为语义和共递归性质。利用范畴论可以为数据类型研究提供统一的数学理论基础,并将代数和共代数中的各种重要研究成果有机地融合在一起,如语法构造与动态行为、递归与共递归、同余与互模拟等。目前,范畴数据类型已经在程序语言、计算描述、理论证明器和并行计算等领域得到广泛的应用。对范畴数据类型的基本概念、数学理论基础、逻辑基础及应用等方面的最新研究成果进行介绍,以引起国内外相关研究领域的学者对计算机科学中的范畴数据类型理论的关注。     

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

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

Institution理论中一个提升函子的余连续性和连续性

本文将[1]一个重要定理（见本文命题2）提升为一个函子F：Insc→(Thc)op，并得到了该函子的余连续性和连续性。这为计算机的共享程序的安全调用以及模块化程序的再用技术的实现提供了一定的理论依据．同时也构造了一个liberal理论范畴TH1，这为“逐步求精”法处理参数化数据类型提供了依据，并且将命题2推广到TH1上。     

基于通用构造器下CDT的关系

CDT(范畴数据类型)模型是一个以范畴理论为基础的计算模型,由于其构造因子存在着不唯一性,因此对某一数据类型的构造就存在多种选择。针对构造因子的多样性,文章给出了构造形式的通用表达方式,并基于该通用构造器的基础深入地研究了不同CDT之间的关系,得到了一些相关的性质和定理。     

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

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

Continuous Functions on Final Coalgebras

It can be traced back to Brouwer that continuous functions of type $\mathsf{Str}A\to B$, where $\mathsf{Str}A$ is the type of infinite streams over elements of A, can be represented by well founded, A-branching trees whose leafs are elements of B. This paper generalises the above correspondence to functions defined on final coalgebras for power-series functors on the category of sets and functions. While our main technical contribution is the characterisation of all continuous functions, defined on a final coalgebra and taking values in a discrete space by means of inductive types, a methodological point is that these inductive types are most conveniently formulated in a framework of dependent type theory.     

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

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

A principled approach to programming with nested types in Haskell

Initial algebra semantics is one of the cornerstones of the theory of modern functional programming languages. For each inductive data type, it provides a Church encoding for that type, a build combinator which constructs data of that type, a fold combinator which encapsulates structured recursion over data of that type, and a fold/build rule which optimises modular programs by eliminating from them data constructed using the buildcombinator, and immediately consumed using the foldcombinator, for that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types in Haskell. Specifically, the standard folds derived from initial algebra semantics have been considered too weak to capture commonly occurring patterns of recursion over data of nested types in Haskell, and no build combinators or fold/build rules have until now been defined for nested types. This paper shows that standard folds are, in fact, sufficiently expressive for programming with nested types in Haskell. It also defines buildcombinators and fold/build fusion rules for nested types. It thus shows how initial algebra semantics provides a principled, expressive, and elegant foundation for programming with nested types in Haskell.     

Remarks on Isomorphisms of Simple Inductive Types

We study isomorphisms of types in the system of simply-typed λ-calculus with inductive types and recursion operators. It is shown that in some cases (multiproducts, copies of types), it is possible to add new reductions in such a way that strong normalisation and confluence of the calculus are preserved, and the isomorphisms may be regarded as intensional w.r.t. a stronger equality relation.     

Safe semi-supervised learning: a brief introduction

Semi-supervised learning constructs the predictive model by learning from a few labeled training examples and a large pool of unlabeled ones. It has a wide range of application scenarios and has attracted much attention in the past decades. However, it is noteworthy that although the learning performance is expected to be improved by exploiting unlabeled data, some empirical studies show that there are situations where the use of unlabeled data may degenerate the performance. Thus, it is advisable to be able to exploit unlabeled data safely. This article reviews some research progress of safe semi-supervised learning, focusing on three types of safeness issue: data quality, where the training data is risky or of low-quality;model uncertainty, where the learning algorithm fails to handle the uncertainty during training; measure diversity, where the safe performance could be adapted to diverse measures.     

Some Properties and Some Problems on Set Functors

We study properties of functors on categories of sets (classes) together with set (class) functions. In particular, we investigate the notion of inclusion preserving functor, and we discuss various monotonicity and continuity properties of set functors. As a consequence of these properties, we show that some classes of set operators do not admit functorial extensions. Then, starting from Aczel's Special Final Coalgebra Theorem, we study the class of functors uniform on maps, we present and discuss various examples of functors which are not uniform on maps but still inclusion preserving, and we discuss simple characterization theorems of final coalgebras as fixpoints. We present a number of conjectures and problems.