License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.6
URN: urn:nbn:de:0030-drops-105136
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10513/
Go to the corresponding LIPIcs Volume Portal

Ahrens, Benedikt ; Hirschowitz, André ; Lafont, Ambroise ; Maggesi, Marco

Modular Specification of Monads Through Higher-Order Presentations

pdf-format:
LIPIcs-FSCD-2019-6.pdf (0.6 MB)

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 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.

BibTeX - Entry

@InProceedings{ahrens_et_al:LIPIcs:2019:10513,
  author =	{Benedikt Ahrens and Andr{\'e} Hirschowitz and Ambroise Lafont and Marco Maggesi},
  title =	{{Modular Specification of Monads Through Higher-Order Presentations}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10513},
  URN =		{urn:nbn:de:0030-drops-105136},
  doi =		{10.4230/LIPIcs.FSCD.2019.6},
  annote =	{Keywords: free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computer-checked proofs}
}

Keywords: free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computer-checked proofs
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019
Supplementary Material: Computer-checked proofs with compilation instructions on https://github.com/UniMath/largecatmodules/tree/50fd617.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI