Reduction Monads and Their Signatures
| Autor: | Marco Maggesi, Benedikt Ahrens, Ambroise Lafont, André Hirschowitz |
|---|---|
| Přispěvatelé: | University of Birmingham [Birmingham], Laboratoire Jean Alexandre Dieudonné (JAD), Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS), Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Laboratoire des Sciences du Numérique de Nantes (LS2N), Dipartimento di Matematica 'Ulisse Dini', Università degli Studi di Firenze = University of Florence [Firenze] (UNIFI), European Project: 637339,H2020 ERC,ERC-2014-STG,CoqHoTT(2015), Laboratoire Jean Alexandre Dieudonné (LJAD), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), IMT Atlantique (IMT Atlantique), Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Università degli Studi di Firenze = University of Florence (UniFI) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
FOS: Computer and information sciences
computer-checked proofs Class (set theory) presentation of monads Monads Computer science 0102 computer and information sciences 02 engineering and technology initial semantics 01 natural sciences Monads Initial semantics Higher-order languages Reduction systems Lambda calculus Reduction (complexity) Computer Science::Logic in Computer Science Mathematics::Category Theory 0202 electrical engineering electronic engineering information engineering Safety Risk Reliability and Quality and phrases free monads syntax ComputingMilieux_MISCELLANEOUS computer.programming_language Lambda calculus Functor Computer Science - Programming Languages Multigraph Substitution (algebra) Reduction systems [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering Monad (functional programming) Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES monadic substitution 010201 computation theory & mathematics signatures TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Higher-order languages CCS Concepts: • Theory of computation → Equational logic and rewriting Categorical semantics Additional Key Words and Phrases: Initial semantics computer Software Initial and terminal objects Programming Languages (cs.PL) |
| Zdroj: | Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages, ACM, 2020, pp.1-29. ⟨10.1145/3371099⟩ Proceedings of the ACM on Programming Languages, 2020, pp.1-29. ⟨10.1145/3371099⟩ |
| ISSN: | 2475-1421 |
| Popis: | 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. POPL 2020 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|