遗传余代数与二次型

给出1类重要的遗传余代数——正规的广义路余代数,在余代数上定义了3种二次型,证明了在Gabriel箭图是局部有限的遗传余代数上定义的这3种二次型一致。     

Hom-余理想的若干性质

根据Hom-结合代数的概念来新定义子Hom-结合代数与Hom-余理想的概念,并进一步讨论子Hom-结合代数、子Hom-余结合余代数与Hom-余理想之间的密切联系。     

Final Coalgebras And a Solution Theorem for Arbitrary Endofunctors

Every endofunctor F of Set has an initial algebra and a final coalgebra, but they are classes in general. Consequently, the endofunctor F^∞ of the category of classes that F induces generates a completely iterative monad T. And solutions of arbitrary guarded systems of iterative equations w.r.t. F exist, and can be found in naturally defined subsets of the classes TY.More generally, starting from any category , we can form a free cocompletion ^∞ of under small-filtered colimits (e.g., Set^∞ is the category of classes), and we give sufficient conditions to obtain analogous results for arbitrary endofunctors of .     

A hierarchy of probabilistic system types

We arrange various types of probabilistic transition systems studied in the literature in an expressiveness hierarchy. The expressiveness criterion is the existence of an embedding of systems of the one class into those of the other. An embedding here is a system transformation which preserves and reflects bisimilarity. To facilitate the task, we define the classes of systems and the corresponding notion of bisimilarity coalgebraically and use the new technical result that an embedding arises from a natural transformation with injective components between the two coalgebra functors under consideration. Moreover, we argue that coalgebraic bisimilarity, on which we base our results, coincides with the concrete notions proposed in the literature for the different system classes, exemplified by a detailed proof for the case of general Segala-type systems.     

A modal proof theory for final polynomial coalgebras

An infinitary proof theory is developed for modal logics whose models are coalgebras of polynomial functors on the category of sets. The canonical model method from modal logic is adapted to construct a final coalgebra for any polynomial functor. The states of this final coalgebra are certain “maximal” sets of formulas that have natural syntactic closure properties.

The syntax of these logics extends that of previously developed modal languages for polynomial coalgebras by adding formulas that express the “termination” of certain functions induced by transition paths. A completeness theorem is proven for the logic of functors which have the Lindenbaum property that every consistent set of formulas has a maximal extension. This property is shown to hold if the deducibility relation is generated by countably many inference rules.

A counter-example to completeness is also given. This is a polynomial functor that is not Lindenbaum: it has an uncountable set of formulas that is deductively consistent but has no maximal extension and is unsatisfiable, even though all of its countable subsets are satisfiable.     

余代数及文档动态描述模型研究

介绍了代数的对偶概念———余代数,以及基于状态系统的余代数描述。将文档的每一句看作一个断言,并动态地将文档理解为一个断言流,从而利用余代数方法对文档的语义进行观察。     

Rational Unification in 28 Characters

We present a case study where Synchronising Graphs, a system of parallel graph transformation, are used to solve the syntactic unification problem for first order rational terms (with possibly infinite unifier). The solution we offer is efficient, that is quasi-linear, and simple: a program of 28 characters.     

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

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