symmetric monoidal (∞,1)-category of spectra
An initial algebra for an endofunctor on a category is an initial object in the category of algebras of . These play a role in particular as the categorical semantics for inductive types.
The concept of an algebra of an endofunctor is arguably somewhat odd, a more natural concept being that of an algebra over a monad. However, the former can often be reduced to the latter.
If is a complete category, then the category of algebras of an endofunctor is equivalent to the category of algebras over a monad of the free monad on , if the latter exists.
The proof is fairly straightforward, see for instance (Maciej) or at free monad.
The existence of free monads, on the other hand, can be a tricky question. One general technique is the transfinite construction of free algebras.
If has an initial algebra , then is isomorphic to via .
In this sense, is a fixed point of . Being initial, is the smallest fixed point of in that there is a map from to any other fixed point (indeed, any other algebra), and this map is an injection if is Set.
The dual concept is terminal coalgebra, which is the largest fixed point of .
Given an initial algebra structure , define an algebra structure on to be . By initiality, there exists an -algebra map , so that
commutes. Now it is trivial, in fact tautological that is itself an -algebra map . Thus , since both sides of the equation are -algebra maps and is initial. As a result, , so that according to the commutative square. Hence is an isomorphism, with inverse .
In many cases, initial algebras can be constructed in a recursive/iterative fashion using Adámek's fixed point theorem.
Initial algebras of endofunctors provide categorical semantics for extensional inductive types. The generalization to weak initial algebras captures the notion in intensional type theory and homotopy type theory.
The archetypical example of an initial algebra is the set of natural numbers natural numbers object.
Let be topos and let the functor given by
(i.e. the functor underlying the “maybe monad”). Then an initial algebra over is precisely a natural number object in .
By definition, an -algebra is an object equipped with a morphism
hence equivalently with a point and an endomorphism . Initiality means that for any other -algebra , there is a unique morphism such that the diagram
commutes. This is the very definition of natural number object .
Another example of an initial algebra is the bi-pointed set .
Let be topos and let the functor given by
Then an initial algebra over is precisely a bi-pointed object in .
Theorem applies (in particular) to any functor which is a colimit of finitely representable functors , as in the following examples.
Let be a set, and let be the functor . Then the initial -algebra is , the free monoid on . The -algebra structure is
where is the identity and is the restriction of the monoid multiplication along the evident inclusion .
This “fixed point” of can be thought of as the result of the (slightly nonsensical) calculation
which can be made rigorous by interpreting the initial equality as defining the solution by recursion, and applying the theorem above.
Let be the functor . Then the initial -algebra is the set of isomorphism classes of finite (planar, rooted) binary trees. The -algebra structure is
where names the tree consisting of just a root vertex, and creates a tree from two trees , by joining their roots to a new root, so that the root of becomes the left child and the root of the right child of the new root.
The recursive equation
would seem to imply that the structure behaves something like a structural “sixth root of unity”, and indeed the structural isomorphism allows one to exhibit an isomorphism
constructively, as famously explored by Andreas Blass in the paper “Seven trees in one”.
Let be the functor (the free monoid from an earlier example). Then the initial -algebra is the set of isomorphism classes of finite planar rooted trees (not necessarily binary as in the previous example).
Let be the coslice category , and let be the functor which pushes out along the multiplication-by- map . Then the initial -algebra is the Pruefer group . See the discussion at the n-Category Café, starting here.
Let be the category of complex Banach spaces and maps of norm bounded above by , and let be the squaring functor . Then the initial -algebra is (with respect to the usual Lebesgue measure). This result is due to Tom Leinster; see this MathOverflow discussion.
A list of notable endofunctors, and their initial algebras/terminal coalgebras.
Nonexistent (co)algebras are labelled with ‘/’, and unknown ones with ‘?’.
Base category | Endofunctor | Initial Algebra | Final Coalgebra | Note, reference |
---|---|---|---|---|
Set | Const | |||
Set | ||||
Set | Conatural numbers | extended natural number | ||
Set | , ie conatural numbers “terminated” (when they aren’t ) with | partial map classifier | ||
Set | or | (i.e. one definition of Stream ) | ||
Set | (i.e. one definition of Stream ) | sequence, writer monad, stream | ||
Set | or | 1 (the unique infinite unlabelled binary tree) | ||
Set | 1 | reader monad | ||
Set | List | another definition of Stream ; i.e. potentially infinite List | list, stream | |
Set | Finite binary tree with -labelled nodes | Potentially infinite binary tree with -labelled nodes | tree | |
Set | Finite -ary tree with -labelled nodes and -labelled leaves | Potentially infinite -ary tree with -labelled nodes with and -labelled leaves | ||
Set | Finite tree with -labelled nodes and -labelled leaves | Potentially infinite tree with -labelled nodes with and -labelled leaves | The number of subtrees is not fixed to a particular , it could be any number | |
Set | Potentially infinite Moore machine | |||
Set | Potentially infinite Mealy machine | |||
Set | / | / | ||
Set | Finite rooted forests | Potentially infinite finitely-branching rooted forests | ||
Set | polynomial endofunctor | W-type | M-type | |
Bipointed Sets | dyadic rational numbers in the interval | The closed interval | coalgebra of the real interval | |
linearly ordered sets | , where is the cartesian product of the natural numbers with the underlying set of , equipped with the lexicographic order. | The non-negative real numbers | real number | |
Archimedean ordered fields | the identity functor | The rational numbers | The real numbers | |
Archimedean ordered fields | where is the Archimedean ordered field of two-sided Dedekind cuts of | The real numbers | The real numbers | |
Archimedean ordered fields | where is the quotient of Cauchy sequences in the Archimedean ordered field | The HoTT book real numbers | The Dedekind real numbers | These are the same objects in the presence of excluded middle or countable choice. |
Any category | The constant functor given object | |||
Any category | The identity functor | initial object | terminal object | |
Any extensive category | given terminal object and coproduct | natural numbers object | ? | |
Any closed abelian category | given tensor unit , tensor product , coproduct , and object | tensor algebra of | cofree coalgebra over | tensor algebra, cofree coalgebra |
-Grpd | sphere spectrum | ? | suspension |
A textbook account of the basic theory is in Chapter 10 of
The relation to free monads is discussed in
Original references on initial algebras include
Věra Pohlová. “On sums in generalized algebraic categories.” Czechoslovak Mathematical Journal 23.2 (1973): 235-251. http://eudml.org/doc/12718.
Jiří Adámek, Free algebras and automata realizations in the language of categories, Commentationes Mathematicae Universitatis Carolinae 15.4 (1974): 589-602.
Jiří Adámek, Věra Trnková, Automata and algebras in categories Vol. 37. Springer Science & Business Media, 1990.
The observation that the categorical semantics of well-founded inductive types (-types) is given by initial algebras over polynomial endofunctors on the type system:
Peter Dybjer, Representing inductively defined sets by wellorderings in Martin-Löf’s type theory, Theoretical Computer Science 176 1–2 (1997) 329-335 doi:10.1016/S0304-3975(96)00145-4
Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories, Annals of Pure and Applied Logic 104 1-3 (2000) 189-218 doi:10.1016/S0168-0072(00)00012-9
Further discussion:
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Containers: Constructing strictly positive types, Theoretical Computer Science 342 1 (2005) 3-27 doi:10.1016/j.tcs.2005.06.002
Benno van den Berg, Ieke Moerdijk, -types in sheaves [arXiv:0810.2398]
Generalization to inductive families (dependent -types):
Nicola Gambino, Martin Hyland, Wellfounded Trees and Dependent Polynomial Functors, in: Types for Proofs and Programs TYPES 200, Lecture Notes in Computer Science 3085, Springer (2004) doi:10.1007/978-3-540-24849-1_14
Michael Abbott, Thorsten Altenkirch, Neil Ghani: Representing Nested Inductive Types using W-types, in: Automata, Languages and Programming, ICALP 2004, Lecture Notes in Computer Science, 3142, Springer (2004) doi:10.1007/978-3-540-27836-8_8, pdf
exposition: Inductive Types for Free – Representing nested inductive types using W-types, talk at ICALP (2004) pdf
Generalization to homotopy-initial algebras as categorical semantics for -types in homotopy type theory:
Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICS’12: (2012) 95–104 arXiv:1201.3898, doi:10.1109/LICS.2012.21, Coq code
Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 arXiv:1307.2765, doi:10.1017/S0960129514000516
Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31–42 arXiv:1402.0761, doi:10.1145/2775051.2676983
Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1–45 arXiv:1504.05531, doi:10.1145/3006383
Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 [arXiv:1307.2765, doi:10.1017/S0960129514000516]
Towards combining generalization to dependent and homotopical W-types:
Last revised on July 10, 2024 at 00:05:42. See the history of this page for a list of all contributions to it.