Showing 1–36 of 36 results for author: Goncharov, S

Big Steps in Higher-Order Mathematical Operational Semantics

Authors: Sergey Goncharov, Pouya Partow, Stelios Tsampas

Abstract: Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy. The latter one implements, in a self-contai… ▽ More Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy. The latter one implements, in a self-contained manner, such a strategy directly by relating a program to the net result of the evaluation process. The agreement between these two styles of semantics is one of the key pillars in operational reasoning on programs; however, such agreement is typically proven from scratch every time on a case-by-case basis. A general, abstract mathematical argument behind this agreement is up till now missing. We cope with this issue within the framework of higher-order mathematical operational semantics by providing an abstract categorical notion of big-step SOS, complementing the existing notion of abstract higher-order GSOS. Moreover, we introduce a general construction for deriving the former from the latter, and prove an abstract equivalence result between the two. △ Less

Submitted 1 June, 2025; originally announced June 2025.

Probabilistic Strategies: Definability and the Tensor Completeness Problem

Authors: Nathan Bowler, Sergey Goncharov, Paul Blain Levy

Abstract: Programs that combine I/O and countable probabilistic choice, modulo either bisimilarity or trace equivalence, can be seen as describing a probabilistic strategy. For well-founded programs, we might expect to axiomatize bisimilarity via a sum of equational theories and trace equivalence via a tensor of such theories. This is by analogy with similar results for nondeterminism, established previousl… ▽ More Programs that combine I/O and countable probabilistic choice, modulo either bisimilarity or trace equivalence, can be seen as describing a probabilistic strategy. For well-founded programs, we might expect to axiomatize bisimilarity via a sum of equational theories and trace equivalence via a tensor of such theories. This is by analogy with similar results for nondeterminism, established previously. While bisimilarity is indeed axiomatized via a sum of theories, and the tensor is indeed at least sound for trace equivalence, completeness in general, remains an open problem. Nevertheless, we show completeness in the case that either the probabilistic choice or the I/O operations used are finitary. We also show completeness up to impersonation, i.e. that the tensor theory regards trace equivalent programs as solving the same system of equations. This entails completeness up to the cancellation law of the probabilistic choice operator. Furthermore, we show that a probabilistic trace strategy arises as the semantics of a well-founded program iff it is victorious. This means that, when the strategy is played against any partial counterstrategy, the probability of play continuing forever is zero. △ Less

Submitted 20 May, 2025; v1 submitted 12 April, 2025; originally announced April 2025.

Comments: accepted at LICS 2025

Bialgebraic Reasoning on Stateful Languages

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionality, guaranteeing that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilit… ▽ More Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionality, guaranteeing that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilitate compositionality proofs and avoid boilerplate work, one would hope to employ the abstract bialgebraic methods provided by Turi and Plotkin's powerful theory of mathematical operational semantics (a.k.a. abstract GSOS) or its recent extension by Goncharov et al. to higher-order languages. However, multiple attempts to apply abstract GSOS to stateful languages have thus failed. We propose a novel approach to the operational semantics of stateful languages based on the formal distinction between readers (terms that expect an initial input store before being executed), and writers (running terms that have already been provided with a store). In contrast to earlier work, this style of semantics is fully compatible with abstract GSOS, and we can thus leverage the existing theory to obtain coinductive reasoning techniques. We demonstrate that our approach generates non-trivial compositionality results for stateful languages with first-order and higher-order store and that it flexibly applies to program equivalences at different levels of granularity, such as trace, cost, and natural equivalence. △ Less

Submitted 13 March, 2025; originally announced March 2025.

Relators and Notions of Simulation Revisited

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: Simulations and bisimulations are ubiquitous in the study of concurrent systems and modal logics of various types. Besides classical relational transition systems, relevant system types include, for instance, probabilistic, weighted, neighbourhood-based, and game-based systems. Universal coalgebra abstracts system types in this sense as set functors. Notions of (bi)simulation then arise by extendi… ▽ More Simulations and bisimulations are ubiquitous in the study of concurrent systems and modal logics of various types. Besides classical relational transition systems, relevant system types include, for instance, probabilistic, weighted, neighbourhood-based, and game-based systems. Universal coalgebra abstracts system types in this sense as set functors. Notions of (bi)simulation then arise by extending the functor to act on relations in a suitable manner, turning it into what may be termed a relator. We contribute to the study of relators in the broadest possible sense, in particular in relation to their induced notions of (bi)similarity. Specifically, (i) we show that every functor that preserves a very restricted type of pullbacks (termed 1/4-iso pullbacks) admits a sound and complete notion of bisimulation induced by the coBarr relator; (ii) we establish equivalences between properties of relators and closure properties of the induced notion of (bi)simulation, showing in particular that the full set of expected closure properties requires the relator to be a lax extension, and that soundness of (bi)simulations requires preservation of diagonals; and (iii) we show that functors preserving inverse images admit a greatest lax extension. In a concluding case study, we apply (iii) to obtain a novel highly permissive notion of twisted bisimulation on labelled transition systems. △ Less

Submitted 21 May, 2025; v1 submitted 3 February, 2025; originally announced February 2025.

Abstract Operational Methods for Call-by-Push-Value

Authors: Sergey Goncharov, Stelios Tsampas, Henning Urbat

Abstract: Levy's call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes both call-by-value and call-by-name evaluation strategies. In the present work, we develop modular methods to reason about program equivalence in call-by-push-value, and in fine-grain call-by-value, which is a popular light… ▽ More Levy's call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes both call-by-value and call-by-name evaluation strategies. In the present work, we develop modular methods to reason about program equivalence in call-by-push-value, and in fine-grain call-by-value, which is a popular lightweight call-by-value sublanguage of the former. Our approach is based on the fundamental observation that presheaf categories of sorted sets are suitable universes to model call-by-(push)-value languages, and that natural, coalgebraic notions of program equivalence such as applicative similarity and logical relations can be developed within. Starting from this observation, we formalize fine-grain call-by-value and call-by-push-value in the higher-order abstract GSOS framework, reduce their key congruence properties to simple syntactic conditions by leveraging existing theory and argue that introducing changes to either language incurs minimal proof overhead. △ Less

Submitted 7 March, 2025; v1 submitted 22 October, 2024; originally announced October 2024.

Identity-Preserving Lax Extensions and Where to Find Them

Authors: Sergey Goncharov, Dirk Hofmaan, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fa… ▽ More Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems. △ Less

Submitted 11 January, 2025; v1 submitted 18 October, 2024; originally announced October 2024.

Comments: Full version of STACS 2025 paper

A Unifying Categorical View of Nondeterministic Iteration and Tests

Authors: Sergey Goncharov, Tarmo Uustalu

Abstract: We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of it came along afterwards to answer the demand for more refined flavors of semantics, such as stateful, concurrent, exceptional, hybrid, branching time, etc. We d… ▽ More We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of it came along afterwards to answer the demand for more refined flavors of semantics, such as stateful, concurrent, exceptional, hybrid, branching time, etc. We detach Kleene iteration from Kleene algebra and analyze it from the categorical perspective. The notion, we arrive at is that of Kleene-iteration category (with coproducts and tests), which we show to be general and robust in the sense of compatibility with programming language features, such as exceptions, store, concurrent behavior, etc. We attest the proposed notion w.r.t. various yardsticks, most importantly, by characterizing the free model as a certain category of (nondeterministic) rational trees. △ Less

Submitted 17 July, 2024; v1 submitted 11 July, 2024; originally announced July 2024.

Comments: Full version of the CONCUR 2024 paper

Higher-Order Bialgebraic Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory… ▽ More Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term \emph{(pointed) higher-order GSOS laws}. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of combinatory logics and the $λ$-calculus w.r.t.\ a strong variant of Abramsky's applicative bisimilarity are obtained as instances. △ Less

Submitted 26 March, 2025; v1 submitted 26 May, 2024; originally announced May 2024.

Comments: Submitted to J. Funct. Program. Extended and updated version of arXiv:2210.13387

Representing Guardedness in Call-by-Value and Guarded Parametrized Monads

Authors: Sergey Goncharov

Abstract: Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian… ▽ More Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representing guarded effectful function spaces calls for certain parametrized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate on a category. △ Less

