Motivated by the study of effectful programming languages and computations, we introduce a relational theory of monadic rewriting systems. The latter are rewriting systems whose notion of reduction is effectful, where effects are modelled as monads. Contrary to what happens in the ordinary operational semantics of monadic programming languages, defining meaningful notions of monadic rewriting turns out to problematic for several monads, including the distribution, powerset, reader, and global state monad. This raises the question of when monadic rewriting is possible. We answer that question by identifying a class of monads, known as weakly cartesian monads, that guarantee monadic rewriting to be well-behaved. In case monads are given as equational theories, as it is the case for algebraic effects, we also show that a sufficient condition to have a well-behaved notion of monadic rewriting is that all equations in the theory are linear. Finally, we apply the abstract theory of monadic rewriting systems to the call-by-value λ-calculus with algebraic effects, this way obtaining effectful (surface) standardisation and confluence theorems.

Gavazzo F., Faggian C. (2021). A Relational Theory of Monadic Rewriting Systems, Part i. New York : Institute of Electrical and Electronics Engineers Inc. [10.1109/LICS52264.2021.9470633].

A Relational Theory of Monadic Rewriting Systems, Part i

Gavazzo F.;
2021

Abstract

Motivated by the study of effectful programming languages and computations, we introduce a relational theory of monadic rewriting systems. The latter are rewriting systems whose notion of reduction is effectful, where effects are modelled as monads. Contrary to what happens in the ordinary operational semantics of monadic programming languages, defining meaningful notions of monadic rewriting turns out to problematic for several monads, including the distribution, powerset, reader, and global state monad. This raises the question of when monadic rewriting is possible. We answer that question by identifying a class of monads, known as weakly cartesian monads, that guarantee monadic rewriting to be well-behaved. In case monads are given as equational theories, as it is the case for algebraic effects, we also show that a sufficient condition to have a well-behaved notion of monadic rewriting is that all equations in the theory are linear. Finally, we apply the abstract theory of monadic rewriting systems to the call-by-value λ-calculus with algebraic effects, this way obtaining effectful (surface) standardisation and confluence theorems.
2021
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
1
14
Gavazzo F., Faggian C. (2021). A Relational Theory of Monadic Rewriting Systems, Part i. New York : Institute of Electrical and Electronics Engineers Inc. [10.1109/LICS52264.2021.9470633].
Gavazzo F.; Faggian C.
File in questo prodotto:
File Dimensione Formato  
On_Monadic_Rewriting_Systems__Part_I (5).pdf

Open Access dal 08/01/2022

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 648.44 kB
Formato Adobe PDF
648.44 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/834391
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact