Behavioural Equivalence via Modalities for Algebraic Effects

The notion of behavioural equivalence between programs is a fundamental concept in the theory of programming languages. A conceptually natural approach to defining behavioural equivalence is to consider two programs as being equivalent if they enjoy the same ‘behavioural properties’. This can be made precise by specifying a behavioural logic whose formulas express behavioural properties. Two programs M, N are then defined to be equivalent if, for all formulas \(\varPhi \), it holds that \(M~\models ~ \varPhi \) iff \(N~\models ~\varPhi \) (where \(M \, \models \, \varPhi \) expresses the satisfaction relation: program M enjoys property \(\varPhi \)).

This logical approach to defining behavioural equivalence has been particularly prominent in concurrency theory, where the classic result is that the equivalence defined by Hennessy-Milner logic [4] coincides with bisimilarity [14, 17]. The aim of the present paper is to adapt the logical approach to the very different computational paradigm of applicative programming with effects.

More precisely, we consider a call-by-value functional programming language with algebraic effects in the sense of Plotkin and Power [21]. Broadly speaking, effects are those aspects of computation that involve a program interacting with its ‘environment’; for example: nondeterminism, probabilistic choice (in both cases, the choice is deferred to the environment); input/output; mutable store (the machine state is modified); control operations such as exceptions, jumps and handlers (which interact with the continuation in the evaluation process); etc. Such general effects collectively enjoy common properties identified in the work of Moggi on monads [15]. Among them, algebraic effects play a special role. They can be included in a programming language by adding effect-triggering operations, whose ‘algebraic’ nature means that effects act independently of the continuation. From the aforementioned examples of effects, only jumps and handlers are non-algebraic. Thus the notion of algebraic effect covers a broad range of effectful computational behaviour. Call-by-value functional languages provide a natural context for exploring effectful programming. From a theoretical viewpoint, other programming paradigms are subsumed; for example, imperative programs can be recast as effectful functional ones. From a practical viewpoint, the combination of effects with call-by-value leads to the natural programming style supported by impure functional languages such as OCaml.

In order to focus on the main contributions of the paper (the behavioural logic and its induced behavioural equivalence), we instantiate “call-by-value functional language with algebraic effects” using a very simple language. Our language is a simply-typed \(\lambda \)-calculus with a base type of natural numbers, general recursion, call-by-value function evaluation, and algebraic effects, similar to [21]; although, for technical convenience, we adopt the (equivalent) formulation of fine-grained call-by-value [13]. The language is defined precisely in Sect. 2. Following [8, 21], an operational semantics is given that evaluates programs to effect trees.

Section 3 introduces the behavioural logic. In our impure functional setting, the evaluation of a program of type \(\tau \) results in a computational process that may or may not invoke effects, and which may or may not terminate with a return value of type \(\tau \). The key ingredient in our logic is an effect-specific family \(\mathcal {O}\) of modalities, where each modality \(o \in \mathcal {O}\) converts a property \(\phi \) of values of type \(\tau \) to a property \(o\,\phi \) of general programs (called computations) of type \(\tau \). The idea is that such modalities capture all relevant effect-specific behavioural properties of the effects under consideration.

A main contribution of the paper is to give a general framework for defining such effect modalities, applicable across a wide range of algebraic effects. The general setting is that we have a signature \(\varSigma \) of effect operations, which determines the programming language, and a collection \(\mathcal {O}\) of modalities, which determines the behavioural logic. In order to specify the semantics of the logic, we require each modality to be assigned a set of unit-type effect trees, which determines the meaning of the modality. Several concrete examples and a detailed general explanation are given in Sect. 3.

In Sect. 4, we consider the relation of behavioural equivalence between programs determined by the logic. A fundamental well-behavedness property is that any reasonable program equivalence should be a congruence with respect to the syntactic constructs of the programming language. Our main theorem (Theorem 1) is that, under two conditions on the collection \(\mathcal {O}\) of modalities, which hold for all the examples of effects we consider, the logically induced behavioural equivalence is indeed a congruence.

