In this work, we study reduction monads, which are essentially the same as monads relative to the free functor from sets into graphs. Reduction monads abstract two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, it is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented graph whose vertices are terms and whose edges witness the reductions between two terms.

We study presentations of reduction monads. To this end, we propose a notion of reduction signature. As usual, such a signature plays the rôle of a virtual presentation, and specifies arities for generating operations—possibly subject to equations—together with arities for generating reduction rules. For each such signature, we define a category of models. Any model is, in particular, a reduction monad, and, in the spirit of Initial Semantics, we define the reduction monad presented (or specified) by the given reduction signature to be, if it exists, the initial object of this category of models.

Our main result identifies a class of reduction signatures which specify a reduction monad in the above sense. In particular, the lambda calculus is naturally specified by such a signature.