Initial algebra

Summary

An initial algebra of an endofunctor $F$ is an F-algebra from which there is exactly one homomorphism to every other $F$-algebra. It is unique up to unique isomorphism, and by Lambek's lemma its structure map is an isomorphism, so it is a fixed point of $F$. Initial algebras give a uniform account of inductive definitions and of definitions by recursion. The unique homomorphism out of the initial algebra is the function defined by structural recursion. For a signature, the initial algebra is the term algebra, which is the basis of initial algebra semantics for abstract data types.