The Berry Order (ideas from 1980s stable domain theory)

Add to your list(s) Download to your calendar using vCal

• Paul Taylor (University of Birmingham)
• Friday 11 March 2022, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact George Kaye.

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

Abstract

Besides Joyal’s “species”, the influences on work akin to polynomial functors in the 1980s were Diers’ “multiadjoints”, Berry’s initial investigations of “sequential programs” and Girard’s adaptation of this to the semantics of “System F”.

Using Berry’s term “stable domain theory”, Lamarche and I constructed numerous cartesian closed (bi)categories of categories and pullback-preserving functors, looking for better models of polymorphism.

In these, the order between maps is not pointwise but the “Berry order”; for categories the naturality squares must be pullbacks, so these were called “cartesian transformations”.

The function-spaces turn out to have a simpler representation than in “Scott” domain theory. This uses what Berry and Girard called the “trace”, which consists of the multiple universal (unit) maps from Diers’ theory, which I called “candidates”.

The one theorem that I shall prove is that the trace provides a factorisation system for stable functors. The “epis” are functors with (single) left adjoints and the “monos” are those which are equivalences on slices. The latter are essentially fibrations whose fibres are groupoids.

The different “flavours” of stable domains are measured by the properties of their slices (including familiar notions from categorical logic for no obvious reason) and the complexity of the “multicolimits” – both their cardinality and the kinds of groups that are involved.

A lot of this material was not written up properly, so there there is a goldmine waiting for younger researchers to develop. For example, Gabriel-Ulmer duality between LFP and lex categories can be extended to “disjunctive” theories. Also, the similarity between (bi)categories of domains and the domains themselves that was used to model System F might be adapted to finding models of univalence in HoTT.

Achim Jung has kindly agreed to chair this talk.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.