Submitted 1 March, 2024; originally announced March 2024.

Comments: Extended version of https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.34

Bialgebraic Reasoning on Higher-Order Program Equivalence

Authors: Sergey Goncharov, Stefan Milius, Stelios Tsampas, Henning Urbat

Abstract: Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mat… ▽ More Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higher-order languages. Our main result asserts that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and $λ$-calculi with recursive types, and to different flavours of contextual equivalence. △ Less

Submitted 16 May, 2024; v1 submitted 1 February, 2024; originally announced February 2024.

Logical Predicates in Higher-Order Mathematical Operational Semantics

Authors: Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We first observe that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a… ▽ More We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We first observe that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a view to enabling inductive reasoning, and identify sufficient conditions on the overall setup in which locally maximal logical refinements canonically exist. Finally, we develop induction-up-to techniques that simplify inductive proofs via logical predicates on systems encoded as (certain classes of) higher-order GSOS laws by identifying and abstracting away from their boiler-plate part. △ Less

Submitted 12 January, 2024; v1 submitted 11 January, 2024; originally announced January 2024.

Comments: Extended version

Weak Similarity in Higher-Order Mathematical Operational Semantics

Authors: Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, Lutz Schröder

Abstract: Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak simil… ▽ More Higher-order abstract GSOS is a recent extension of Turi and Plotkin's framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky's applicative similarity for the lambda-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe's method. △ Less

Submitted 28 September, 2023; v1 submitted 16 February, 2023; originally announced February 2023.

Shades of Iteration: from Elgot to Kleene

Authors: Sergey Goncharov

Abstract: Notions of iteration range from the arguably most general Elgot iteration to a very specific Kleene iteration. The fundamental nature of Elgot iteration has been extensively explored by Bloom and Esik in the form of iteration theories, while Kleene iteration became extremely popular as an integral part of (untyped) formalisms, such as automata theory, regular expressions and Kleene algebra. Here,… ▽ More Notions of iteration range from the arguably most general Elgot iteration to a very specific Kleene iteration. The fundamental nature of Elgot iteration has been extensively explored by Bloom and Esik in the form of iteration theories, while Kleene iteration became extremely popular as an integral part of (untyped) formalisms, such as automata theory, regular expressions and Kleene algebra. Here, we establish a formal connection between Elgot iteration and Kleene iteration in the form of Elgot monads and Kleene monads, respectively. We also introduce a novel class of while-monads, which like Kleene monads admit a relatively simple description in algebraic terms. Like Elgot monads, while-monads cover a large variety of models that meaningfully support while-loops, but may fail the Kleene algebra laws, or even fail to support a Kleen iteration operator altogether. △ Less

Submitted 2 June, 2023; v1 submitted 15 January, 2023; originally announced January 2023.

Comments: Extended version of the accepted one for "Recent Trends in Algebraic Development Techniques - 26th IFIP WG 1.3 International Workshop, WADT 2022"

Towards a Higher-Order Mathematical Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the pr… ▽ More Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the $λ$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. △ Less

Submitted 26 October, 2022; v1 submitted 24 October, 2022; originally announced October 2022.

Quantitative Hennessy-Milner Theorems via Notions of Density

Authors: Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on… ▽ More The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on behavioural distance (e.g.~in weighted, metric, or probabilistic transition systems) are witnessed by quantitative modal formulas. Both the qualitative and the quantitative versions have been accommodated within the framework of coalgebraic logic, with distances taking values in quantales, subject to certain restrictions, such as being so-called value quantales. While previous quantitative coalgebraic Hennessy-Milner theorems apply only to liftings of set functors to (pseudo-)metric spaces, in the present work we provide a quantitative coalgebraic Hennessy-Milner theorem that applies more widely to functors native to metric spaces; notably, we thus cover, for the first time, the well-known Hennessy-Milner theorem for continuous probabilistic transition systems, where transitions are given by Borel measures on metric spaces, as an instance. In the process, we also relax the restrictions imposed on the quantale, and additionally parametrize the technical account over notions of closure and, hence, density, providing associated variants of the Stone-Weierstrass theorem; this allows us to cover, for instance, behavioural ultrametrics. △ Less

