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 below

The 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.

Typing rules

Full size image

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].)

Example 0

(Pure functional computation). This is the trivial case (from an effect point of view) in which the signature \(\varSigma \) of effect operations is empty. The resulting language is a call-by-value variant of PCF [20].

Example 1

(Error). We take a set of error labels E. For each \(e \in E\) there is an effect operator \(\textit{raise}_e: \alpha ^0 \rightarrow \alpha \) which, when invoked by the computation \(\textit{raise}_e()\), aborts evaluation and outputs e as an error message.

Example 2

(Nondeterminism). There is a binary choice operator \(\textit{or}: \alpha ^2 \rightarrow \alpha \) which gives two options for continuing the computation. The choice of continuation is under the control of some external agent, which one may wish to model as being cooperative (angelic), antagonistic (demonic), or neutral.

Example 3

(Probabilistic choice). Again there is a single binary choice operator \(\textit{p-or}: \alpha ^2 \rightarrow \alpha \) which gives two options for continuing the computation. In this case, the choice of continuation is probabilistic, with a \(\frac{1}{2}\) probability of either option being chosen. Other weighted probabilistic choices can be programmed in terms of this fair choice operation.

Example 4

(Global store). We take a set of locations L for storing natural numbers. For each \(l \in L\) we have \(\textit{lookup}_l: \alpha ^\mathbf{N } \rightarrow \alpha \) and \(\textit{update}_l: \mathbf N \times \alpha \rightarrow \alpha \). The computation \(\textit{lookup}_l(V)\) looks up the number at location l and passes it as an argument to the function V, and \(\textit{update}_l(\overline{n};M)\) stores n at l and then continues with the computation M.

Example 5

(Input/output). Here we have two operators, \(\textit{read}: \alpha ^\mathbf{N } \rightarrow \alpha \) which reads a number from an input channel and passes it as the argument to a function, and \(\textit{write}: \mathbf N \times \alpha \rightarrow \alpha \) which outputs a number (the first argument) and then continues as the computation given as the second argument.

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’.

Definition 1

An effect tree (henceforth tree), over a set X, determined by a signature \(\varSigma \) of effect operations, is a labelled and possibly infinite tree whose nodes have the possible forms.

1. 1.

   A leaf node labelled with \(\bot \) (the symbol for nontermination).

2. 2.

   A leaf node labelled with x where \(x \in X\).

3. 3.

   A node labelled \(\sigma \) with children \(t_0,\dots , t_{n-1}\), when \(\sigma \in \varSigma \) has arity \(\alpha ^n \rightarrow \alpha \).

4. 4.

   A node labelled \(\sigma \) with children \(t_0,t_1,\dots \), when \(\sigma \in \varSigma \) has arity \(\alpha ^\mathbf{N } \rightarrow \alpha \).

5. 5.

   A node labelled \(\sigma _m\) where \(m \in \mathbb {N}\) with children \(t_0,\dots , t_{n-1}\), when \(\sigma \in \varSigma \) has arity \(\mathbf N \times \alpha ^n \rightarrow \alpha \).

6. 6.

   A node labelled \(\sigma _m\) where \(m \in \mathbb {N}\) with children \(t_0,t_1,\dots \), when \(\sigma \in \varSigma \) has arity \(\mathbf N \times \alpha ^\mathbf{N } \rightarrow \alpha \).

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\).

Example 3

(Nondeterminism). Nondeterministically generate a natural number:

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 relations

which 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.  

(C1):

The logic should express only ‘behaviourally meaningful’ properties of programs. This guides us to build the logic upon primitive notions that have a direct behavioural interpretation according to a natural understanding of program behaviour.

(C2):

The logic should be as expressive as possible within the constraints imposed by criterion (C1).

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.^{Footnote 1} 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 definition

defines a formula whose derived semantics is

In 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.

Example 0

(Pure functional computation). Define \(\mathcal {O} = \{{\downarrow }\}\). Here the single modality \(\downarrow \) is the termination modality: \({\downarrow \! \phi }\) asserts that a computation terminates with a return value V satisfying \(\phi \). This is formalised using effect trees:

Note that, in the case of pure functional computation, all trees are leaves: either value leaves V, or nontermination leaves \(\bot \).

Example 1

(Error). Define \(\mathcal {O} = \{{\downarrow }\} \cup \{\mathsf {E}_e \mid e \in E\}\). The semantics of the termination modality \(\downarrow \) is defined as above. The error modality \(\mathsf {E}_e\) flags error e:

(Because \(\textit{raise}_e\) is an operation of arity 0, a \(\textit{raise}_e\) node in a tree has 0 children.) Note that the semantics of \(\mathsf {E}_e \phi \) makes no reference to \(\phi \). Indeed it would be natural to consider \(\mathsf {E}_e\) as a basic computation formula in its own right, which could be done by introducing a notion of 0-argument modality, and considering \(\mathsf {E}_e\) as such. In this paper, however, we keep the treatment uniform by always considering modalities as unary operations, with natural 0-argument modalities subsumed as unary modalities with redundant argument.

Example 2

(Nondeterminism). Define \(\mathcal {O} = \{\Diamond , \, \Box \}\) with:

Including both modalities amounts to a neutral view of nondeterminism. In the case of angelic nondeterminism, one would include just the \(\Diamond \) modality; in that of demonic nondeterminism, just the \(\Box \) modality. Because of the way the semantic definitions interact with termination, the modalities \(\Box \) and \(\Diamond \) are not De Morgan duals. Indeed, each of the three possibilities \(\{\Diamond , \, \Box \}, \{\Diamond \}, \{\Box \}\) for \(\mathcal {O}\) leads to a logic with a different expressivity.

Example 3

(Probabilistic choice). Define \(\mathcal {O} = \{ \mathsf {P}_{>q} \mid q \in \mathbb {Q},\, 0 \le q < 1\}\) with:

