-
Protocol Choice and Iteration for the Free Cornering
Authors:
Chad Nester,
Niels Voorneveld
Abstract:
We extend the free cornering of a symmetric monoidal category, a double categorical model of concurrent interaction, to support branching communication protocols and iterated communication protocols. We validate our constructions by showing that they inherit significant categorical structure from the free cornering, including that they form monoidal double categories. We also establish some elemen…
▽ More
We extend the free cornering of a symmetric monoidal category, a double categorical model of concurrent interaction, to support branching communication protocols and iterated communication protocols. We validate our constructions by showing that they inherit significant categorical structure from the free cornering, including that they form monoidal double categories. We also establish some elementary properties of the novel structure they contain. Further, we give a model of the free cornering in terms of strong functors and strong natural transformations, inspired by the literature on computational effects.
△ Less
Submitted 5 January, 2024; v1 submitted 26 May, 2023;
originally announced May 2023.
-
Inductive and Coinductive Predicate Liftings for Effectful Programs
Authors:
Niccolò Veltri,
Niels F. W. Voorneveld
Abstract:
We formulate a framework for describing behaviour of effectful higher-order recursive programs. Examples of effects are implemented using effect operations, and include: execution cost, nondeterminism, global store and interaction with a user. The denotational semantics of a program is given by a coinductive tree in a monad, which combines potential return values of the program in terms of effect…
▽ More
We formulate a framework for describing behaviour of effectful higher-order recursive programs. Examples of effects are implemented using effect operations, and include: execution cost, nondeterminism, global store and interaction with a user. The denotational semantics of a program is given by a coinductive tree in a monad, which combines potential return values of the program in terms of effect operations.
Using a simple test logic, we construct two sorts of predicate liftings, which lift predicates on a result type to predicates on computations that produce results of that type, each capturing a facet of program behaviour. Firstly, we study inductive predicate liftings which can be used to describe effectful notions of total correctness. Secondly, we study coinductive predicate liftings, which describe effectful notions of partial correctness. The two constructions are dual in the sense that one can be used to disprove the other.
The predicate liftings are used as a basis for an endogenous logic of behavioural properties for higher-order programs. The program logic has a derivable notion of negation, arising from the duality of the two sorts of predicate liftings, and it generates a program equivalence which subsumes a notion of bisimilarity. Appropriate definitions of inductive and coinductive predicate liftings are given for a multitude of effect examples.
The whole development has been fully formalized in the Agda proof assistant.
△ Less
Submitted 28 December, 2021;
originally announced December 2021.
-
From Equations to Distinctions: Two Interpretations of Effectful Computations
Authors:
Niels Voorneveld
Abstract:
There are several ways to define program equivalence for functional programs with algebraic effects. We consider two complementing ways to specify behavioural equivalence. One way is to specify a set of axiomatic equations, and allow proof methods to show that two programs are equivalent. Another way is to specify an Eilenberg-Moore algebra, which generate tests that could distinguish programs. Th…
▽ More
There are several ways to define program equivalence for functional programs with algebraic effects. We consider two complementing ways to specify behavioural equivalence. One way is to specify a set of axiomatic equations, and allow proof methods to show that two programs are equivalent. Another way is to specify an Eilenberg-Moore algebra, which generate tests that could distinguish programs. These two methods are said to complement each other if any two programs can be shown to be equivalent if and only if there is no test to distinguish them.
In this paper, we study a generic method to formulate from a set of axiomatic equations an Eilenberg-Moore algebra which complements it. We will look at an additional condition which must be satisfied for this to work. We then apply this method to a handful of examples of effects, including probability and global store, and show they coincide with the usual algebras from the literature. We will moreover study whether or not it is possible to specify a set of unary Boolean modalities which could function as distinction-tests complementing the equational theory.
△ Less
Submitted 30 April, 2020;
originally announced May 2020.
-
Quantitative Logics for Equivalence of Effectful Programs
Authors:
Niels Voorneveld
Abstract:
In order to reason about effects, we can define quantitative formulas to describe behavioural aspects of effectful programs. These formulas can for example express probabilities that (or sets of correct starting states for which) a program satisfies a property. Fundamental to this approach is the notion of quantitative modality, which is used to lift a property on values to a property on computati…
▽ More
In order to reason about effects, we can define quantitative formulas to describe behavioural aspects of effectful programs. These formulas can for example express probabilities that (or sets of correct starting states for which) a program satisfies a property. Fundamental to this approach is the notion of quantitative modality, which is used to lift a property on values to a property on computations. Taking all formulas together, we say that two terms are equivalent if they satisfy all formulas to the same quantitative degree. Under sufficient conditions on the quantitative modalities, this equivalence is equal to a notion of Abramsky's applicative bisimilarity, and is moreover a congruence. We investigate these results in the context of Levy's call-by-push-value with general recursion and algebraic effects. In particular, the results apply to (combinations of) nondeterministic choice, probabilistic choice, and global store.
△ Less
Submitted 26 April, 2019;
originally announced April 2019.
-
Behavioural Equivalence via Modalities for Algebraic Effects
Authors:
Alex Simpson,
Niels Voorneveld
Abstract:
The paper investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collect…
▽ More
The paper investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability, are satisfied by the modalities then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe's method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store and input/output.
△ Less
Submitted 25 October, 2019; v1 submitted 18 April, 2019;
originally announced April 2019.
