Reduction Monads and Their Signatures

Benedikt Ahrens, Andre Hirschowitz, Ambroise Lafont, Marco Maggesi

Research output: Contribution to journalConference articlepeer-review

2 Citations (Scopus)
120 Downloads (Pure)

Abstract

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.
Original languageEnglish
Article number31
Number of pages29
JournalProceedings of the ACM on Programming Languages
Volume4
Issue numberPOPL
DOIs
Publication statusPublished - 19 Jan 2020
Event47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020). - New Orleans, United States
Duration: 19 Jan 202025 Jan 2020

Keywords

  • Higher-order languages
  • Initial semantics
  • Lambda calculus
  • Monads
  • Reduction systems

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Fingerprint

Dive into the research topics of 'Reduction Monads and Their Signatures'. Together they form a unique fingerprint.

Cite this