where the probability on the right is the probability that a run through the tree |M|, starting at the root, and making an independent fair probabilistic choice at each branching node, terminates at a value node with a value V in the set \(\{V \mid V \models ~\phi \}\). We observe that the restriction to rational thresholds q is immaterial, as, for any real r with \(0 \le r < 1\), we can define:

Similarly, we can define non-strict threshold modalities, for \(0 < r \le 1\), by:

Also, we can exploit negation to define modalities expressing strict and non-strict upper bounds on probabilities. Notwithstanding the definability of non-strict and upper-bound thresholds, we shall see later that it is important that we include only strict lower-bound modalities in our set \(\mathcal {O}\) of primitive modalities.

Example 4

(Global store). For a set of locations L, define the set of states by \(\textit{State} = \mathbb {N}^L\). The modalities are \(\mathcal {O} = \{(s \rightarrowtail r) \mid s,r \in \textit{State}\}\), where informally:

We make the above definition precise using the effect tree of M. Define

for any set X, to be the least partial function satisfying:

where \(s[l:=n]\) is the evident modification of state s. Intuitively, \(\textit{exec}(t,s)\) defines the result of “executing” the tree of commands in effect tree t starting in state s, whenever this execution terminates. In terms of operational semantics, it can be viewed as defining a ‘big-step’ semantics for effect trees (in the signature of global store). We can now define the semantics of the \( (s \rightarrowtail r)\) modality formally:

Example 5

(Input/output). Define an i/o-trace to be a word w over the alphabet

The idea is that such a word represents an input/output sequence, where ?n means the number n is given in response to an input prompt, and !n means that the program outputs n. Define the set of modalities

The intuitive semantics of these modalities is as follows.

In order to define the semantics of formulas precisely, we first define relations \(t~\models ~ {\langle w \rangle \!\!\downarrow }\, P\) and \(t~\models ~ {\langle w\rangle _{\!\dots }}\), between \(t \in TX\) and \(P \subseteq X\), by induction on words (Note that we are overloading the \(\models \) symbol.) In the following, we write \(\varepsilon \) for the empty word, and we use textual juxtaposition for concatenation of words.

The formal semantics of modalities is now easily defined by:

Note that, as in Example 1, the formula argument of the \({\langle w\rangle _{\!\dots }}\) modality is redundant. Also, note that our modalities for input/output could naturally be formed by combining the termination modality \(\downarrow \), which lifts value formulas to computation formulas, with sequences of atomic modalities \(\langle ?n\rangle \) and \(\langle !n\rangle \) acting directly on computation formulas. In this paper, we do not include such modalities, acting on computation formulas, in our general theory. But this is a natural avenue for future consideration.

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.

The logic \(\mathcal {V}\)

Full size image

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.

Definition 2

(The logic \(\mathcal {V}\)). The classes \(\textit{VF}(\tau )\) and \(\textit{CF}(\tau )\) of value and computation formulas, for each type \(\tau \), are mutually inductively defined by the rules in Fig. 2. In this, I can be instantiated to any set, allowing for arbitrary conjunctions and disjunctions. When I is \(\emptyset \), we get the special formulas \(\top = \bigwedge _{\emptyset }\) and \(\bot = \bigvee _{\emptyset }\). The use of arbitrary index sets means that formulas, as defined, form a proper class. However, we shall see below that countable index sets suffice.

In order to specify the semantics of modal formulas, we require a connection between modalities and effect trees, which is given by an interpretation function

That 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})\).

Example 0

(Pure functional computation). We have \(\mathcal {O} = \{{\downarrow }\}\). Define:

Example 1

(Error). We have \(\mathcal {O} = \{{\downarrow }\} \cup \{\mathsf {E}_e \mid e \in E\}\). Define:

Example 2

(Nondeterminism). We have \(\mathcal {O} = \{\Diamond , \, \Box \}\). Define:

Example 3

(Probabilistic choice). \(\mathcal {O} = \{ \mathsf {P}_{>q} \mid q \in \mathbb {Q},\, 0 \le q < 1\}\). Define:

Example 4

(Global store). \(\mathcal {O} = \{(s \rightarrowtail r) \mid s,r \in \textit{State}\}\). Define:

Example 5

(Input/output). \(\mathcal {O} = \{{\langle w \rangle \!\!\downarrow },\, \langle w\rangle _{\!\dots } \mid w~ \text {an i/o-trace}\}\). Define:

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}\).

Definition 3

(The logic \(\mathcal {V}^+\)). The logic \(\mathcal {V}^+\) is the fragment of \(\mathcal {V}\) consisting of those formulas in \(\textit{VF}(\tau )\) and \(\textit{CF}(\tau )\) that do not contain negation.

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.

Definition 4

(Logical preorder and equivalence). Given a fragment \(\mathcal {L}\) of \(\mathcal {V}\), we define the logical preorder \(\sqsubseteq _{\mathcal {L}}\), between well-typed terms of the same type and aspect, by:

The logical equivalence \(\equiv _{\mathcal {L}}\) on terms is the equivalence relation induced by the preorder (the intersection of \(\sqsubseteq _{\mathcal {L}}\) and its converse).

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.

Definition 5

(Compatibility). A well-typed open relation \(\mathcal {R}\) is said to be compatible if it is closed under the rules in Fig. 3.

Rules for compatibility

Full size image

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

Theorem 1

If \(\mathcal {O}\) is a decomposable set of Scott-open modalities then the open extensions of \(\equiv _{\mathcal {V}}\) and \(\sqsubseteq _{\mathcal {V}^+}\) are both compatible. (It is an immediate consequence that the open extension of \(\equiv _{\mathcal {V}^+}\) is also compatible.)

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

Definition 6

