Algebraic cocompleteness and finitary functors

Finitary Corecursion for the Infinitary Lambda Calculus

Kurz et al. have recently shown that infinite $λ$-trees with finitely many free variables modulo $α$-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational $λ$-trees, i.e. those $λ$-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational $λ$-trees.

Strongly Complete Logics for Coalgebras

Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations …

可数步下的终余代数

Terminal Coalgebras in Countably Many Steps

该研究证明了局部有限呈现范畴上有限自函子的终余代数可通过终余代数链的可数极限得到，并给出Vietoris多项式函子等多类函子终余代数的步长结果及相关证明。

On Corecursive Algebras for Functors Preserving Coproducts

For an endofunctor $H$ on a hyper-extensive category preserving countable coproducts we describe the free corecursive algebra on $Y$ as the coproduct of the final coalgebra for $H$ and the free $H$-algebra on $Y$. As a consequence, we derive that $H$ is a cia functor, i.e., its corecursive algebras are precisely the cias (completely iterative algebras). Also all functors $H(-) + Y$ are then cia functors. For finitary set functors we prove that, conversely, if $H$ is a cia functor, then it has the form $H = W \times (-) + Y$ for some sets $W$ and $Y$.

On free completely iterative algebras

For every finitary set functor F we demonstrate that free algebras carry a canonical partial order. In case F is bicontinuous, we prove that the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra. Moreover, the algebra structure of the latter is the unique continuous extension of the algebra structure of the free algebra. For general finitary functors the free algebra and the free completely iterative algebra are proved to be posets sharing the same conservative completion. And for every recursive equation e in the free completely iterative…

A New Foundation for Finitary Corecursion

This paper contributes to a theory of the behaviour of "finite-state" systems that is generic in the system type. We propose that such systems are modeled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint (LFF). We prove that if the given endofunctor preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adámek, Milius and Velebil). Mor…