Higher-Order Algebraic Theories
Reykjavik University
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).