We say that \(o \in \mathcal {O}\) is upwards closed if \(\llbracket o \rrbracket \) is an upper-closed subset of \(T\mathbf 1 \); i.e., if \(t \in \llbracket o \rrbracket \) implies \(t' \in \llbracket o \rrbracket \) whenever \(t \le t'\).

Definition 7

We say that \(o \in \mathcal {O}\) is Scott-open if \(\llbracket o \rrbracket \) is an open subset in the Scott topology on \(T\mathbf 1 \); i.e., \(\llbracket o \rrbracket \) is upper closed and, whenever \(t_1 \le t_2 \le \dots \) is an ascending chain in \(T\mathbf 1 \) with supremum \(\sqcup _i t_i \in \llbracket o \rrbracket \), we have \(t_n \in \llbracket o \rrbracket \) for some n.

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

Lemma 8

For any \(V_0, V_1 \in \textit{Val}(\rho \rightarrow \tau )\), we have \(V_0 \sqsubseteq _{\mathcal {V}^+} V_1\) if and only if:

Lemma 9

For any \(M_0, M_1 \in \textit{Com}(\tau )\), we have \(M_0 \sqsubseteq _{\mathcal {V}^+} M_1\) if and only if:

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:

Proposition 10

For computations \(M, N \in \textit{Com}(\mathbf {1})\), it holds that \(|M| \preceq |N|\) if and only if \(M \sqsubseteq _{\mathcal {V}^+} N\).

Proof

The defining condition for \(|M| \preceq |N|\) unwinds to:

This coincides with \(M \sqsubseteq _{\mathcal {V}^+} N\) by Lemma 9.    \(\square \)

We now formulate the required notion of decomposability. We first give the general definition, and then follow it with a related notion of strong decomposability, which can be more convenient to establish in examples. Both definitions are unavoidably technical in nature.

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.

Definition 11

(Decomposability). We say that \(\mathcal {O}\) is decomposable if, for all \(r,r' \in TT\mathbf 1 \), we have:

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.

Definition 12

(Strong decomposability). We say that \(\mathcal {O}\) is strongly decomposable if, for every \(r \in TT\mathbf 1 \) and \(o \in \mathcal {O}\) for which \(\mu r \in \llbracket o \rrbracket \), there exists a collection \(\{(o_i,o_i')\}_{i \in I}\) of pairs of modalities such that:

1. 1.

   \(\forall i \in I, ~ r[\in \llbracket o_i' \rrbracket ]\in \llbracket o_i \rrbracket \,\); and

2. 2.

   for every \(r' \in TT\mathbf 1 \), \((\,\forall i \in I, ~ r'[\in \llbracket o_i' \rrbracket ]\in \llbracket o_i \rrbracket \,)\) implies \(\mu r' \in \llbracket o \rrbracket \).

Proposition 13

If \(\mathcal {O}\) is a strongly decomposable then it is decomposable.

Proof

Suppose that \(r[\in A] \preceq r'[\in ({\preceq ^{\uparrow }\! A)}]\) holds for every \(A \subseteq T\mathbf 1 \). Assume that \(\mu r \in \llbracket o \rrbracket \in \mathcal {O}\). Then strong decomposability gives a collection \(\{(o_i,o_i')\}_I\). By the definition of \(\preceq \), for each \(o_i'\) we have \({\preceq ^{\uparrow }\! \llbracket o_i' \rrbracket } = \llbracket o_i' \rrbracket \). By the initial assumption, \(r[\in \llbracket o_i' \rrbracket ]\in \llbracket o_i \rrbracket \) implies \(r'[\in (\preceq ^{\uparrow } \! \llbracket o_i' \rrbracket )] \in \llbracket o_i \rrbracket \), and hence \(r'[\in \llbracket o_i' \rrbracket ] \in \llbracket o_i \rrbracket \). This holds for every i, so by strong decomposability \(\mu r' \in \llbracket o \rrbracket \). We have shown that \(\mu r \in \llbracket o \rrbracket \) implies \(\mu r' \in \llbracket o \rrbracket \). One can prove similarly that \(\mu r[\in \emptyset ] \in \llbracket o \rrbracket \) implies that \(\mu r'[\in \emptyset ] \in \llbracket o \rrbracket \) by observing that \(\preceq ^{\uparrow } \{x \,|\, x[\in \emptyset ] \in \llbracket o_i'\rrbracket \} = \{x \,|\, x[\in \emptyset ] \in \llbracket o_i'\rrbracket \}\). Thus it holds that \(\mu r \preceq \mu r'\) and hence \(\mathcal {O}\) is decomposable.    \(\square \)

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.

Example 0

(Pure functional computation). We have \(\mathcal {O} = \{{\downarrow }\}\) and \( \llbracket {\downarrow } \rrbracket = \{\, * \, \}\). Scott openness holds since if \(\sqcup _i t_i = *\) then for some i we must already have \(t_i = *\). It is strongly decomposable since: \(\mu r \in \llbracket \downarrow \rrbracket \Leftrightarrow r[\in \llbracket \downarrow \rrbracket ] \in \llbracket \downarrow \rrbracket \), which means r returns a tree t which is a leaf \(*\).

Example 1

(Error). We have \(\mathcal {O} = \{{\downarrow }\} \cup \{\mathsf {E}_e \mid e \in E\}\) and \( \llbracket {\mathsf {E}_e} \rrbracket = \{\, \textit{raise}_e \, \}\). Scott-openness holds for both modalities for the same reason as in the previous example, and its strongly decomposable since:

Which means r returns a tree t which returns \(*\).

Which means r raises an error, or returns a tree that raises an error.

Example 2

