RAIRO-Theor. Inf. Appl.
Volume 33, Number 4-5, July October 1999
|Page(s)||401 - 426|
|Published online||15 August 2002|
Final Dialgebras: From Categories to Allegories
School of Computer Science and IT, University
of Nottingham, Nottingham NG8 1BB, U.K.
2 Philips Research Laboratories, Prof. Holstlaan 4, 5656 AA Eindhoven, The Netherlands.
Revised: 29 April 1999
The study of inductive and coinductive types (like finite lists and streams, respectively) is usually conducted within the framework of category theory, which to all intents and purposes is a theory of sets and functions between sets. Allegory theory, an extension of category theory due to Freyd, is better suited to modelling relations between sets as opposed to functions between sets. The question thus arises of how to extend the standard categorical results on the existence of final objects in categories (for example, coalgebras and products) to their existence in allegories. The motivation is to streamline current work on generic programming, in which the use of a relational theory rather than a functional theory has proved to be desirable. In this paper, we define the notion of a relational final dialgebra and prove, for an important class of dialgebras, that a relational final dialgebra exists in an allegory if and only if a final dialgebra exists in the underlying category of maps. Instances subsumed by the class we consider include coalgebras and products. An important lemma expresses bisimulations in allegorical terms and proves this equivalent to Aczel and Mendler's categorical definition.
Mathematics Subject Classification: 68N05
Key words: Programming theory / theory of datatypes / inductive type / co-inductive type / relation algebra / category theory / allegory theory / generic programming / polytypic programming.
© EDP Sciences, 1999
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.