Categorical recursion: 1990s workPaul Taylor |
All of the work described on this page has been superseded by more recent material.
Principal influences — My book — Intuitionistic Sets and Ordinals — Towards a Unified Treatment of Induction — The Fixed Point Property in Synthetic Domain Theory.
Miscellaneous slides from several lectures given in the 1990s, in no particular order.
Important influences behind my work were
André Joyal and Ieke Moerdijk gave a different point of view on these matters in their book Algebraic Set Theory (CUP 1995, ISBN 0-521-55830-1) and this was developed by several other authors.
When I was writing my book Practical Foundations of Mathematics I hoped to include an account of transfinite recursion over the ordinals that would be intuitionistic and naturally expressed in terms of category theory.
Journal of Symbolic Logic, 61 (1996) 705–744
Presented at Category Theory and Computer Science 5, Amsterdam, September 1993.
Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality.
We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifies the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals grow very rapidly.
Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it.
We treat ordinals as order-types, and develop a corresponding set theory similar to Osius’ transitive set objects. This presents Mostowski’s theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski’s theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank.
The comparison between sets and toposes is developed as far as the identification of replacement with completeness and there are some suggestions for further work in this area.
Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x≤ s x, monotonicity or s(x∨ y)≤ s x∨ s y.
Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result.
This manuscript is obsolete and only included here for the historical record. All of the material in it is superseded by Well founded coalgebras and recursion.
Presented at
Presented at Logic in Computer Science 6, Amsterdam, July 1991.
We present an elementary axiomatisation of synthetic domain theory and show that it is sufficient to deduce the fixed point property and solve domain equations. Models of these axioms based on partial equivalence relations have received much attention, but there are also very simple sheaf models based on classical domain theory. In any case the aim of this paper is to show that an important theorem can be derived from an abstract axiomatisation, rather than from a particular model. Also, by providing a common framework in which both PER and classical models can be expressed, this work builds a bridge between the two.
This document was translated from LATEX by HEVEA.