Online seminář z algebry - 13.5.2021 PDF Tisk

Další seminář z algebry se koná 13.5.2021 od 13.00 online na platformě ZOOM. Informace pro připojení a další program semináře je zde.

Nathanael Arkor

Higher-order algebraic theories and relative monads

There have traditionally been two ways to reason about universal algebraic structure categorically: via algebraic theories, and via monads. It is well known that the two are tightly related: in particular, there is a correspondence between algebraic theories and a  class of monads on the category of sets.

Motivated by the study of simple type theories, Fiore and Mahmoud introduced second-order algebraic theories, which extend classical (first-order) algebraic theories by variable-binding operators, such as the existential quantifier ∃x of first-order logic; the differential operators d/dx analysis; and the λ-abstraction operator of the untyped λ-calculus. Fiore and Mahmoud estab- lished a correspondence between second-order algebraic theories and a second-order equational logic, but did not pursue a general understanding of the categorical structure of second-order algebraic theories. In particular, the possibility of a  monad–theory correspondence for second- order algebraic theories was left as an open question.

In this talk, I will present a generalisation of algebraic theories to higher-order structure, in particular subsuming the second-order algebraic theories of Fiore and Mahmoud, and describe a universal property of the category of nth-order algebraic theories. The central result is a correspondence between (n + 1)th-order algebraic theories and a class of relative monads on the category of nth-order algebraic theories, which extends to a monad correspondence subsuming that of the classical setting. Finally, I will discuss how the perspective lent by higher-order algebraic theories sheds new light on the classical monad–theory correspondence.

This is a report on joint work with Dylan McDermott.

Aktualizováno Středa, 12 Květen 2021 15:32