Submitted 30 August, 2022; v1 submitted 19 July, 2022; originally announced July 2022.

Stateful Structural Operational Semantics

Authors: Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

Abstract: Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We intr… ▽ More Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences. △ Less

Submitted 11 May, 2022; v1 submitted 22 February, 2022; originally announced February 2022.

Kantorovich Functors and Characteristic Logics for Behavioural Distances

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take… ▽ More Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take, thus covering, e.g., two-valued equivalences, (pseudo-)metrics, and probabilistic (pseudo-)metrics. Coalgebraic behavioural distances have been based either on liftings of SET-functors to categories of metric spaces, or on lax extensions of SET-functors to categories of quantitative relations. Every lax extension induces a functor lifting but not every lifting comes from a lax extension. It was shown recently that every lax extension is Kantorovich, i.e. induced by a suitable choice of monotone predicate liftings, implying via a quantitative coalgebraic Hennessy-Milner theorem that behavioural distances induced by lax extensions can be characterized by quantitative modal logics. Here, we essentially show the same in the more general setting of behavioural distances induced by functor liftings. In particular, we show that every functor lifting, and indeed every functor on (quantale-valued) metric spaces, that preserves isometries is Kantorovich, so that the induced behavioural distance (on systems of suitably restricted branching degree) can be characterized by a quantitative modal logic. △ Less

Submitted 2 May, 2023; v1 submitted 14 February, 2022; originally announced February 2022.

A Point-free Perspective on Lax extensions and Predicate liftings

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Abstract: Lax extensions of set functors play a key role in various areas including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundame… ▽ More Lax extensions of set functors play a key role in various areas including topology, concurrent systems, and modal logic, while predicate liftings provide a generic semantics of modal operators. We take a fresh look at the connection between lax extensions and predicate liftings from the point of view of quantale-enriched relations. Using this perspective, we show in particular that various fundamental concepts and results arise naturally and their proofs become very elementary. Ultimately, we prove that every lax extension is induced by a class of predicate liftings; we discuss several implications of this result. △ Less

Submitted 7 December, 2023; v1 submitted 23 December, 2021; originally announced December 2021.

Journal ref: Mathematical Structures in Computer Science. 2023:1-30

Uniform Elgot Iteration in Foundations

Authors: Sergey Goncharov

Abstract: Category theory is famous for its innovative way of thinking of concepts by their descriptions, in particular by establishing universal properties. Concepts that can be characterized in a universal way receive a certain quality seal, which makes them easily transferable across application domains. The notion of partiality is however notoriously difficult to characterize in this way, although the i… ▽ More Category theory is famous for its innovative way of thinking of concepts by their descriptions, in particular by establishing universal properties. Concepts that can be characterized in a universal way receive a certain quality seal, which makes them easily transferable across application domains. The notion of partiality is however notoriously difficult to characterize in this way, although the importance of it is certain, especially for computer science where entire research areas, such as synthetic and axiomatic domain theory revolve around notions of partiality. More recently, this issue resurfaced in the context of (constructive) intensional type theory. Here, we provide a generic categorical iteration-based notion of partiality, which is arguably the most basic one. We show that the emerging free structures, which we dub uniform-iteration algebras enjoy various desirable properties, in particular, yield an equational lifting monad. We then study the impact of classicality assumptions and choice principles on this monad, in particular, we establish a suitable categorial formulation of the axiom of countable choice entailing that the monad is an Elgot monad. △ Less

Submitted 3 July, 2021; v1 submitted 23 February, 2021; originally announced February 2021.

Comments: Full version of ICALP 2021 accepted paper

Implementing Hybrid Semantics: From Functional to Imperative

Authors: Sergey Goncharov, Renato Neves, José Proença