In order to prove Theorem 1, we develop an alternative perspective on behavioural equivalence, which is of interest in its own right. In Sect. 5 we show how the modalities \(\mathcal {O}\) determine a relation of applicative \(\mathcal {O}\)-bisimilarity, which is an effect-sensitive version of Abramsky’s notion of applicative bisimilarity [1]. Theorem 2 shows that applicative \(\mathcal {O}\)-bisimilarity coincides with the logically defined relation of behavioural equivalence.

The proof of Theorem 1 is then concluded in Sect. 6, where we use Howe’s method [5, 6] to show that applicative \(\mathcal {O}\)-bisimilarity is a congruence. Although the proof is technically involved, we give only a brief outline, as the details closely follow the recent paper [9], in which Howe’s method is applied to an untyped language with general algebraic effects.

In Sect. 7, we present a variation on our behavioural logic, in which we make the syntax of logical formulas independent of the syntax of the programming language.

Finally, in Sect. 8 we discuss related and further work.

As motivated in the introduction, our chosen base language is a simply-typed call-by-value functional language with general recursion and a ground type of natural numbers, to which we add (algebraic) effect-triggering operations. This means that our language is a call-by-value variant of PCF [20], extended with algebraic effects, resulting in a language similar to the one considered in [21]. In order to simplify the technical treatment of the language, we present it in the style of fine-grained call-by-value [13]. This means that we make a syntactic distinction between values and computations, representing the static and dynamic aspects of the language respectively. Furthermore, all sequencing of computations is performed using a single language construct, the \(~\mathbf{let }~\) construct. The resulting language is straightforwardly intertranslatable with the more traditional call-by-value formulation. But the encapsulation of all sequencing within a single construct has the benefit of avoiding redundancy in proofs.

Our types are just the simple types obtained by iterating the function type construction over two base types: \(\mathbf N \) of natural numbers, and also a unit type \(\mathbf {1}\).

Types: \(\tau ,\rho :\,\!:= ~ \mathbf {1}\) | \(\mathbf N \) | \(\rho \rightarrow \tau \)

Contexts: \(\varGamma :\,\!:= ~ \emptyset \) | \(\varGamma , \,x : \tau \)

As usual, term variables x are taken from a countably-infinite stock of such variables, and the context \(\varGamma , \, x : \tau \) can only be formed if the variable x does not already appear in \(\varGamma \).

As discussed above, program terms are separated into two mutually defined but disjoint categories: values and computations.

Values: \(V,W :\,\!:= ~ *\) | Z | S(V) | \(\lambda x.M\) | x

Computations: \(M,N :\,\!:= ~VW\) | return V | let  \(M \Rightarrow x\) in  N | fix (V) |

      case V  in  \(\{Z \Rightarrow M, S(x) \Rightarrow N\}\)

Here, \(*\) is the unique value of the unit type. The values of the type of natural numbers are the numerals represented using zero Z and successor S. The values of function type are the \(\lambda \)-abstractions. And a variable x can be considered a value, because, under the call-by-value evaluation strategy of the language, it can only be instantiated with a value.

The computations are: function application VW; the computation that does nothing but return a value V; a \({~\mathbf{let }~}\) construct for sequencing; a \(\mathbf{fix }\) construct for recursive definition; and a \(\mathbf{case }\) construct that branches according to whether its natural-number argument is zero or positive. The computation \(~\mathbf{let }~M~\Rightarrow ~x~\mathbf{in }~N\) implements sequencing in the following sense. First the computation M is evaluated. Only in the case that the evaluation of M terminates, with return value V, does the thread of execution continue to N. In this case, the computation N[V/x] is evaluated, and its return value (if any) is the one returned by the \(~\mathbf{let }~\) construct.

To the pure functional language described above, we add effect operations. The collection of effect operations is specified by a set \(\varSigma \) (the signature) of such operations, together with, for each \(\sigma \in \varSigma \) an associated arity which takes one of the four forms belowThe notation here is chosen to be suggestive of the way in which such arities are used in the typing rules below, viewing \(\alpha \) as a type variable. Each of the forms of arity has an associated term constructor, for building additional computation terms, with which we extend the above grammar for computation terms.

Effects:  \(\sigma (M_0,M_1,\dots ,M_{n-1})\) | \(\sigma (V;M_0,M_1,\dots ,M_{n-1})\) | \(\sigma (V)\) | \(\sigma (W;V)\)

Motivating examples of effect operations and their computation terms can be found in Examples 0–5 below.

The typing rules for the language are given in Fig. 1 below. Note that the choice of typing rule for an effect operation \(\sigma \in \varSigma \) depends on its declared arity.

The terms of type \(\tau \) are the values and computations generated by the constructors above. Every term has a unique aspect as either a value or computation. We write \(\textit{Val}(\tau )\) and \(\textit{Com}(\tau )\) respectively for closed values and computations. So the closed terms of \(\tau \) are \(\textit{Term}(\tau ) = \textit{Val}(\tau ) \cup \textit{Com}(\tau )\). For \(n \in \mathbb {N}\) a natural number, we write \(\overline{n}\) for the numeral \(S^n(Z)\), hence \(Val(\mathbf N ) := \{\overline{n} \,|\, n \in \mathbb {N}\}\).

We now consider some standard signatures of computationally interesting effect operations, which will be used as running examples throughout the paper. (We use the same examples as in [8].)

We next present an operational semantics for our language, under which a computation term evaluates to an effect tree: essentially, a coinductively generated term using operations from \(\varSigma \), and with values and \(\bot \) (nontermination) as the generators. This idea appears in [8, 21], and our technical treatment follows approach of the latter, adapted to call-by-value.

We define a single-step reduction relation \(\rightarrowtail \) between configurations (S, M) consisting of a stack S and a computation M. The computation M is the term under current evaluation. The stack S represents a continuation computation awaiting the termination of M. First, we define a stack-independent reduction relation on computation terms that do not involve \(~\mathbf{let }~\) at the top level.The behaviour of \( ~\mathbf{let }~\) is implemented using a system of stacks where:

Stacks \(S :\,\!:= ~ \textit{id} \;\; | \;\; S \circ ({~\mathbf{let }~}~(-) \Rightarrow x~\mathbf{ in }~M)\)

We write \(S\{N\}\) for the computation term obtained by ‘applying’ the stack S to N, defined by:We write \(\textit{Stack}(\tau ,\rho )\) for the set of stacks S such that for any \(N \in \textit{Com}(\tau )\), it holds that \(S\{N\}\) is a well-typed expression of type \(\rho \). We define a reduction relation on pairs \(\textit{Stack}(\tau ,\rho ) \times \textit{Com}(\tau )\) (denoted \((S_1,M_1) \rightarrowtail (S_2,M_2)\)) by:We define the notion of effect tree for an arbitrary set X, where X is thought of as a set of abstract ‘values’.

We write TX for the set of trees over X. We define a partial ordering on TX where \(t_1 \le t_2\), if \(t_1\) can be obtained by replacing subtrees of \(t_2\) by \(\bot \). This forms an \(\omega \)-complete partial order, meaning that every ascending sequence \(t_1 \le t_2 \le \dots \) has a least upper bound \(\bigsqcup _n t_n\). Let \(\textit{Tree}(\tau ) := T\textit{Val}(\tau )\), we will define a reduction relation from computations to trees of values.

Given \(f: X \rightarrow Y\) and a tree \(t \in TX\), we write \(t[x \mapsto f(x)] \in TY\) for the tree whose leaves \(x \in X\) are renamed to f(x). We have a function \(\mu : TTX \rightarrow TX\), which takes a tree r of trees and flattens it to a tree \(\mu r \in TX\), by taking the labelling tree at each non-\(\bot \) leaf of r as the subtree at the corresponding node in \(\mu r\). The function \(\mu \) is the multiplication associated with the monad structure of the T operation. The unit of the monad is the map \(\eta : X \rightarrow TX\) which takes an element \(x \in X\) and returns a leaf labelled x.

The operational mapping from a computation \(M \in \textit{Com}(\tau )\) to an effect tree is defined intuitively as follows. Start evaluating the M in the empty stack \(\textit{id}\), until the evaluation process (which is deterministic) terminates (if this never happens the tree is \(\bot \)). If the evaluation process terminates at a configuration of the form \((\textit{id}, \mathbf{return }\ V)\) then the tree is the leaf V. Otherwise the evaluation process can only terminate at a configuration of the form \((S, \sigma (\dots ))\) for some effect operation \(\sigma \in \varSigma \). In this case, create an internal node in the tree of the appropriate kind (depending on \(\sigma \)) and continue generating each child tree of this node by repeating the above process by evaluating an appropriate continuation computation, starting from a configuration with the current stack S.

The following (somewhat technical) definition formalises the idea outlined above in a mathematically concise way. We define a family of maps \(|-,-|_{(-)} : \textit{Stack}(\tau ,\rho ) \times \textit{Com}(\tau ) \times \mathbb {N}\rightarrow \textit{Tree}(\rho )\) indexed over \(\tau ,\) and \(\rho \) by:It follows that \(|S,M|_n \le |S,M|_{n+1}\) in the given ordering on trees. We write \(|-|_{(-)}: \textit{Com}(\tau ) \times \mathbb {N}\rightarrow \textit{Tree}(\tau )\) for the function defined by \(|M|_n = |\textit{id},M|_n\). Using this we can give the operational interpretation of computation terms as effect trees by defining \(|-|: \textit{Com}(\tau ) \rightarrow \textit{Tree}(\tau )\) by \(|M| := \bigsqcup _n |M|_n\).

The goal of this section is to motivate and formulate a logic for expressing behavioural properties of programs. In our language, program means (well-typed) term, and we shall be interested both in properties of computations and in properties of values. Accordingly, we define a logic that contains both value formulas and computation formulas. We shall use lower case Greek letters \(\phi ,\psi ,\dots \) for the former, and upper case Greek letters \(\varPhi ,\varPsi ,\dots \) for the latter. Our logic will thus have two satisfaction relationswhich respectively assert that “value V enjoys the value property expressed by \(\phi \)” and “computation M enjoys the computation property expressed by \(\varPhi \)”.

In order to motivate the detailed formulation of the logic, it is useful to identify criteria that will guide the design.    

For every type \(\tau \), we define a collection \(\textit{VF}(\tau )\) of value formulas, and a collection \(\textit{CF}(\tau )\) of computation formulas, as motivated above.

Since boolean logical connectives say nothing themselves about computational behaviour, it is a reasonable general principle that ‘behavioural properties’ should be closed under such connectives. Thus, in keeping with criterion (C2), which asks for maximal expressivity, we close each set \(\textit{CF}(\tau )\) and \(\textit{VF}(\tau )\), of computation and value formulas, under infinitary propositional logic.

In addition to closure under infinitary propositional logic, each set \(\textit{VF}(\tau )\) contains a collection of basic value formulas, from which compound formulas are constructed using (infinitary) propositional connectives.¹ The choice of basic formulas depends on the type \(\tau \).

In the case of the natural numbers type, we include a basic value formula \(\{n\} \in \textit{VF}(\mathbf N )\), for every \(n \in \mathbb {N}\). The semantics of this formula are given by:By the closure of \( \textit{VF}(\mathbf N )\) under infinitary disjunctions, every subset of \(\mathbb {N}\) can be represented by some value formula. Moreover, since a general value formula in \( \textit{VF}(\mathbf N )\) is an infinitary boolean combination of basic formulas of the form \(\{n\}\), the value formulas represent exactly the subsets on \(\mathbb {N}\).

For the unit type, we do not require any basic value formulas. The unit type has only one value, \(*\). The two subsets of this singleton set of values are defined by the formulas \(\bot \) (‘falsum’, given as an empty disjunction), and \(\top \) (the truth constant, given as an empty conjunction).

For a function type \(\tau \rightarrow \rho \), we want each basic formula to express a fundamental behavioural constraint on values (i.e., \(\lambda \)-abstractions) W of type \(\tau \rightarrow \rho \). In keeping with the applicative nature of functional programming, the only way in which a \(\lambda \)-abstraction can be used to generate behaviour is to apply it to an argument of type \(\tau \), which, because we are in a call-by-value setting, must be a value V. The application of W to V results in a computation WV of type \(\rho \), whose properties can be probed using computation formulas in \(\textit{CF}(\rho )\). Based on this, for every value \(V \in \textit{Val}(\tau )\) and computation formula \(\varPhi \in \textit{CF}(\rho )\), we include a basic value formula \((V \mapsto \varPhi ) \in \textit{VF}(\tau \rightarrow \rho )\) with the semantics:Using this simple construct, based on application to a single argument V, other natural mechanisms for expressing properties of \(\lambda \)-abstractions are definable, using infinitary propositional logic. For example, given \(\phi \in \textit{VF}(\tau )\) and \(\varPsi \in \textit{CF}(\rho )\), the definitiondefines a formula whose derived semantics isIn Sect. 7, we shall consider the possibility of changing the basic value formulas in \(\textit{VF}(\tau \rightarrow \rho )\) to formulas \((\phi \mapsto \varPsi )\).