(Nondeterminism). We have \(\mathcal {O} = \{\Diamond , \, \Box \}\). The Scott-openness of \(\llbracket {\Diamond } \rrbracket = \{ t \mid ~t~\text {has some * leaf} \}\) is because if \(\sqcup _i t_i\) has a \(*\) leaf, then that leaf must already be contained in \(t_i\) for some i. Similarly, if \(\sqcup _i t_i \in \llbracket {\Box } \rrbracket \) then, because \(\llbracket {\Box } \rrbracket = \{ t \mid \)t\(~\text {has finite height and every leaf is a} *\}\), the tree \(\sqcup _i t_i\) has finitely many leaves and all must be contained in \(t_i\) for some i. Hence \(t_i \in \llbracket {\Box } \rrbracket \). Strong decomposability holds because:

The right-hand-side of the former states that r has as a leaf a tree t, which itself has a leaf \(*\). That of the latter states that r is finite and all leaves are finite trees t that have only \(*\) leaves. The same arguments show that \(\{\Diamond \}\) and \(\{\Box \}\) are also decomposable sets of Scott open modalities.

Example 3

(Probabilistic choice). \(\mathcal {O} = \{ \mathsf {P}_{>q} \mid q \in \mathbb {Q},\, 0 \le q < 1\}\). For the Scott-openness of \(\llbracket \mathsf {P}_{>q} \rrbracket = \{ t \mid \mathbf {P} (\,t~\text {terminates with a * leaf}\,)~>~q\}\), note that \(\mathbf {P}(\,\sqcup _i t_i~\text {terminates with a} * \mathrm{leaf}\,)\) is determined by some countable sum over the leaves of \(t_i\). If this sum is greater than a rational q, then some finite approximation of the sum must already be above q. The finite sum is over finitely many leaves from \(\sqcup _i t_i\), all of which will be present in \(t_i\) for some i. Hence \(t_i \in \llbracket \mathsf {P}_{>q} \rrbracket \).

We have strong decomposability, since \(\mathbf {P}(\,\mu r~ \text {terminates with a} * \mathrm{leaf}\,)\) equals the integral of the function \(f_r(x) = \textit{sup}\{y \in [0,1] \, | \, r[\llbracket \mathsf {P}_{>x} \rrbracket ] \in \llbracket \mathsf {P}_{>y} \rrbracket \}\) from [0, 1] to [0, 1]. Indeed, \(f_r(x)\) gives the probability that r return a tree \(t \in \llbracket \mathsf {P}_{>x} \rrbracket \). So we know that if \(\forall x,y, r[\llbracket \mathsf {P}_{>x} \rrbracket ] \in \llbracket \mathsf {P}_{>y} \rrbracket \Rightarrow r'[\llbracket \mathsf {P}_{>x} \rrbracket ] \in \llbracket \mathsf {P}_{>y} \rrbracket \), then \(f_{r'}(x) \ge f_r(x)\) for any x. Hence if \(\mu r \in \llbracket \mathsf {P}_{>q} \rrbracket \) then \(\int f_r > q\), whence also \(\int f_{r'} > q\), which means \(\mu r' \in \llbracket \mathsf {P}_{>q} \rrbracket \).

Example 4

(Global store). We have \(\mathcal {O} = \{(s \rightarrowtail s') \mid s,s' \in \textit{State}\}\). For the Scott-openness of \(\llbracket (s \rightarrowtail s') \rrbracket = \{ t \mid \textit{exec}(t,s) = (*,r)\}\), note that if \(\textit{exec}(\sqcup _i t_i,s) = (*,s')\), there is a single finite branch of t that follows the path the recursive function \(\textit{exec}\) took. This branch must already be contained in \(t_i\) for some i. We also have strong decomposability since:

Which just means that \(\textit{exec}(r,s) = (t,s'')\) and \(\textit{exec}(t,s'') = (*,s')\) for some \(s''\).

Example 5

(Input/output). We have \(\mathcal {O} = \{{\langle w \rangle \!\!\downarrow },\, \langle w\rangle _{\!\dots } \mid w~\text {an i/o-trace}\}\). For the Scott-openness of \(\llbracket \langle w \rangle \!\!\downarrow \,\rrbracket = \{ t \mid t~\models ~ {\langle w \rangle \!\!\downarrow }\, \{*\}\, \}\), note that the i/o-trace \(\langle w \rangle \!\!\downarrow \) is given by some finite branch, which if in \(\sqcup _i t_i\) must be in \(t_i\) for some i. The Scott-openness of \(\llbracket \langle w\rangle _{\!\dots } \, \rrbracket = \{ t \mid t~\models ~ \langle w\rangle _{\!\dots }\, \}\) holds for similar reasons. We have strong decomposability because of the implications:

Which means r follows trace v returning t, and t follows trace u returning \(*\).

Which means either r follows trace w immediately, or it follows v returning a tree that follows u.

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.

Definition 14

An applicative \(\mathcal {O}\)-simulation is given by a pair of relations \(\mathcal {R}^v_{\tau }\) and \(\mathcal {R}^c_{\tau }\) for each type \(\tau \), where \(\mathcal {R}^v_{\tau } \subseteq \textit{Val}(\tau )^2\) and \(\mathcal {R}^c_{\tau } \subseteq \textit{Com}(\tau )^2\), such that:

1. 1.

   \(V \mathcal {R}^v_\mathbf{N } W ~ \Rightarrow ~ (V = W)\)

2. 2.

   \(M \mathcal {R}^c_{\tau } N~ \Rightarrow ~|M|\) \(\mathcal {O}(\mathcal {R}^v_{\tau })\) |N|

3. 3.

   \(V \mathcal {R}^v_{\rho \rightarrow \tau } W ~\Rightarrow ~\forall U \in \textit{Val}(\rho ), \; VU \; \mathcal {R}^c_{\tau } \; WU\)

Applicative \(\mathcal {O}\)-similarity is the largest applicative \(\mathcal {O}\)-simulation, which is equal to the union of all applicative \(\mathcal {O}\)-simulations.

Definition 15

An applicative \(\mathcal {O}\)-bisimulation is a symmetric \(\mathcal {O}\)-simulation. The relation of \(\mathcal {O}\)-bisimilarity is the largest applicative \(\mathcal {O}\)-bisimulation.

Lemma 16

Applicative \(\mathcal {O}\)-bisimilarity is identical to the relation of applicative \((\mathcal {O} \cap \mathcal {O}^{\mathsf {op}})\)-similarity, where \(t (\mathcal {O} \cap \mathcal {O}^{\mathsf {op}})(\mathcal {R}) r \Leftrightarrow t \mathcal {O} (\mathcal {R}) r \wedge r \mathcal {O} (\mathcal {R}^{\mathsf {op}}) t\).

Proof

Let \(\mathcal {R}\) be the \(\mathcal {O}\)-bisimilarity, then by symmetry we have \(\mathcal {R}^{\mathsf {op}} = \mathcal {R}\). So if \(M \mathcal {R} N\) we have \(N \mathcal {R} M\), and by the simulation rules we derive \(|M| \mathcal {O} (\mathcal {R}) |N|\) and \(|N| \mathcal {O} (\mathcal {R}) |M|\) which is what we needed.

Let \(\mathcal {R}\) be the \(\mathcal {O} \cap \mathcal {O}^{\mathsf {op}}\)-similarity. If \(M \mathcal {R}^{\mathsf {op}} N\) then \(|N| (\mathcal {O} \cap \mathcal {O}^{\mathsf {op}})(\mathcal {R}) |M|\) so \(|N| \mathcal {O} (\mathcal {R}) |M| \wedge |M| \mathcal {O} (\mathcal {R}^{\mathsf {op}}) |N|\) which results in \(|M| (\mathcal {O} \cap \mathcal {O}^{\mathsf {op}})(\mathcal {R}^{\mathsf {op}}) |N|\). Verifying the other simulation conditions as well, we can conclude that the symmetric closure \(\mathcal {R} \cup \mathcal {R}^{\mathsf {op}}\) is also a \(\mathcal {O} \cap \mathcal {O}^{\mathsf {op}}\)-simulation. So \(\mathcal {R}\) must, as the largest such simulation, be symmetric. Hence \(\mathcal {R}\) is a symmetric \(\mathcal {O}\)-simulation as well.

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.

Lemma 17

For any fragment \(\mathcal {L}\) of \(\mathcal {V}\) closed under countable conjunction, it holds that for each value V there is a formula \(\chi _V \in \mathcal {L}\) s.t. \(W~\models _{\mathcal {L}} \chi _V \Leftrightarrow V \sqsubseteq _{\mathcal {L}}~W\).

Proof

For each U such that \((V \not \sqsubseteq _{\mathcal {L}} U)\), choose a formula \(\phi ^U \in \mathcal {L}\) such that \(V \models _{\mathcal {L}} \phi ^U\) and \((U \not \models ~\phi ^U)\). Then if we define \(\chi _V := \bigwedge _{\{U \mid V \not \sqsubseteq _{\mathcal {L}} U\}} \phi ^U\) it holds that \(V \not \sqsubseteq _{\mathcal {L}} U \Leftrightarrow U \not \models \chi _V\), which is what we want.

Theorem 2

(a). For any family of upwards closed modalities \(\mathcal {O}\), we have that the logical preorder \(\sqsubseteq _{\mathcal {V}^+}\) is identical to \(\mathcal {O}\)-similarity.

Proof

We write \(\sqsubseteq \) instead of \(\sqsubseteq _{\mathcal {V}^+}\) to make room for other annotations. We first prove that our logical preorder \(\sqsubseteq \) is an \(\mathcal {O}\)-simulation by induction on types.

1. 1.

   Values of \(\mathbf N \). If \(\overline{n} \sqsubseteq ^v_\mathbf{N } \overline{m}\), then since \(\overline{n} \models ~\{n\}\) we have that \(\overline{m}~\models ~\{n\}\), hence \(m=n\).

2. 2.

   Computations of \(\tau \). Assume \(M \sqsubseteq ^c_{\tau } N\), we prove that \(|M| \mathcal {O}(\sqsubseteq ^v_{\tau }) |N|\). Take \(A \subseteq \textit{Val}(\tau )\) and \(o \in \mathcal {O}\) such that \(|M|[\in A] \in o\). Taking the following formula \(\phi := \bigvee _{a \in A} \chi _a\) (where \(\chi _a\) as in Lemma 17), then \(b \models ~\phi \Leftrightarrow \exists a \in A, a \sqsubseteq ^v_{\tau } b\) and \(a \in A \Rightarrow a~\models \phi \). So \(|M|[\models ~\phi ] \ge |M|[\in A]\), hence since o is upwards closed, \(|M|[\models ~\phi ] \in o\). By \(M \sqsubseteq ^c_{\tau } N\) we have \(|N|[\in \{b \in \textit{Val}(\tau ) \,|\, \exists a \in A, a \sqsubseteq ^v_{\tau } b\}] = |N|[\models ~\phi ] \in o\). Hence we can conclude that \(|M| \mathcal {O}(\sqsubseteq ^v_{\tau }) |N|\).

3. 3.

   Function values of \(\rho \rightarrow \tau \), this follows from Lemma 8 and the Induction Hypothesis.

We can conclude that \(\sqsubseteq \) is an \(\mathcal {O}\)-simulation. Now take an arbitrary \(\mathcal {O}\)-simulation \(\mathcal {R}\). We prove by induction on types that \(\mathcal {R} \subseteq (\sqsubseteq )\).

1. 1.

   Values of \(\mathbf N \). If \(V \mathcal {R}^v_\mathbf{N } W\) then \(V=W\), hence by reflexivity we get \(V \sqsubseteq ^v_\mathbf{N } W\).

2. 2.

   Computations of \(\tau \). Assume \(M \mathcal {R}^c_{\tau } N\), we prove that \(M \sqsubseteq ^c_{\tau } N\) using the characterisation from Lemma 9. Say for \(o \in \mathcal {O}\) and \(\phi \in \textit{VF}(\tau )\) we have \(M~\models ~o[\phi ]\). Let \(A_{\phi } := \{a \in \textit{Val}(\tau ) \,|\, a~\models ~\phi \} \subseteq \textit{Val}(\tau )\), then \(|M|[\in A_{\phi }] = |M|[\models ~\phi ] \in o\) hence by \(M \mathcal {R}^c_{\tau } N\) we derive \(|N|[\in \{b \in \textit{Val}(\tau ) \,|\, \exists a \in A_{\phi }, a \mathcal {R}^v_{\tau } b \}] \in o\). By Induction Hypothesis on values of \(\tau \), we know that \(\mathcal {R}^v_{\tau } \subseteq (\sqsubseteq ^v_{\tau })\), hence ‘\(\exists a \in A_{\phi }, a \mathcal {R}^v_{\tau } b\)’ implies \(b~\models ~\phi \). We get that \(|N|[\models ~\phi ] \ge |N|[\in \{b \in \textit{Val}(\tau ) \,|\, \exists a \in A_{\phi }, a \mathcal {R}^v_{\tau } b \}]\), so by upwards closure of o we have \(|N|[\models ~\phi ] \in o\) meaning \(N~\models ~o[\phi ]\). We conclude that \(M \sqsubseteq ^c_{\tau } N\).

3. 3.

   Function values of \(\rho \rightarrow \tau \), assume \(V \mathcal {R}^v_{\rho \rightarrow \tau } W\). We prove \(V \sqsubseteq ^v_{\rho \rightarrow \tau } W\) using the characterisation from Lemma 8. Assume \(V~\models ~(U \mapsto \varPhi )\) where \(U \in \textit{Val}(\rho )\) and \(\varPhi \in \textit{CF}(\tau )\), so \(VU~\models ~\varPhi \). By \(V \mathcal {R}^v_{\rho \rightarrow \tau } W\) we have \(VU \; \mathcal {R}^c_{\tau } \; WU\) and by Induction Hypothesis we have \(\mathcal {R}^c_{\tau } \subseteq (\sqsubseteq ^c_{\tau })\), so \(VU \sqsubseteq ^c_{\tau } WU\). Hence \(WU~\models ~\varPhi \) meaning \(W \models ~(U \mapsto \varPhi )\). We can conclude that \(V \sqsubseteq ^v_{\rho \rightarrow \tau } W\).

4. 4.

   Values of \(\mathbf {1}\). If \(V \mathcal {R}^v_\mathbf{{1}} W\) then \(V=*=W\) hence \(V \sqsubseteq ^v_\mathbf{{1}} W\).

In conclusion: any \(\mathcal {O}\)-simulation \(\mathcal {R}\) is a subset of the \(\mathcal {O}\)-simulation \(\sqsubseteq _{\mathcal {V}^+}\). So \(\sqsubseteq _{\mathcal {V}^+}\) is \(\mathcal {O}\)-similarity.    \(\square \)

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

Theorem 2

(b). For any family of upwards closed modalities \(\mathcal {O}\), we have that the logical equivalence \(\equiv _{\mathcal {V}}\) is identical to \(\mathcal {O}\)-bisimilarity.

Proof

Note first that \(\equiv _{\mathcal {V}}\) is symmetric.

Secondly, note that since \(\equiv _{\mathcal {V}} = \sqsubseteq _{\mathcal {V}}\) we know by Lemma 17, that for any V, there is a formula \(\chi _V\) such that \(W~\models ~\chi _V \Leftrightarrow V \equiv _{\mathcal {V}} W\).

Using these special formulas \(\chi _V\), the rest of the proof is very similar to the proof in Theorem 2(a). Here follow the non-trivial parts of the proof, different from the previous lemma. For proving \(\equiv _{\mathcal {V}}\) is an \(\mathcal {O}\)-simulation:

1. 1.

   Computations of \(\tau \). Assume \(M \equiv ^c_{\tau } N\) and \(|M|[\in A] \in o \in \mathcal {O}\). Then \(M~\models o[\bigvee _{V \in A} \chi _V]\) hence \(N~\models ~o[\bigvee _{V \in A} \chi _V]\) meaning \(|N|[\in \{W \,|\, \exists V \in A, V \equiv ^c_{\tau } W\}]\). So \(|M| \mathcal {O}(\equiv ^v_{\tau }) |N|\).

2. 2.

   Functions of \(\rho \rightarrow \tau \), if \(V \equiv ^v_{\rho \rightarrow \tau } W\) and \(U \in \textit{Val}(\rho )\). If \(VU~\models ~\varPhi \), then \(V~\models ~U \mapsto \varPhi \) hence \(W~\models ~U \mapsto \varPhi \) so \(WU~\models ~\varPhi \). Same vice versa, so \(VU \equiv ^c_{\tau } WU\).

So \(\equiv _{\mathcal {V}}\) is an \(\mathcal {O}\)-bisimulation. Now take any \(\mathcal {O}\)-bisimulation \(\mathcal {R}\).

1. 1.

   Computations of \(\tau \), if \(M \mathcal {R} N\) and \(M \models ~o[\phi ]\) then \(|M|[\models ~\phi ] \in o\) hence \(|N|[\in \{W \,|\, \exists V~\models ~\phi , V \mathcal {R}^v_{\tau }W\}] \in o\). By Induction Hypothesis, \((\mathcal {R}^v_{\tau }) \subseteq (\equiv ^v_{\tau })\) so \(\{W \,|\, \exists V~\models ~\phi , V \mathcal {R}^v_{\tau }W\} \subseteq \{W \,|\, \exists V~\models \phi , V \equiv ^v_{\tau } W\}\). So by upwards closure of o we get that \(|N|[\in \{W \,|\, \exists V~\models ~\phi , V \equiv ^v_{\tau } W\}] \in o\) and further that \(N~\models o[\phi ]\). We can conclude \(M \equiv _{\mathcal {V}} N\).

2. 2.

   Values of \(\rho \rightarrow \tau \), if \(V \mathcal {R} W\) and \(V~\models ~U \mapsto \varPhi \), then \(VU~\models \varPhi \) and \(VU \; \mathcal {R} \; WU\) hence by Induction Hypothesis, \(VU \equiv WU\) meaning \(WU~\models ~\varPhi \) so \(W~\models ~U \mapsto \varPhi \). If \(V~\models ~\lnot (U \mapsto \varPhi )\) then \(\lnot (VU~\models \varPhi )\) hence by \(VU \equiv WU\) we have \(\lnot (WU~\models ~\varPhi )\) so \(W \models ~\lnot (U \mapsto \varPhi )\). For the \(\bigvee \) and \(\bigwedge \) constructors, a simple Induction Step would suffice, and for higher level negation note that \(\lnot \bigvee \phi \Leftrightarrow \bigwedge \lnot \phi \) and \(\lnot \bigwedge \phi \Leftrightarrow \bigvee \lnot \phi \).

We can conclude that \((\mathcal {R}) \subseteq (\equiv _{\mathcal {V}})\), so \(\equiv _{\mathcal {V}}\) is indeed \(\mathcal {O}\)-bisimilarity.    \(\square \)

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]:

Lemma 18

If the modalities from \(\mathcal {O}\) are upwards closed, then \(\mathcal {O}(-)\) is a relator, meaning that:

1. 1.

   If \(\mathcal {R} \subseteq X \times X\) is reflexive, then so is \(\mathcal {O}(\mathcal {R})\).

2. 2.

   \(\forall \mathcal {R}, \forall \mathcal {S}, \quad \mathcal {O}(\mathcal {R}) \mathcal {O}(\mathcal {S}) \subseteq \mathcal {O}(\mathcal {R} \mathcal {S})\), where \(\mathcal {R} \mathcal {S}\) is relation composition.

3. 3.

   \(\forall \mathcal {R}, \forall \mathcal {S}, \quad \mathcal {R} \subseteq \mathcal {S} \Rightarrow \mathcal {O}(\mathcal {R}) \subseteq \mathcal {O}(\mathcal {S})\).

4. 4.

   \(\forall f: X \rightarrow Z, g: Y \rightarrow W, \mathcal {R} \subseteq Z \times W, \mathcal {O}((f \times g)^{-1}\mathcal {R}) = (Tf \times Tg)^{-1} \mathcal {O}(\mathcal {R})\)

   where \((f \times g)^{-1}(\mathcal {R}) = \{(x,y) \in X \times Y \,|\, f(x) \mathcal {R} g(y)\}\).

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

Lemma 19

If the modalities from \(\mathcal {O}\) are upwards closed, then \(\mathcal {O}(-)\) is monotone, meaning for any \(f: X \rightarrow Z\), \(g: Y \rightarrow W\), \(\mathcal {R} \subseteq X \times Y\) and \(\mathcal {S} \subseteq Z \times W\):

The relator also interacts well with the monad structure on T.

Lemma 20

If \(\mathcal {O}\) is a decomposable set of upwards closed modalities, then:

1. 1.

   \(x \mathcal {R} y~ \Rightarrow ~\eta (x) \mathcal {O}(\mathcal {R}) \eta (y)\);

2. 2.

   \(t \mathcal {O}(\mathcal {O}(\mathcal {R})) r~ \Rightarrow ~ \mu t \mathcal {O}(\mathcal {R}) \mu r\).

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

Lemma 21

If \(\mathcal {O}\) only contains Scott open modalities, then:

1. 1.

   If \(\mathcal {R}\) is reflexive, then \(t \le r \Rightarrow t \mathcal {O}(\mathcal {R}) r\).

2. 2.

   For any two sequences \(u_0 \le u_1 \le u_2 \le \dots \) and \(v_0 \le v_1 \le v_2 \le \dots \):

   \(\forall n, (u_n \mathcal {O}(\mathcal {R}) v_n) ~ \Rightarrow ~ (\sqcup _n u_n) \mathcal {O}(\mathcal {R}) (\sqcup _n v_n)\)

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.

Corollary 22

If \(\mathcal {O}\) contains only upwards closed modalities, then:

Corollary 23

If \(\mathcal {O}\) is a decomposable family of upwards closed modalities, then lifted relations are preserved by Kleisli lifting and effect operators:

1. 1.

   Given \(f: X \rightarrow Z\), \(g: Y \rightarrow W\), \(\mathcal {R} \subseteq X \times Y\) and \(\mathcal {S} \subseteq Z \times W\), if for all \(x \in X\) and \(y \in Y\) we have \(x \mathcal {R} y \Rightarrow f(x) \, \mathcal {O}(\mathcal {S}) \, g(y))\) and if \(t \mathcal {O}(\mathcal {R}) r\) then \(\mu (t[x \mapsto f(x)]) \, \mathcal {O}(\mathcal {S}) \, \mu (r[y \mapsto g(y)])\)

2. 2.

   \((\forall k, u_k \mathcal {O}(\mathcal {S}) v_k) ~ \Rightarrow ~ \sigma (u_0,u_1,\dots ) \mathcal {O}(\mathcal {S}) \sigma (v_0,v_1,\dots )\)

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].

Proposition 24

If \(\mathcal {O}\) is a decomposable set of Scott open modalities, then for any \(\mathcal {O}\)-simulation preorder \(\sqsubseteq \), the restriction of its Howe closure \(\sqsubseteq ^{\bullet }\) to closed terms is an \(\mathcal {O}\)-simulation.

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.

Theorem 3

(a). If \(\mathcal {O}\) is a decomposable set of Scott open modalities, then the open extension of the relation of \(\mathcal {O}\)-similarity is compatible.

Proof

(sketch). We write \(\sqsubseteq _{s}\) for the relation of \(\mathcal {O}\)-similarity. Since \(\sqsubseteq _{s}\) is an \(\mathcal {O}\)-simulation, we know by Proposition 24 that \(\sqsubseteq _{s}^{\bullet }\) limited to closed terms is one as well, and hence is contained in the largest \(\mathcal {O}\)-simulation \(\sqsubseteq _{s}\). Since \(\sqsubseteq _{s}^{\bullet }\) is compatible, it is contained in the open extension \(\sqsubseteq _{s}^{\circ }\). We can conclude that \(\sqsubseteq _{s}^{\circ }\) is equal to the Howe closure \(\sqsubseteq _{s}^{\bullet }\), which is compatible.    \(\square \)

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}\)).

