Kestrel Institute - Research Staff - Dusko Pavlovic

Home : Research Staff : Dusko Pavlovic : Coalgebra

Coalgebra

1998

Calculus in coinductive form --- with Martin Escardo

Abstract

Coinduction is often seen as a way of implementing infinite objects. Since real numbers are typical infinite objects, it may not come as a surprise that calculus, when presented in a suitable way, is permeated by coinductive reasoning. What is surprising is that mathematical techniques, recently developed in the context of computer science, seem to be shedding a new light on some basic methods of calculus.

We introduce a coinductive formalization of elementary calculus that can be used as a tool for symbolic computation, and geared towards computer algebra and theorem proving. So far, we have covered ordinary differential and difference equations, Taylor series, Laplace transform and the basics of operator calculus.

Guarded induction on final coalgebras

Abstract

We make an initial step towards categorical semantics of guarded induction. While ordinary induction is usually modelled in terms of least fixpoints and initial algebras, guarded induction is based on unique fixpoints of certain operations, called guarded, on final coalgebras. So far, such operations were treated syntactically. We analyse them categorically. Guarded induction appears as couched in coinduction.

The applications of the presented categorical analysis span across the gamut of the applications of coinduction, from modelling of computation to solving differential equations. A subsequent paper will provide an account of some domain theoretical aspects, which are presently left implicit.

1999

On coalgebra of real numbers --- with Vaughan Pratt

Abstract

We define the continuum up to order isomorphism (and hence homeomorphism) as the final coalgebra of the functor capturing the ordinal product with omega. This makes an attractive analogy with the definition of the ordinal omega itself as the initial algebra of the functor prepending the unity, with both definitions made in the category of posets. The variants of these functors yield respectively Cantor space (surplus rationals), Baire space (no rationals), and again the continuum as their final coalgebras.

2001

Categories of processes enriched in final coalgebras --- with Sava Krstic and John Launchbury

Abstract

Simulations between processes can be understood in terms of coalgebra homomorphisms, with homomorphisms to the final coalgebra exactly identifying bisimilar processes. The elements of the final coalgebra are thus natural representatives of bisimilarity classes, and a denotational semantics of processes can be developed in a final-coalgebra-enriched category where arrows are processes, canonically represented.

In the present paper, we describe a general framework for building final-coalgebra-enriched categories. Every such category is constructed from a multivariant functor representing a notion of process, much like Moggi's categories of computations arising from monads as notions of computation. The "notion of process" functors are intended to capture different flavors of processes as dynamically extended computations. These functors may involve a computational (co)monad, so that a process category in many cases contains an associated computational category as a retract. We further discuss categories of resumptions and of hyperfunctions, which are the main examples of prcess categories. Very informally, resumptions can be understood as computations extended in time, whereas hypercomputations are extended in space.

2002

The continuum as a final coalgebra --- with Vaughan Pratt

Abstract

We define the continuum in terms of the final coalgebras of simple functors: either the functor N×X , mapping the sets X into their products with the set of natural numbers, or the functor 1+N ×X. This makes an attractive analogy with the definition of N itself as the initial algebra of the functor 1+X, which adds a singleton to each set X. We furthermore characterize Baire space and Cantor space in terms of these final coalgebras.

The presented coalgebraic approach leads to coinductive definitions of these infinitary concepts both in the category of sets, and in the category of posets. We analyze the structural differences that arise, and conclude with some paradoxical discrepancies between continuity and constructiveness in this setting.

- Back to Top -

- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -