Coalgebra
2009
A semantical approach to equilibria and rationality
Abstract
Game theoretic equilibria are mathematical expressions of rationality. Rational agents are used to model not only humans and their software representatives, but also organisms, populations, species and genes, interacting with each other and with the environment. Rational behaviors are achieved not only through conscious reasoning, but also through spontaneous stabilization at equilibrium points.
Formal theories of rationality are usually guided by informal intuitions, which are acquired by observing some concrete economic, biological, or network processes. Treating such processes as instances of computation, we reconstruct and refine some basic notions of equilibrium and rationality from the some basic structures of computation.
It is, of course, well known that equilibria arise as fixed points; the point is that semantics of computation of fixed points seems to be providing novel methods, algebraic and coalgebraic, for reasoning about them.
2007
Labelled Markov Processes as generalised stochastic relations
— with Michael Mislove and James Worrell
Abstract
Labelled Markov processes (LMPs) are labelled transition systems in which each transition has an associated probability. In this paper we present a universal LMP as the spectrum of a commutative C*-algebra consisting of formal linear combinations of labelled trees. This yields a simple trace-tree semantics for LMPs that is fully abstract with respect to probabilistic bisimilarity. We also consider LMPs with distinguished entry and exit points as stateful stochastic relations. This allows us to define a category LMP, with measurable spaces as objects and LMPs as morphisms. Our main result in this context is to provide a predicate-transformer duality for LMP that generalises Kozen’s duality for the category SRel of stochastic relations.
2006
Testing semantics: Connecting processes and process logics
— with Michael Mislove and James Worrell
Abstract
We propose a methodology based on testing as a framework to capture the interactions of a machine represented in a denotational model and the data it manipulates. Using a connection that models ma- chines on the one hand, and the data they manipulate on the other, test- ing is used to capture the interactions of each with the objects on the other side: just as the data that are input into a machine can be viewed as tests that the machine can be subjected to, the machine can be viewed as a test that can be used to distinguish data. This approach is based on generalizing from duality theories that now are common in semantics to logical connections, which are simply contravariant adjunctions. In the process, it accomplishes much more than simply moving from one side of a duality to the other; it faithfully represents the interactions that embody what is happening as the computation proceeds.
Our basic philosophy is that tests can be used as a basis for modeling interactions, as well as processes and the data on which they operate. In more abstract terms, tests can be viewed as formulas of process logics, and testing semantics connects processes and process logics, and assigns computational meanings to both.
2004
Duality for Labelled Markov Processes
— with Michael Mislove, Joel Ouaknine and James Worrell
Abstract
Labelled Markov processes (LMPs) are probabilistic labelled transition systems. In this paper we present a ‘universal’ LMP as the Stone-Gelfand-Naimark dual of a C*-algebra consisting of formal linear combinations of labelled trees. We characterize the state space of the universal LMP as the set of homomorphims from an ordered commutative monoid of labelled trees into the multiplicative unit interval. This yields a simple semantics for LMPs which is fully abstract with respect to probabilistic bisimilarity. We also consider LMPs with entry points and exit points in the framework of Elgot’s iterative theories. We define an iterative theory of LMPs by specifing its categorical dual: a category of commutative rings consisting of C*-algebras of trees and `shapely maps’ between them. We find that the basic operations for composing LMPs have simple definitions in the dual category.
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 NxX , mapping the sets X into their products with the set of natural numbers, or the functor 1+NxX. 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.
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.
2000
Process fusion
Abstract
The technique of build fusion, also known as deforestation, removes intermediate results in a composition involving the “build” of an initial (inductive, finite) data structure, followed by its consumption. Here we show that it is analogously possible to do process fusion, removing intermediate final (coinductive, potentially infinite) data passing between a producer and a consumer.
The key observation leading to our results is the fact that the Curry-Howard isomorphism, relating types to propositions, programs to proofs, and sequential composition to cut, extends to the correspondence of fusion to cut elimination. this simple idea gives us logical interpretations of the basic methods of generic and transformational programming. In the present paper, we provide a logical analysis of the general form of build fusion over the inductive data types, regular or nested. The analysis is based on a novel logical interpretation of parametricity in terms of the paranatural transformations, introduced in the paper. We extend it to cover process fusion on coinductive data types.
The results obtained are truly generic, in the sense of applying to all coinductive (final) data types, including nested ones, and allow a far wider range of optimizations than previously possible. By the standard embedding of initial into final data types, it also applies to arbitrary intial-final mixtures (e.g., infinitely unfolding trees of finite lists).
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.
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.