Abstract: Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combi… ▽ More Hybrid programs combine digital control with differential equations, and naturally appear in a wide range of application domains, from biology and control theory to real-time software engineering. The entanglement of discrete and continuous behaviour inherent to such programs goes beyond the established computer science foundations, producing challenges related to e.g. infinite iteration and combination of hybrid behaviour with other effects. A systematic treatment of hybridness as a dedicated computational effect has emerged recently. In particular, a generic idealized functional language HybCore with a sound and adequate operational semantics has been proposed. The latter semantics however did not provide hints to implementing HybCore as a runnable language, suitable for hybrid system simulation (e.g. the semantics features rules with uncountably many premises). We introduce an imperative counterpart of HybCore, whose semantics is simpler and runnable, and yet intimately related with the semantics of HybCore at the level of hybrid monads. We then establish a corresponding soundness and adequacy theorem. To attest that the resulting semantics can serve as a firm basis for the implementation of typical tools of programming oriented to the hybrid domain, we present a web-based prototype implementation to evaluate and inspect hybrid programs, in the spirit of GHCi for Haskell and UTop for OCaml. The major asset of our implementation is that it formally follows the operational semantic rules. △ Less

Submitted 29 September, 2020; originally announced September 2020.

Comments: This is an extended version of a paper accepted in ICTAC'20

MSC Class: 03B70

Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store

Authors: Miriam Polzer, Sergey Goncharov

Abstract: Modelling and reasoning about dynamic memory allocation is one of the well-established strands of theoretical computer science, which is particularly well-known as a source of notorious challenges in semantics, reasoning, and proof theory. We capitalize on recent progress on categorical semantics of full ground store, in terms of a full ground store monad, to build a corresponding semantics of a h… ▽ More Modelling and reasoning about dynamic memory allocation is one of the well-established strands of theoretical computer science, which is particularly well-known as a source of notorious challenges in semantics, reasoning, and proof theory. We capitalize on recent progress on categorical semantics of full ground store, in terms of a full ground store monad, to build a corresponding semantics of a higher order logic over the corresponding programs. Our main result is a construction of an (intuitionistic) BI-hyperdoctrine, which is arguably the semantic core of higher order logic over local store. Although we have made an extensive use of the existing generic tools, certain principled changes had to be made to enable the desired construction: while the original monad works over total heaps (to disable dangling pointers), our version involves partial heaps (heaplets) to enable compositional reasoning using separating conjunction. Another remarkable feature of our construction is that, in contrast to the existing generic approaches, our BI-algebra does not directly stem from an internal categorical partial commutative monoid. △ Less

Submitted 11 March, 2020; originally announced March 2020.

Comments: version with appendix

The Expressiveness of Looping Terms in the Semantic Programming

Authors: Sergey Goncharov, Sergey Ospichev, Denis Ponomaryov, Dmitri Sviridenko

Abstract: We consider the language of $Δ_0$-formulas with list terms interpreted over hereditarily finite list superstructures. We study the complexity of reasoning in extensions of the language of $Δ_0$-formulas with non-standard list terms, which represent bounded list search, bounded iteration, and bounded recursion. We prove a number of results on the complexity of model checking and satisfiability for… ▽ More We consider the language of $Δ_0$-formulas with list terms interpreted over hereditarily finite list superstructures. We study the complexity of reasoning in extensions of the language of $Δ_0$-formulas with non-standard list terms, which represent bounded list search, bounded iteration, and bounded recursion. We prove a number of results on the complexity of model checking and satisfiability for these formulas. In particular, we show that the set of $Δ_0$-formulas with bounded recursive terms true in a given list superstructure $HW(\mathcal{M})$ is non-elementary (it contains the class kEXPTIME, for all $k\geqslant 1$). For $Δ_0$-formulas with restrictions on the usage of iterative and recursive terms, we show lower complexity. △ Less

Submitted 24 January, 2020; v1 submitted 5 December, 2019; originally announced December 2019.

An Adequate While-Language for Hybrid Computation

Authors: Sergey Goncharov, Renato Neves

