A metalanguage for guarded iteration - Goncharov, Sergey; Rauch, Christoph; Schröder, Lutz (Theoretical Computer Science, 2021)
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.
CRIS-Team Scopus Importer:2021-05-21
Keywords: Computational adequacy; Computational monads; Guarded iteration; Metalanguage

A Metalanguage for Guarded Iteration - Goncharov, Sergey; Rauch, Christoph; Schröder, Lutz (Theoretical Aspects of Computing - ICTAC 2018 (LNCS 11187), 2018)

Cheap CTL Compassion in NuSMV - Hausmann, Daniel; Litak, Tadeusz Michal; Rauch, Christoph; Zinner, Matthias (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2020)
We discuss expansions of with connectives able to express Streett fairness objectives for single paths. We focus on: (Extended) Streett-Fair inspired by a seminal paper of Emerson and Lei. Unlike several other fair extensions of, our entire formalism (not just a subclass of formulas in some canonical form) allows a succinct embedding into the-calculus, while being able to express concisely all relevant types of path-based fairness objectives. We implement our syntax in the well-known symbolic model checker NuSMV, consequently also implementing model checking with “compassion” objectives. Since the-calculus embedding requires only alternation depth two, the resulting specifications correspond to parity games with two priorities. This allows a comparison of the performance of our NuSM with existing parity game solvers (both explicit and symbolic). The advantages of the symbolic approach seem to extend to fair model checking.
CRIS-Team Scopus Importer:2020-02-18
Keywords: CTL; Fairness and compassion; Model checking; NuSMV; Parity games

Complete Elgot Monads and Coalgebraic Resumptions - Goncharov, Sergey; Milius, Stefan; Rauch, Christoph (Electronic Notes in Theoretical Computer Science, 2016)
Monads are used to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. Complete Elgot monads are monads that are equipped with a (uniform) iteration operator satisfying a set of natural axioms, which allows to model iterative computations just as abstractly. 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, which were previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of complete Elgot monads and their relationship with generalized coalgebraic resumption monads. We give a characterization of the Eilenberg-Moore algebras of the latter. In fact, we work more generally with Uustalu's parametrized monads; we introduce complete Elgot algebras for a parametrized monad and we prove that they form an Eilenberg-Moore category. This is further used for establishing a characterization of complete Elgot monads as those monads whose algebras are coherently equipped with the structure of complete Elgot algebras for the parametrized monads obtained from generalized coalgebraic resumption monads.
UnivIS-Import:2018-09-05:Pub.2016.tech.IMMD.profes_1.comple
Keywords: complete Elgot monads; complete Elgot algebras; resumption; coalgebra

Complete Elgot Monads and Coalgebraic Resumptions - Goncharov, Sergey; Milius, Stefan; Rauch, Christoph (MFPS XXXII, 2016)
<em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">Monads<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;"> are used to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">Complete Elgot monads<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;"> are monads that are equipped with a (<em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">uniform<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;">) <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">iteration operator<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;"> satisfying a set of natural axioms, which allows to model <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">iterative computations<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;"> just as abstractly. 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 <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">generalized coalgebraic resumption monads<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;">, which were previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of complete Elgot monads and their relationship with generalized coalgebraic resumption monads. We give a characterization of the Eilenberg-Moore algebras of the latter. In fact, we work more generally with Uustalu's <em style="border: 0px; font-size: 16px; margin: 0px; padding: 0px; vertical-align: baseline; font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; color: rgb(46, 46, 46); word-spacing: -1.24453px;">parametrized monads<span style="color: rgb(46, 46, 46); font-family: Arial, Helvetica, "Lucida Sans Unicode", "Microsoft Sans Serif", "Segoe UI Symbol", STIXGeneral, "Cambria Math", "Arial Unicode MS", sans-serif; font-size: 16px; word-spacing: -1.24453px;">; we introduce complete Elgot algebras for a parametrized monad and we prove that they form an Eilenberg-Moore category. This is further used for establishing a characterization of complete Elgot monads as those monads whose algebras are coherently equipped with the structure of complete Elgot algebras for the parametrized monads obtained from generalized coalgebraic resumption monads.
Keywords: Complete Elgot monad; complete Elgot algebra; resumption monad; uniform iteration

Generic Hoare Logic for Order-Enriched Effects with Exceptions - Rauch, Christoph; Goncharov, Sergey; Schröder, Lutz (Recent Trends in Algebraic Development Techniques: 23rd IFIP WG 1.3 International Workshop, WADT 2016, Revised Selected Papers, 2017)

Guarded and Unguarded Iteration for Generalized Processes - Goncharov, Sergey; Schröder, Lutz; Rauch, Christoph; Pirog, Maciej (Logical Methods in Computer Science, 2019)
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.
CRIS-Team WoS Importer:2019-08-13

Unguarded Recursion on Coinductive Resumptions - Goncharov, Sergey; Rauch, Christoph; Schröder, Lutz (Mathematical Foundations of Programming Semantics XXXI, MFPS 2015, 2015)
We study a model of side-effecting processes obtained by adjoining free operations to a monad modelling base effects by means of 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. Types 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.
Keywords: recursion; coalgebra; coinduction; complete Elgot monad; resumptions

Unguarded Recursion on Coinductive Resumptions - Goncharov, Sergey; Schröder, Lutz; Rauch, Christoph; Jakob, Julian (Logical Methods in Computer Science, 2018)
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 monad
Keywords: recursion; coalgebra; coinduction; complete Elgot monad; resumptions

Unifying Guarded and Unguarded Iteration - Goncharov, Sergey; Schröder, Lutz; Rauch, Christoph; Piróg, Maciej (Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), 2017)
Keywords: Recursion theory; equational theories; guarded recursion