Initial Algebras of Terms with Binding and Algebraic Structure

Abstract

One of the many results which makes Joachim Lambek famous is: an initial algebra of an endofunctor is an isomorphism. This fixed point result is often referred to as “Lambek’s Lemma”. In this paper, we illustrate the power of initiality by exploiting it in categories of algebra-valued presheaves $\mathcal{E}{\kern-.2ex}\mathcal{M}(T)^{\mathbb{N}}$, for a monad T on Sets. The use of presheaves to obtain certain calculi of expressions (with variable binding) was introduced by Fiore, Plotkin, and Turi. They used set-valued presheaves, whereas here the presheaves take values in a category $\mathcal{E}{\kern-.2ex}\mathcal{M}(T)$ of Eilenberg-Moore algebras. This generalisation allows us to develop a theory where more structured calculi can be obtained. The use of algebras means also that we work in a linear context and need a separate operation ! for replication, for instance to describe strength for an endofunctor on $\mathcal{E}{\kern-.2ex}\mathcal{M}(T)$. We apply the resulting theory to give systematic descriptions of non-trivial calculi: we introduce non-deterministic and weighted lambda terms and expressions for automata as initial algebras, and we formalise relevant equations diagrammatically.