Lemma 25

If \(\mathcal {R}^{\circ }\) is symmetric and reflexive, then \(\mathcal {R}^{\bullet *}\) is symmetric.

Theorem 3

(b). If \(\mathcal {O}\) is a decomposable set of Scott open modalities, then the open extension of the relation of \(\mathcal {O}\)-bisimilarity is compatible.

Proof

(sketch). We write \(\mathcal {O}\)-bisimilarity as \(\sqsubseteq _{b}\). From Proposition 24 we know that \(\sqsubseteq _{b}^{\bullet }\) on closed terms is an \(\mathcal {O}\)-simulation, and so we know \(\sqsubseteq _{b}^{\bullet *}\) is an \(\mathcal {O}\)-simulation as well (using Lemma 18). Since \(\sqsubseteq _{b}\) is reflexive and symmetric, we know by the previous lemma that \(\sqsubseteq _{b}^{\bullet *}\) is symmetric. Hence \(\sqsubseteq _{b}^{\bullet *}\) is an \(\mathcal {O}\)-bisimulation, implying \((\sqsubseteq _{b}^{\bullet *}) \subseteq (\sqsubseteq _{b}^{\circ })\) by compatibility of \(\sqsubseteq _{b}^{\bullet *}\). Since \((\sqsubseteq _{b}^{\circ }) \subseteq (\sqsubseteq _{b}^{\bullet }) \subseteq (\sqsubseteq _{b}^{\bullet *})\) we have that \((\sqsubseteq _{b}^{\bullet *}) = (\sqsubseteq _{b}^{\circ })\), and we can conclude that \(\sqsubseteq _{b}^{\circ }\) is compatible.    \(\square \)

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.

