4 Jun 2020, 14:00, online

Speaker

Dylan McDermott, Reykjavik University

Title

Higher-order algebraic theories

Abstract

First-order algebraic theories describe algebraic structures that can be presented by a collection of operators and equations. These were generalized by Fiore et al. to second-order algebraic theories, in which the operators can bind simple variables. Examples include lambda- abstraction in the untyped lambda-calculus, and quantification in first-order logic.

We generalize to higher-order theories, in which operators can bind variables of higher orders. I will explain a notion of nth-order Lawvere theory and some of its metatheory. In particular, I will describe a correspondence between (n+1)th-order Lawvere theories and certain monads on nth-order Lawvere theories, analogous to the correspondence between (monosorted) first-order theories and finitary monads on Set.

This is joint work with Nathanael Arkor (University of Cambridge).