2026-07-22T19:33:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10513 2024-03-06T10:46:06Z ddc:004 open_access

Modular Specification of Monads Through Higher-Order Presentations Ahrens, Benedikt Hirschowitz, André Lafont, Ambroise Maggesi, Marco free monads presentation of monads initial semantics signatures syntax monadic substitution computer-checked proofs In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of "models", and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair. In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating ("higher-order") operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to beta- and eta-equalities. Such a 2-signature is hence a pair (Sigma,E) of a binding signature Sigma and a family E of equations for Sigma. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context. We associate, to each 2-signature (Sigma,E), a category of "models of (Sigma,E)"; and we say that a 2-signature is "effective" if this category has an initial object; the monad underlying this (essentially unique) object is the "monad specified by the 2-signature". Not every 2-signature is effective; we identify a class of 2-signatures, which we call "algebraic", that are effective. Importantly, our 2-signatures together with their models enjoy "modularity": when we glue (algebraic) 2-signatures together, their initial models are glued accordingly. We provide a computer formalization for our main results. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benedikt Ahrens and André Hirschowitz and Ambroise Lafont and Marco Maggesi 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.6 urn:nbn:de:0030-drops-105136 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.6 eng https://creativecommons.org/licenses/by/3.0/legalcode