It remains to explain how the basic computation formulas in \(\textit{CF}(\tau )\) are formed. For this we require a given set \(\mathcal {O}\) of modalities, which depends on the algebraic effects contained in the language. The basic computation formulas in \(\textit{CF}(\tau )\) then have the form \(o\,\phi \), where \(o \in \mathcal {O}\) is one of the available modalities, and \(\phi \) is a value formula in \(\textit{VF}(\tau )\). Thus a modality ‘lifts’ properties of values of type \(\tau \) to properties of computations of type \(\tau \).

In order to give semantics to computation formulas \(o\, \phi \), we need a general theory of the kind of modality under consideration. This is one of the main contributions of the paper. Before presenting the general theory, we first consider motivating examples, using our running examples of algebraic effects.

We now give a formal treatment of the logic and its semantics, in full generality. We assume given a signature \(\varSigma \) of effect operations, as in Sect. 2. And we assume given a set \(\mathcal {O}\), whose elements we call modalities.

We call our main behavioural logic \(\mathcal {V}\), where the letter \(\mathcal {V}\) is chosen as a reference to the fact that the basic formula at function type specifies function behaviour on individual value arguments V.

In order to specify the semantics of modal formulas, we require a connection between modalities and effect trees, which is given by an interpretation functionThat is, every modality \(o \in \mathcal {O}\) is mapped to a subset \(\llbracket o \rrbracket \subseteq T\mathbf {1}\) of unit-type effect trees. Given a subset \(P \subseteq X\) (e.g. given by a formula) and a tree \(t \in TX\) we can define a unit-type tree \(t[\in \! P] \in T\mathbf 1 \) as the tree created by replacing the leaves of t that belong to P by \(*\) and the others by \(\bot \). In the case that P is the subset \(\{V \mid V~\models ~\phi \}\) specified by a formula \(\phi \in \textit{VF}(\tau )\), we also write \(t[\,\models ~\phi ]\) for \(t[\in \! P]\).

We can now formally define the two satisfaction relations \({\models } \subseteq \textit{Val}(\tau ) \times \textit{VF}(\tau )\) and \({\models } \subseteq \textit{Com}(\tau ) \times \textit{CF}(\tau )\), mutually inductively, by:We omit the evident clauses for the other propositional connectives. We remark that all conjunctions and disjunctions are semantically equivalent to countable ones, because value and computation formulas are interpreted over sets of terms, \(\textit{Val}(\tau )\) and \(\textit{Com}(\tau )\), which are countable.

We end this section by revisiting our running examples, and showing, in each case, that the example modalities presented above are all specified by suitable interpretation functions \(\llbracket \cdot \rrbracket : \mathcal {O} \rightarrow \mathcal {P}(T \mathbf {1})\).

The goal of this section is to precisely formulate our main theorem: under suitable conditions, the behavioural equivalence determined by the logic \(\mathcal {V}\) of Sect. 3 is a congruence. In order to achieve this, it will be useful to consider the positive fragment \(\mathcal {V}^+\) of \(\mathcal {V}\).

Whenever we have a logic \(\mathcal {L}\) whose value and computation formulas are given as subcollections \(\textit{VF}_\mathcal {L}(\tau ) \subseteq \textit{VF}(\tau )\) and \(\textit{CF}_\mathcal {L}(\tau ) \subseteq \textit{CF}(\tau )\), then \(\mathcal {L}\) determines a preorder (and hence also an equivalence relation) between terms of the same type and aspect.

In the case that formulas in \(\mathcal {L}\) are closed under negation, it is trivial that the preorder \(\sqsubseteq _{\mathcal {L}}\) is already an equivalence relation, and hence coincides with \(\equiv _{\mathcal {L}}\). Thus we shall only refer specifically to the preorder \(\sqsubseteq _{\mathcal {L}}\), for fragments, such as \(\mathcal {V}^+\), that are not closed under negation.