Abstract: Hybrid computation combines discrete and continuous dynamics in the form of an entangled mixture inherently present both in various natural phenomena, and in applications ranging from control theory to microbiology. The emergent behaviours bear signs of both computational and physical processes, and thus present difficulties not only for analysis, but also for describing them adequately in a struc… ▽ More Hybrid computation combines discrete and continuous dynamics in the form of an entangled mixture inherently present both in various natural phenomena, and in applications ranging from control theory to microbiology. The emergent behaviours bear signs of both computational and physical processes, and thus present difficulties not only for analysis, but also for describing them adequately in a structural, well-founded way. Here, we introduce a language for hybrid computation, inspired by the fine-grain call-by-value paradigm, and equip it with a denotational and computationally adequate denotational semantics. Our denotational semantics crucially relies on a hybrid monad supporting an (Elgot) iteration operator, we developed elsewhere. As an intermediate step we introduce a more lightweight duration semantics furnished with analogous results and drawing on a new duration monad that we introduce as a lightweight counterpart to the hybrid monad. △ Less

Submitted 17 July, 2019; v1 submitted 20 February, 2019; originally announced February 2019.

Comments: Accepted at PPDP'19

Using fuzzy bits and neural networks to partially invert few rounds of some cryptographic hash functions

Authors: Sergij V. Goncharov

Abstract: We consider fuzzy, or continuous, bits, which take values in [0;1] and (-1;1] instead of {0;1}, and operations on them (NOT, XOR etc.) and on their sequences (ADD), to obtain the generalization of cryptographic hash functions, CHFs, for the messages consisting of fuzzy bits, so that CHFs become smooth and non-constant functions of each bit of the message. We then train the neural networks to predi… ▽ More We consider fuzzy, or continuous, bits, which take values in [0;1] and (-1;1] instead of {0;1}, and operations on them (NOT, XOR etc.) and on their sequences (ADD), to obtain the generalization of cryptographic hash functions, CHFs, for the messages consisting of fuzzy bits, so that CHFs become smooth and non-constant functions of each bit of the message. We then train the neural networks to predict the message that has a given hash, where the loss function for the hash of predicted message and given true hash is backpropagatable. The results of the trainings for the standard CHFs - MD5, SHA1, SHA2-256, and SHA3/Keccak - with small number of (optionally weakened) rounds are presented and compared. △ Less

Submitted 8 January, 2019; originally announced January 2019.

Comments: 26 pages, 31 figures, 48 refs

ACM Class: D.4.6; I.2.6

A Metalanguage for Guarded Iteration

Authors: Sergey Goncharov, Christoph Rauch, Lutz Schröder

Abstract: 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 gua… ▽ More 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. △ Less

Submitted 24 May, 2021; v1 submitted 30 July, 2018; originally announced July 2018.

Comments: extended version for the special issue

A Semantics for Hybrid Iteration

Authors: Sergey Goncharov, Julian Jakob, Renato Neves

Abstract: The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and preserving its merits. In this paper we use these notions and the corresponding stock of results to examine different types of iteration for hybrid computations. As… ▽ More The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and preserving its merits. In this paper we use these notions and the corresponding stock of results to examine different types of iteration for hybrid computations. As a starting point we use an available notion of hybrid monad restricted to the category of sets, and modify it in order to obtain a suitable notion of guarded iteration with guardedness interpreted as progressiveness in time - we motivate this modification by our intention to capture Zeno behaviour in an arguably general and feasible way. We illustrate our results with a simple programming language for hybrid computations and interpret it over the developed semantic foundations. △ Less

Submitted 5 February, 2019; v1 submitted 3 July, 2018; originally announced July 2018.

Comments: Corrected version of a CONCUR'18 paper; more proof details

Guarded Traced Categories

Authors: Sergey Goncharov, Lutz Schröder

Abstract: Notions of guardedness serve to delineate the admissibility of cycles, e.g. in recursion, corecursion, iteration, or tracing. We introduce an abstract notion of guardedness structure on a symmetric monoidal category, along with a corresponding notion of guarded traces, which are defined only if the cycles they induce are guarded. We relate structural guardedness, determined by propagating guardedn… ▽ More Notions of guardedness serve to delineate the admissibility of cycles, e.g. in recursion, corecursion, iteration, or tracing. We introduce an abstract notion of guardedness structure on a symmetric monoidal category, along with a corresponding notion of guarded traces, which are defined only if the cycles they induce are guarded. We relate structural guardedness, determined by propagating guardedness along the operations of the category, to geometric guardedness phrased in terms of a diagrammatic language. In our setup, the Cartesian case (recursion) and the co-Cartesian case (iteration) become completely dual, and we show that in these cases, guarded tracedness is equivalent to presence of a guarded Conway operator, in analogy to an observation on total traces by Hasegawa and Hyland. Moreover, we relate guarded traces to unguarded categorical uniform fixpoint operators in the style of Simpson and Plotkin. Finally, we show that partial traces based on Hilbert-Schmidt operators in the category of Hilbert spaces are an instance of guarded traces. △ Less

