Modular specification of monads through higher-order presentations

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • Université Côte d’Azur, CNRS, LJAD, France
  • IMT Atlantique Inria, LS2N CNRS, France
  • Università degli Studi di Firenze, Italy

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.

Details

Original languageEnglish
Title of host publication4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
EditorsHerman Geuvers
Publication statusPublished - 1 Jun 2019
EventInternational Conference on Formal Structures for Computation and Deduction (FSCD 2019) - Dortmund, Germany
Duration: 24 Jun 201930 Jun 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume131
ISSN (Print)1868-8969

Conference

ConferenceInternational Conference on Formal Structures for Computation and Deduction (FSCD 2019)
CountryGermany
CityDortmund
Period24/06/1930/06/19

Keywords

  • free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computer-checked proofs, Computer-checked proofs, Monadic substitution, Presentation of monads, Initial semantics, Free monads, Signatures, Syntax

ASJC Scopus subject areas