The two main relations of interest to us in this paper are the primary relations determined by \(\mathcal {V}\) and \(\mathcal {V}^+\): full behavioural equivalence \(\equiv _{\mathcal {V}}\); and the positive behavioural preorder \(\sqsubseteq _{\mathcal {V}^+}\) (which induces positive behavioural equivalence \(\equiv _{\mathcal {V}^+}\)).

We next formulate the appropriate notion of (pre)congruence to apply to the relations \(\equiv _{\mathcal {V}}\) and \(\sqsubseteq _{\mathcal {V}^+}\). These two preorders are examples of well-typed relations on closed terms. Any such relation can be extended to a relation on open terms in the following way. Given a well-typed relation \(\mathcal {R}\) on closed terms, we define the open extension \(\mathcal {R}^{\circ }\) where \(\varGamma \vdash M \mathcal {R}^{\circ } N : \tau \) precisely when, for every well-typed vector of closed values \(\overrightarrow{V} : \varGamma \), it holds that \(M[\overrightarrow{V}] \,\mathcal {R}\, N[\overrightarrow{V}]\). The correct notion of precongruence for a well-typed preorder on closed terms, is to ask for its open extension to be compatible in the sense of the definition below; see, e.g., [10, 19] for further explanation.

We now state our main congruence result, although we have not yet defined the conditions it depends upon.

The Scott-openness condition refers to the Scott topology on \(T\mathbf 1 \).

Before formulating the property of decomposability, we make some simple observations about the positive preorder \(\sqsubseteq _{\mathcal {V}^+}\).

Similar characterisations, with appropriate adjustments, hold for behavioural equivalence \(\equiv _{\mathcal {V}}\).

The decomposability property is formulated using an extension of the positive preorder \(\sqsubseteq _{\mathcal {V}^+}\), at unit type, from a relation on computations to a relation on arbitrary effect trees. Accordingly, we define a preorder \(\preceq \) on \(T\mathbf 1 \) by:

For any relation \(\mathcal {R} \subseteq X \times Y\) and subset \(A \subseteq X\), we write \(\mathcal {R}^{\uparrow } A\) for the right set \(\{y \in Y \, | \, \exists x \in A, x \mathcal {R} y \}\). This allows use to easily define our required notion.

Corollary 22 in Sect. 5, may help to motivate the formulation of the above property, which might otherwise appear purely technical. The following stronger version of decomposability, which suffices for all examples considered in the paper, is perhaps easier to understand in its own right.

We end this section by again looking at our running examples, and showing, in each case, that the identified collection \(\mathcal {O}\) of modalities is Scott-closed (hence upwards closed) and strongly decomposable (hence decomposable). For any of the examples, upwards closure is easily established, so we will not show it here.

In this section we look at an alternative description of our logical pre-order. Central to such a definition lies the concept of a relator [12, 25], which we use to lift a relation on value terms to a relation on computation terms. With our family of modalities \(\mathcal {O}\) we can define a relator which takes a relation \(\mathcal {R} \subseteq X \times Y\) and returns the relation \(\mathcal {O}(\mathcal {R}) \subseteq TX \times TY\), defined by:Note that \(\mathcal {O}(\textit{id}_\mathbf{1 }) = (\preceq )\). Following [9], we use this relation-lifting operation to define notions of applicative similarity and bisimilarity.

For brevity, we will leave out the word “applicative” from here on, and write o to mean its denotation \(\llbracket o \rrbracket \). We also introduce brackets, writing \(o[\phi ]\) for \(o \, \phi \). The key result now is that the maximal relation, the \(\mathcal {O}\)-similarity is in most cases the same object as our logical preorder. We first give a short Lemma.

Alternatively, we can look at the variation of our logic with negation. This is related to applicative bisimulations.

We end this section by stating the abstract properties of our relational lifting \(\mathcal {O}(\mathcal {R})\) required for the proof by Howe’s method in Sect. 6 to go through. The necessary properties were identified in [9]. The contribution of this paper is that all the required properties follow from our modality-based definition of \(\mathcal {O}(\mathcal {R})\).

