Free algebras for functors, with not an ordinal in sight

Abstract: Martin Escardo challenged me to make Pataraia's fixed point theorem "predicative". Whilst I have never understood the motivation for that notion, I have eliminated one instance of impredicativity and isolated the infinitary aspects to a single specific directed join.

So then I looked for the categorical version. Pataraia's idea plays a quite small part: the construction uses ideas from categorical algebra since its origins, and if I were to credit one person it would be Joachim Lambek.

The problem breaks into two parts, one finitary and the other infinitary. The infinitary part says that the category of pointed endofunctors of a small category with coequalisers is filtered, so has a terminal object if the given category has the required filtered colimit. This is probably widely applicable as an alternative to transfinite methods.

The finitary construction is that of fragments of the initial algebra. It may be done in several ways, but one is to consider coalgebras for the given functor that are have a cone over all algebras for it. We identify a "special condition" that this construction satisfies and that ensures that the terminal endofunctor (applied to any object) yields the terminal object of the finitary category, which is the required initial algebra of the functor.

The hope is that a similar finitary category of partial models could be found for more complex systems of algebra and logic and that these would correspond to the intermediate stages in proof theoretic arguments for normalisation, cut elimination etc.

computational complexitydiscrete mathematicsformal languages and automata theorylogic in computer scienceprogramming languagescategory theorylogic

Audience: researchers in the topic

---

University of Birmingham theoretical computer science seminar

Series comments: Meeting ID: 818 7333 5084 ~ Password: 217

---