arXiv subjects

Christoph Rauch

Publications and source records attributed to Christoph Rauch.

4 recordsLinked to original sources

arXiv2021

A Metalanguage for Guarded Iteration

Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. In recent work, we have introduced an axiomatic notion of guardedness in symmetric monoidal categories, which serves as a unifying framework for various examples from program semantics, process algebra, and beyond. In the present paper, we propose a generic metalanguage for guarded iteration based on combining this notion with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. We give a generic (categorical) semantics of this language over a suitable class of strong monads supporting guarded iteration, and show it to be in touch with the standard operational behaviour of iteration by giving a concrete big-step operational semantics for a certain specific instance of the metalanguage and establishing soundness and (computational) adequacy for this case.

cs.LO↗

arXiv2019

Guarded and Unguarded Iteration for Generalized Processes

Models of iterated computation, such as (completely) iterative monads, often depend on a notion of guardedness, which guarantees unique solvability of recursive equations and requires roughly that recursive calls happen only under certain guarding operations. On the other hand, many models of iteration do admit unguarded iteration. Solutions are then no longer unique, and in general not even determined as least or greatest fixpoints, being instead governed by quasi-equational axioms. Monads that support unguarded iteration in this sense are called (complete) Elgot monads. Here, we propose to equip (Kleisli categories of) monads with an abstract notion of guardedness and then require solvability of abstractly guarded recursive equations; examples of such abstractly guarded pre-iterative monads include both iterative monads and Elgot monads, the latter by deeming any recursive definition to be abstractly guarded. Our main result is then that Elgot monads are precisely the iteration-congruent retracts of abstractly guarded iterative monads, the latter being defined as admitting unique solutions of abstractly guarded recursive equations; in other words, models of unguarded iteration come about by quotienting models of guarded iteration.

cs.LO↗

arXiv2018

Unguarded Recursion on Coinductive Resumptions

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.

cs.LO↗

arXiv2016

Complete Elgot Monads and Coalgebraic Resumptions

Monads are extensively used nowadays to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. It turns out that equipping a monad with a (uniform) iteration operator satisfying a set of natural axioms allows for modelling iterative computations just as abstractly. The emerging monads are called complete Elgot monads. It has been shown recently that extending complete Elgot monads with free effects (e.g. operations of sending/receiving messages over channels) canonically leads to generalized coalgebraic resumption monads, previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of the relationship between abstract complete Elgot monads and those that capture coalgebraic resumptions, by comparing the corresponding categories of (Eilenberg-Moore) algebras. To this end we first provide a characterization of the latter category; even more generally, we formulate this characterization in terms of Uustalu's parametrized monads. This is further used for establishing a characterization of complete Elgot monads as precisely those monads whose algebras are coherently equipped with the structure of algebras of coalgebraic resumption monads.

cs.LO↗