Submitted 23 February, 2018; originally announced February 2018.

Comments: full version with appendix

Guarded and Unguarded Iteration for Generalized Processes

Authors: Sergey Goncharov, Lutz Schröder, Christoph Rauch, Maciej Piróg

Abstract: 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 deter… ▽ More 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. △ Less

Submitted 3 July, 2019; v1 submitted 27 December, 2017; originally announced December 2017.

MSC Class: 03D75; 68Q55 ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 3 (July 4, 2019) lmcs:4170

Complete Elgot Monads and Coalgebraic Resumptions

Authors: Sergey Goncharov, Stefan Milius, Christoph Rauch

Abstract: 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… ▽ More 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. △ Less

Submitted 7 March, 2016; originally announced March 2016.

Comments: full version, 39 p

Some Remarks on Conway and Iteration Theories

Authors: Zoltan Esik, Sergey Goncharov

Abstract: We present an axiomatization of Conway theories which yields,as a corollary, a very concise axiomatization of iteration theories satisfying the functorial implication for base morphisms. We present an axiomatization of Conway theories which yields,as a corollary, a very concise axiomatization of iteration theories satisfying the functorial implication for base morphisms. △ Less

Submitted 2 March, 2016; originally announced March 2016.

MSC Class: 68Q55; 18C10 ACM Class: F.3.2; F.3.3

Unguarded Recursion on Coinductive Resumptions

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

Abstract: 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 re… ▽ More 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. △ Less

Submitted 24 August, 2018; v1 submitted 5 May, 2014; originally announced May 2014.

Comments: 47 pages, extended version of http://www.sciencedirect.com/science/article/pii/S1571066115000791

ACM Class: F.3.2; F.3.3; D.3.3

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 3 (August 27, 2018) lmcs:4773

Coalgebraic Weak Bisimulation from Recursive Equations over Monads

Authors: Sergey Goncharov, Dirk Pattinson

Abstract: Strong bisimulation for labelled transition systems is one of the most fundamental equivalences in process algebra, and has been generalised to numerous classes of systems that exhibit richer transition behaviour. Nearly all of the ensuing notions are instances of the more general notion of coalgebraic bisimulation. Weak bisimulation, however, has so far been much less amenable to a coalgebraic tr… ▽ More Strong bisimulation for labelled transition systems is one of the most fundamental equivalences in process algebra, and has been generalised to numerous classes of systems that exhibit richer transition behaviour. Nearly all of the ensuing notions are instances of the more general notion of coalgebraic bisimulation. Weak bisimulation, however, has so far been much less amenable to a coalgebraic treatment. Here we attempt to close this gap by giving a coalgebraic treatment of (parametrized) weak equivalences, including weak bisimulation. Our analysis requires that the functor defining the transition type of the system is based on a suitable order-enriched monad, which allows us to capture weak equivalences by least fixpoints of recursive equations. Our notion is in agreement with existing notions of weak bisimulations for labelled transition systems, probabilistic and weighted systems, and simple Segala systems. △ Less

Submitted 2 May, 2014; v1 submitted 4 April, 2014; originally announced April 2014.

Comments: final version

Towards a Uniform Theory of Effectful State Machines

Authors: Sergey Goncharov, Stefan Milius, Alexandra Silva

