
In this work, we study reduction monads , which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, the lambda calculus is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented multigraph 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 role 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. If the initial object of this category of models exists, we call it the reduction monad presented (or specified) by the given reduction signature . Our main result identifies a class of reduction signatures which specify a reduction monad in the above sense. We show in the examples that our approach covers several standard variants of the lambda calculus.
computer-checked proofs, FOS: Computer and information sciences, presentation of monads, Monads, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science - Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Reduction systems, initial semantics, Monads, Initial semantics, Higher-order languages, Reduction systems, Lambda calculus, monadic substitution, signatures, CCS Concepts: • Theory of computation → Equational logic and rewriting, Higher-order languages, Categorical semantics Additional Key Words and Phrases: Initial semantics, syntax, and phrases free monads, Lambda calculus, Programming Languages (cs.PL)
computer-checked proofs, FOS: Computer and information sciences, presentation of monads, Monads, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science - Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Reduction systems, initial semantics, Monads, Initial semantics, Higher-order languages, Reduction systems, Lambda calculus, monadic substitution, signatures, CCS Concepts: • Theory of computation → Equational logic and rewriting, Higher-order languages, Categorical semantics Additional Key Words and Phrases: Initial semantics, syntax, and phrases free monads, Lambda calculus, Programming Languages (cs.PL)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 4 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