Definition 26

The pure behavioural logic \(\mathcal {F}\) is defined by replacing rule (2) in Fig. 2 with the alternative:

The semantics is modified by defining \(V~\models ~(\phi \mapsto \varPsi )\) using formula (2) of Sect. 3.

Proposition 27

If the open extension of \(\equiv _\mathcal {V}\) is compatible then the logics \(\mathcal {V}\) and \(\mathcal {F}\) are equi-expressive. Similarly, if the open extension of \(\sqsubseteq _{\mathcal {V}^+}\) is compatible then the positive fragments \(\mathcal {V}^+\) and \(\mathcal {F}^+\) are equi-expressive.

Proof

The definition of \((\phi \mapsto \varPsi )\) within \(\mathcal {V}\), given in (1) of Sect. 3, can be used as the basis of an inductive translation from \(\mathcal {F}\) to \(\mathcal {V}\) (and from \(\mathcal {F}^+\) to \(\mathcal {V}^+\)).

For the reverse translation, whose correctness proof is more interesting, we give a little more detail. Every value/computation formula, \(\phi \)/\(\varPhi \), of \(\mathcal {V}\) is inductively translated to a corresponding formula \(\widehat{\phi }\)/\(\widehat{\varPhi }\) of \(\mathcal {F}\). The interesting case is:

