Abstract:
The abstract mathematical structures known as coalgebras are of increasing
interest in computer science for their use in modelling certain types
of data structures and programs. Traditional algebraic methods describe
objects in terms of their construction, whilst coalgebraic methods describe
objects in terms of their decomposition, or observational behaviour. The
latter techniques are particularly useful for modelling infinite data structures
and providing semantics for object-oriented programming languages,
such as Java.
There have been many different logics developed for reasoning about
coalgebras of particular functors, most involving modal logic. We define
a modal logic for coalgebras of polynomial functors, extending Rößiger’s
logic [33], whose proof theory was limited to using finite constant sets,
by adding an operator from Goldblatt [11]. From the semantics we define
a canonical coalgebra that provides a natural construction of a final
coalgebra for the relevant functor. We then give an infinitary axiomatization
and syntactic proof relation that is sound and complete for functors
constructed from countable constant sets.
