Other Computer Engineering Commons^™

Approximation Of Nested Fixpoints, Alexander Kurz

Engineering Faculty Articles and Research

The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is …

Coalgebraic Semantics Of Reflexive Economics (Dagstuhl Seminar 15042), Samson Abramsky, Alexander Kurz, Pierre Lescanne, Viktor Winschel

Engineering Faculty Articles and Research

This report documents the program and the outcomes of Dagstuhl Seminar 15042 “Coalgebraic Semantics of Reflexive Economics”.

Presenting Distributive Laws, Marcello M. Bonsangue, Helle H. Hansen, Alexander Kurz, Jurriaan Rot

Engineering Faculty Articles and Research

Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation …

Relation Lifting, With An Application To The Many-Valued Cover Modality, Marta Bílková, Alexander Kurz, Daniela Petrişan, Jirí Velebil

Engineering Faculty Articles and Research

We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the “powerset monad” on categories, one is the preservation by T of “exactness” of certain squares. Both characterisations are generalisations of the “classical” results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks.

The results presented in this paper …

Completeness For The Coalgebraic Cover Modality, Clemens Kupke, Alexander Kurz, Yde Venema

Engineering Faculty Articles and Research

We study the finitary version of the coalgebraic logic introduced by L. Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a so-called coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation.

As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically valid inequalities. Our soundness and completeness proof is algebraic, …

Coalgebraic Logics (Dagstuhl Seminar 12411), Ernst-Erich Doberkat, Alexander Kurz

Engineering Faculty Articles and Research

This report documents the program and the outcomes of Dagstuhl Seminar 12411 “Coalgebraic Logics”. The seminar deals with recent developments in the area of coalgebraic logic, a branch of logics which combines modal logics with coalgebraic semantics. Modal logic finds its uses when reasoning about behavioural and temporal properties of computation and communication, coalgebras have evolved into a general theory of systems. Consequently, it is natural to combine both areas for a mathematical description of system specification. Coalgebraic logics are closely related to the broader categories semantics/formal methods and verification/logic.

On Coalgebras Over Algebras, Adriana Balan, Alexander Kurz

Engineering Faculty Articles and Research

We extend Barr’s well-known characterization of the final coalgebra of a Set-endofunctor as the completion of its initial algebra to the Eilenberg-Moore category of algebras for a Set-monad M for functors arising as liftings. As an application we introduce the notion of commuting pair of endofunctors with respect to the monad M and show that under reasonable assumptions, the final coalgebra of one of the endofunctors involved can be obtained as the free algebra generated by the initial algebra of the other endofunctor.

Equational Coalgebraic Logic, Alexander Kurz, Raul Leal

Engineering Faculty Articles and Research

Coalgebra develops a general theory of transition systems, parametric in a functor T; the functor T specifies the possible one-step behaviours of the system. A fundamental question in this area is how to obtain, for an arbitrary functor T, a logic for T-coalgebras. We compare two existing proposals, Moss’s coalgebraic logic and the logic of all predicate liftings, by providing one-step translations between them, extending the results in [21] by making systematic use of Stone duality. Our main contribution then is a novel coalgebraic logic, which can be seen as an equational axiomatization of Moss’s logic. The three logics are …

Functorial Coalgebraic Logic: The Case Of Many-Sorted Varieties, Alexander Kurz, Daniela Petrişan

Engineering Faculty Articles and Research

Following earlier work, a modal logic for T-coalgebras is a functor L on a suitable variety. Syntax and proof system of the logic are given by presentations of the functor. This paper makes two contributions. First, a previous result characterizing those functors that have presentations is generalized from endofunctors on one-sorted varieties to functors between many-sorted varieties. This yields an equational logic for the presheaf semantics of higher-order abstract syntax. As another application, we show how the move to functors between many-sorted varieties allows to modularly combine syntax and proof systems of different logics. Second, we show how to associate …

Algebraic Semantics For Coalgebraic Logics, Clemens Kupke, Alexander Kurz, Dirk Pattinson

Engineering Faculty Articles and Research

With coalgebras usually being defined in terms of an endofunctor T on sets, this paper shows that modal logics for T-coalgebras can be naturally described as functors L on boolean algebras. Building on this idea, we study soundness, completeness and expressiveness of coalgebraic logics from the perspective of duality theory. That is, given a logic L for coalgebras of an endofunctor T, we construct an endofunctor L such that L-algebras provide a sound and complete (algebraic) semantics of the logic. We show that if L is dual to T, then soundness and completeness of the algebraic semantics immediately yield the …

Coalgebras And Modal Expansions Of Logics, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

In this paper we construct a setting in which the question of when a logic supports a classical modal expansion can be made precise. Given a fully selfextensional logic S, we find sufficient conditions under which the Vietoris endofunctor V on S-referential algebras can be defined and we propose to define the modal expansions of S as the logic that arises from the V-coalgebras. As an example, we also show how the Vietoris endofunctor on referential algebras extends the Vietoris endofunctor on Stone spaces. From another point of view, we examine when a category of ‘spaces’ (X,A), ie sets X …

Stone Coalgebras, Clemens Kupke, Alexander Kurz, Yde Venema

Engineering Faculty Articles and Research

In this paper we argue that the category of Stone spaces forms an interesting base category for coalgebras, in particular, if one considers the Vietoris functor as an analogue to the power set functor. We prove that the so-called descriptive general frames, which play a fundamental role in the semantics of modal logics, can be seen as Stone coalgebras in a natural way. This yields a duality between the category of modal algebras and that of coalgebras over the Vietoris functor. Building on this idea, we introduce the notion of a Vietoris polynomial functor over the category of Stone spaces. …

Definability, Canonical Models, And Compactness For Finitary Coalgebraic Modal Logic, Alexander Kurz, Dirk Pattinson

Engineering Faculty Articles and Research

This paper studies coalgebras from the perspective of the finitary observations that can be made of their behaviours. Based on the terminal sequence, notions of finitary behaviours and finitary predicates are introduced. A category Behω(T) of coalgebras with morphisms preserving finitary behaviours is defined. We then investigate definability and compactness for finitary coalgebraic modal logic, show that the final object in Behω(T) generalises the notion of a canonical model in modal logic, and study the topology induced on a coalgebra by the finitary part of the terminal sequence.