The first set of properties tell us that \(\mathcal {O}(-)\) is a relator in the sense of [12]:

The next property together with the previous lemma establishes that \(\mathcal {O}(-)\) is a monotone relator in the sense of [25].

Finally, the following properties show that relator behaves well with respect to the order on trees.

The lemmas above list the core properties of the relator, which are satisfied when our family \(\mathcal {O}\) is decomposable and contains only Scott open modalities. The results below follow from those above.

Point 2 of Corollary 23 has been stated in such a way that it contains both the infinite arity case \(\alpha ^\mathbf{N } \rightarrow \alpha \) and the finite arity case \(\alpha ^{n} \rightarrow \alpha \). So it states that any lifted relation is preserved under any of the predefined algebraic effects.

In this section, we apply Howe’s method, first developed in [5, 6], to establish the compatibility of applicative (bi)similarity, and hence of the behavioural preorders. Given a relation \(\mathcal {R}\) on terms, one defines its Howe closure \(\mathcal {R}^{\bullet }\), which is compatible and contains the open extension \(\mathcal {R}^{\circ }\). Our proof makes fundamental use of the relator properties from Sect. 5, closely following the approach of [9].

In the proof of the proposition, the relator properties are mainly used to show that \(\sqsubseteq ^{\bullet }\) satisfies condition (2) in Definition 14.

We can now establish the compatibility of applicative \(\mathcal {O}\)-similarity.

To prove that \(\mathcal {O}\)-bisimilarity is compatible, we use the following result from [10] (where we write \(\mathcal {S}^{*}\) for the transitive-reflexive closure of a relation \(\mathcal {S}\)).

Theorem 1 is an immediate consequence of Theorems 2 and 3.

In this section, we briefly explore an alternative formulation of our logic. This has both conceptual and practical motivations. Our very approach to behavioural logic, fits into the category of endogenous logics in the sense of Pnueli [24]. Formulas (\(\phi \) and \(\varPhi \)) express properties of individual programs, through satisfaction relations (\(V~\models ~\phi \) and \(M \models ~\varPhi \)). Programs are thus considered as ‘models’ of the logic, with the satisfaction relation being defined via program behaviour.

It is conceptually appealing to push the separation between program and logic to its natural conclusion, and ask for the syntax of the logic to be independent of the syntax of the programming language. Indeed, it seems natural that it should be possible to express properties of program behaviour without knowledge of the syntax of the programming language. Under our formulation of the logic \(\mathcal {V}\), this desideratum is violated by the value formula \((V \mapsto \varPsi )\) at function type, which mentions the programming language value V.

This issue can be addressed, by replacing the basic value formula \((V \mapsto \varPsi )\) with the alternative \((\phi \mapsto \varPsi )\), already mentioned in Sect. 3. Such a change also has a practical motivation. The formula \((\phi \mapsto \varPsi )\) declares a precondition and postcondition for function application, supporting a useful specification style.

Combining the above proposition with Theorem 1 we obtain the following.

We do not know any proof of the compatibility of the \(\equiv _{\mathcal {F}}\) and \(\sqsubseteq _{\mathcal {F}^+}\) relations that does not go via the logic \(\mathcal {V}\). In particular, the compatibility property of the \(\mathbf{fix }\) operator seems difficult to establish directly for \(\equiv _{\mathcal {F}}\) and \(\sqsubseteq _{\mathcal {F}^+}\).

The behavioural logics considered in this paper are designed for the purpose of clarifying the notion of ‘behavioural property’, and for defining behavioural equivalence. As infinitary propositional logics, they are not directly suited to practical applications such as specification and verification. Nevertheless, they serve as low-level logics into which more practical finitary logics can be translated. For this, the closure of the logics under infinitary propositional logic is important. For example, there are standard translations of quantifiers and least and greatest fixed points into infinitary propositional logic. Also, in the case of global store, Hoare triples translate into logical combinations of modal formulas.

Our approach, of basing logics for effects on behavioural modalities, may potentially inform the design of practical logics for specifying and reasoning about effects. For example, Pitts’ evaluation logic was an early logic for general computational effects [18]. In the light of the general theory of modalities in the present paper, it seems natural to replace the built-in \(\Box \) and \(\Diamond \) modalities of evaluation logic, with effect-specific modalities, as in Sect. 3.