Abstract: Using recent developments in coalgebraic and monad-based semantics, we present a uniform study of various notions of machines, e.g. finite state machines, multi-stack machines, Turing machines, valence automata, and weighted automata. They are instances of Jacobs' notion of a T-automaton, where T is a monad. We show that the generic language semantics for T-automata correctly instantiates the usua… ▽ More Using recent developments in coalgebraic and monad-based semantics, we present a uniform study of various notions of machines, e.g. finite state machines, multi-stack machines, Turing machines, valence automata, and weighted automata. They are instances of Jacobs' notion of a T-automaton, where T is a monad. We show that the generic language semantics for T-automata correctly instantiates the usual language semantics for a number of known classes of machines/languages, including regular, context-free, recursively-enumerable and various subclasses of context free languages (e.g. deterministic and real-time ones). Moreover, our approach provides new generic techniques for studying the expressivity power of various machine-based models. △ Less

Submitted 17 March, 2020; v1 submitted 21 January, 2014; originally announced January 2014.

Comments: final version accepted by TOCL

Journal ref: ACM Transactions on Computational Logic, March 2020, Article No.: 23, Volume 21, Issue 3

Exploring the Boundaries of Monad Tensorability on Set

Authors: Nathan Bowler, Sergey Goncharov, Paul Blain Levy, Lutz Schröder

Abstract: We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts;… ▽ More We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We present two main results: we show that the tensor of two monads need not in general exist by presenting two counterexamples, one of them involving finite powerset (i.e. the theory of join semilattices); this solves a somewhat long-standing open problem, and contrasts with recent results that had ruled out previously expected counterexamples. On the other hand, we show that tensors with bounded powerset monads do exist from countable powerset upwards. △ Less

Submitted 17 September, 2013; v1 submitted 9 September, 2013; originally announced September 2013.

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 3 (September 18, 2013) lmcs:740

A Coinductive Calculus for Asynchronous Side-effecting Processes

Authors: Sergey Goncharov, Lutz Schröder

Abstract: We present an abstract framework for concurrent processes in which atomic steps have generic side effects, handled according to the principle of monadic encapsulation of effects. Processes in this framework are potentially infinite resumptions, modelled using final coalgebras over the monadic base. As a calculus for such processes, we introduce a concurrent extension of Moggi's monadic metalanguag… ▽ More We present an abstract framework for concurrent processes in which atomic steps have generic side effects, handled according to the principle of monadic encapsulation of effects. Processes in this framework are potentially infinite resumptions, modelled using final coalgebras over the monadic base. As a calculus for such processes, we introduce a concurrent extension of Moggi's monadic metalanguage of effects. We establish soundness and completeness of a natural equational axiomatisation of this calculus. Moreover, we identify a corecursion scheme that is explicitly definable over the base language and provides flexible expressive means for the definition of new operators on processes, such as parallel composition. As a worked example, we prove the safety of a generic mutual exclusion scheme using a verification logic built on top of the equational calculus. △ Less

Submitted 14 April, 2011; originally announced April 2011.

Powermonads and Tensors of Unranked Effects

Authors: Sergey Goncharov, Lutz Schröder

Abstract: In semantics and in programming practice, algebraic concepts such as monads or, essentially equivalently, (large) Lawvere theories are a well-established tool for modelling generic side-effects. An important issue in this context are combination mechanisms for such algebraic effects, which allow for the modular design of programming languages and verification logics. The most basic combination ope… ▽ More In semantics and in programming practice, algebraic concepts such as monads or, essentially equivalently, (large) Lawvere theories are a well-established tool for modelling generic side-effects. An important issue in this context are combination mechanisms for such algebraic effects, which allow for the modular design of programming languages and verification logics. The most basic combination operators are sum and tensor: while the sum of effects is just their non-interacting union, the tensor imposes commutation of effects. However, for effects with unbounded arity, such as continuations or unbounded nondeterminism, it is not a priori clear whether these combinations actually exist in all cases. Here, we introduce the class of uniform effects, which includes unbounded nondeterminism and continuations, and prove that the tensor does always exist if one of the component effects is uniform, thus in particular improving on previous results on tensoring with continuations. We then treat the case of nondeterminism in more detail, and give an order-theoretic characterization of effects for which tensoring with nondeterminism is conservative, thus enabling nondeterministic arguments such as a generic version of the Fischer-Ladner encoding of control operators. △ Less

Submitted 11 April, 2011; v1 submitted 14 January, 2011; originally announced January 2011.

Comments: extended version; first 10 pages are to appear on LICS'11