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 β- and η-equalities. Such a 2-signature is hence a pair (Σ,E) of a binding signature Σ and a family E of equations for Σ. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context. We associate, to each 2-signature (Σ,E), a category of “models of (Σ,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.
Modular Specification of Monads Through Higher-Order Presentations / Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco maggesi. - ELETTRONICO. - 131:(2019), pp. 1-19. (Intervento presentato al convegno FSCD 2019 International Conference on Formal Structures for Computation and Deduction tenutosi a Dortmund, Germany nel June 24-30,2019) [10.4230/LIPIcs.FSCD.2019.6].
Modular Specification of Monads Through Higher-Order Presentations
Benedikt Ahrens;Marco maggesi
2019
Abstract
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 β- and η-equalities. Such a 2-signature is hence a pair (Σ,E) of a binding signature Σ and a family E of equations for Σ. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context. We associate, to each 2-signature (Σ,E), a category of “models of (Σ,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.File | Dimensione | Formato | |
---|---|---|---|
LIPIcs-FSCD-2019-6.pdf
accesso aperto
Descrizione: Versione pubblicata online dall'editore
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Creative commons
Dimensione
651.55 kB
Formato
Adobe PDF
|
651.55 kB | Adobe PDF | |
1903.00922.pdf
accesso aperto
Descrizione: Versione ArXiv 2019-03-03
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
Open Access
Dimensione
658.04 kB
Formato
Adobe PDF
|
658.04 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.