The logic for algebraic effects, of Plotkin and Pretnar [23], axiomatises effectful behaviour by means of an equational theory over the signature of effect operations, following the algebraic approach to effects advocated by Plotkin and Power [22]. Such equational axiomatisations are typically sound with respect to more than one notion of program equivalence. The logic of [23] can thus be used to soundly reason about program equivalence, but does not in itself determine a notion of program equivalence. Instead, our logic is specifically designed as a vehicle for defining program equivalence. In doing so, our modalities can be viewed as a chosen family of ‘observations’ that are compatible with the effects present in the language. It is the choice of modalities that determines the equational properties that the effect operations satisfy.

The logic of [23] itself makes use of modalities, called operation modalities, each associated with a single effect operations in \(\varSigma \). It would be natural to replace these modalities, which are syntactic in nature, with behavioural modalities of the form we consider. Similarly, our behavioural modalities appear to offer a promising basis for developing a modality-based refinement-type system for algebraic effects. In general, an important advantage we see in the use of behavioural modalities is that our notion of strong decomposability appears related to the availability of compositional proof principles for modal properties. This is a promising avenue for future exploration.

A rather different approach to logics for effects has been proposed by Goncharov, Mossakowski and Schröder [3, 16]. They assume a semantic setting in which the programming language is rich enough to contain a pure fragment that itself acts as a program logic. This approach is very powerful for certain effects. For example, Hoare logic can be derived in the case of global store. However, it appears not as widely adaptable across the range of effects as our approach.

Our logics exhibit certain similarities in form with the endogenous logic developed in Abramsky’s domain theory in logical form [2]. Our motivation and approach are, however, quite different. Whereas Abramsky shows the usefulness of an axiomatic approach to a finitary logic as a way of characterising denotational equality, the present paper shows that there is a similar utility in considering an infinitary logic from a semantic perspective (based on operational semantics) as a method of defining behavioural equivalence.

The work in this paper has been carried out for fine-grained call-by-value [13], which is equivalent to call-by-value. The definitions can, however, be adapted to work for call-by-name, and even call-by-push-value [11]. Adding type constructors such as sum and product is also straightforward. We have not checked the generalisation to arbitrary recursive types, but we do not foresee any problem.

An omission from the present paper is that we have not said anything about contextual equivalence, which is often taken to be the default equivalence for applicative languages. In addition to determining the logically defined preorders/equivalences, the choice of the set \(\mathcal {O}\) of modalities gives rise to a natural definition of contextual preorder, namely the largest compatible preorder that, on computations of unit type \(\mathbf {1}\), is contained in the \(\preceq \) relation from Sect. 4. The compatibility of \(\sqsubseteq _{\mathcal {V}^+}\) established in the present paper means that we have the expected relation inclusions \({\equiv _\mathcal {V}}\, \subseteq \, {\sqsubseteq _{\mathcal {V}^+}} \,\subseteq \,{\sqsubseteq _\text {ctxt}}\). It is an interesting question whether the logic can be restricted to characterise contextual equivalence/preorder. A more comprehensive investigation of contextual equivalence is being undertaken, in ongoing work, by Aliame Lopez and the first author.

The crucial notion of modality, in the present paper, was adapted from the notion of observation in [8]. The change from a set of trees of type \(\mathbf N \) (an observation) to a set of unit-type trees (a modality) allows value formulas to be lifted to computation formulas, analogously to predicate lifting in coalgebra [7], which is a key characteristic of our modalities. Properties of Scott-openness and decomposability play a similar role the present paper to the role they play in [8]. However, the notion of decomposability for modalities (Definition 11) is more subtle than the corresponding notion for observations in [8].

There are certain limitations to the theory of modalities in the present paper. For example, for the combination of probability and nondeterminism, one might naturally consider modalities \(\Diamond \mathsf {P}_r\) and \(\Box \mathsf {P}_r\) asserting the possibility and necessity of the termination probability exceeding r. However, the decomposability property fails. It appears that this situation can be rescued by changing to a quantitative logic, with a corresponding notion of quantitative modality. This is a topic of ongoing research.