where \(\psi _V\) is a formula such that: \(V~\models _{\mathcal {F}} \psi _V\); and, for any \(\psi \), if \(V ~\models _{\mathcal {F}} \psi \) then \(\psi _V \rightarrow \psi \) (meaning that \(V'~\models _{\mathcal {F}} \psi _V\) implies \(V'~\models _{\mathcal {F}} \psi \), for all \(V'\)). Such a formula \(\psi _V\) is easily constructed as a countable conjunction (cf. Lemma 17). One then proves, by induction on types, that the \(\mathcal {F}\)-semantics of \(\widehat{\phi }\) (resp. \(\widehat{\varPhi }\)) coincides with the \(\mathcal {V}\)-semantics of \({\phi }\) (resp. \({\varPhi }\)). In the case for \(\widehat{(V \mapsto \varPhi )}\), the induction hypothesis is used to establish that any \(V'\) satisfying \(V'~\models _{\mathcal {F}} \psi _V\) enjoys the property that \(V' \equiv _{\mathcal {V}} V\). It then follows from the compatibility of \(\equiv _{\mathcal {V}}\) that \(WV' \equiv _{\mathcal {V}} WV\), for any W of appropriate type, whence \(WV' \equiv _{\mathcal {F}} WV\). The rest of the proof can easily be erected around these observations.    \(\square \)

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

Corollary 28

Suppose \(\mathcal {O}\) is a decomposable family of Scott-open modalities. Then \(\equiv _{\mathcal {F}}\) coincides with \(\equiv _{\mathcal {V}}\), and \(\sqsubseteq _{\mathcal {F}^+}\) coincides with \(\sqsubseteq _{\mathcal {V}^+}\). Hence the open extensions of \(\equiv _{\mathcal {F}}\) and \(\sqsubseteq _{\mathcal {F}^+}\) are compatible.

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.