nLab second order algebraic theory

Idea

A second-order algebraic theory is a generalization of the notion of Lawvere theory to describe algebraic structures with variable binding.

While single-sorted Lawvere theories are cartesian monoidal categories generated from a single object, single-sorted second-order algebraic theories are cartesian monoidal categories generated from a single exponentiable object.

Definition

A second-order algebraic theory is a category $T$ with cartesian products and an exponentiable object $o$ such that every object of $T$ is isomorphic to a finite cartesian product of objects of the form $o^n \Rightarrow o$.

A model of a theory $T$ is given by a functor $M : T \to \Set$ that preserves cartesian products (not necessarily exponentials). On objects, such a functor must give for each $o^n \Rightarrow o$ a set $M(n)$ and the functoriality determines a first-order Lawvere theory/cartesian multicategory structure on $M$. So models of second order algebraic theories are first order algebraic theories with additional structure.

Multicategory

Just as Lawvere theories can be identified with cartesian multicategories, there should be a similar correspondence between second-order theories and some notion of second-order cartesian multicategory.

Examples

• The untyped lambda calculus can be described as a second-order algebraic theory, and simply typed lambda calculus as a multi-sorted second-order theory.

• The calculus of derivatives or more generally partial derivatives.

References

• Marcelo Fiore and Chung-Kil Hur, Term Equational Systems and Logics, MFPS XXIV, doi

• Marcelo Fiore and Ola Mahmoud, Second-order Algebraic Theories, MFCS 2010, arxiv

A formalization in Agda:

• Marcelo Fiore and Dmitrij Szamozvancev: webpage with an accompanying talk.

Discussion via monads:

• Nathanael Arkor, Monadic and Higher-Order Structure, PhD thesis, Cambridge (2022) [doi:10.17863/CAM.86347, pdf, pdf]