Polynomial fixpoint equations and bialgebras of inductive datatypes
The combinatorial Dyson-Schwinger equations are fixpoint
equations, commonly formulated inside predefined
Connes-Kreimer-style Hopf algebras. Their solutions are
infinite series, which can be accessed and manipulated thanks to
their recursive structure, as exemplified by antipodes and BPHZ
renormalisation. The aim of this talk is to explain how
similar mechanisms play an important role in the foundations of
mathematics, more concretely in constructive type theory. Here
infinite structures are introduced in terms of syntactically
defined induction principles, which simultaneously specify how
terms can be constructed and how they can be accessed. The
fundamental example is the set of natural numbers and ordinary
induction. The induction principles are specified in terms of
the basic type constructors: dependent sums and dependent
products. In the categorical semantics, these are polynomial
endofunctors, and the resulting inductive type is interpreted as
the least fixpoint of the endofunctor (initial algebra).
Combinatorially, the datatypes are always some kind of tree
structures, and they always generate a graded bialgebra
containing a canonical copy of the Faa di Bruno bialgebra.
The recent homotopy interpretation of type theory facilitates
the handling of symmetries, so as to make formal sense of the
statement that Feynman graphs are inductive datatypes.