Comodule representations of Second-order functionals

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

• Andrej Bauer, University of Ljubljana
• Wednesday 01 May 2024, 10:00-11:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Jon Sterling.

Note the unusual date and time.

In information-theoretic terms, a map is continuous when a finite amount of information about the input suffices for computing a finite amount of information about the output. Already Brouwer observed that this allows one to represent a continuous functional from sequences to numbers with a certain well-founded question-answer tree. The idea has been extended to other kinds of second-order functionals, such as stream transformers, continuous functionals on final coalgebras, sequentially realizable functionals, and others.

In type theory a second-order functional is a map F : (∏(a : A), P a) → (∏(b : B) → Q b). Its continuity is once again witnessed by a well-founded tree whose nodes are “questions” a : A, the branches are indexed by “answers” P a, and the leaves are “results” Q b. Such tree representations can be expressed in purely category-theoretic terms, using the notion of right T-comodules for the monad T of well-founded trees on the category of containers. Doing so exposes a rich underlying structure, and immediately suggests generalizations: any right T-comodule for any monad T on containers gives rise to a representation theorem for second-order functionals. We give several examples of these.

Joint work with Danel Ahman, University of Tartu, https://danel.ahman.ee/

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.