Sergey Goncharov ; Lutz Schröder ; Christoph Rauch ; Julian Jakob - Unguarded Recursion on Coinductive Resumptions

lmcs:4773 - Logical Methods in Computer Science, August 27, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:10)2018
Unguarded Recursion on Coinductive ResumptionsArticle

Authors: Sergey Goncharov ; Lutz Schröder ORCID; Christoph Rauch ; Julian Jakob

    We study a model of side-effecting processes obtained by starting from a monad modelling base effects and adjoining free operations using a cofree coalgebra construction; one thus arrives at what one may think of as types of non-wellfounded side-effecting trees, generalizing the infinite resumption monad. Correspondingly, the arising monad transformer has been termed the coinductive generalized resumption transformer. Monads of this kind have received some attention in the recent literature; in particular, it has been shown that they admit guarded iteration. Here, we show that they also admit unguarded iteration, i.e. form complete Elgot monads, provided that the underlying base effect supports unguarded iteration. Moreover, we provide a universal characterization of the coinductive resumption monad transformer in terms of coproducts of complete Elgot monads.


    Volume: Volume 14, Issue 3
    Published on: August 27, 2018
    Accepted on: August 23, 2018
    Submitted on: August 23, 2018
    Keywords: Computer Science - Logic in Computer Science,F.3.2,F.3.3,D.3.3

    1 Document citing this article

    Consultation statistics

    This page has been seen 1211 times.
    This article's PDF has been downloaded 307 times.