Behavioural Equivalence via Modalities for Algebraic Effects

TL;DR

This paper develops a logic with effect-specific modalities to characterize behavioural equivalence in effectful functional programs, ensuring congruence under certain conditions for various algebraic effects.

Contribution

It introduces a general theory of modalities for behavioural equivalence, establishing conditions for their effectiveness and applicability to multiple algebraic effects.

Findings

Modalities satisfy openness and decomposability for several effects

Behavioural equivalence coincides with applicative bisimilarity under these modalities

The approach ensures congruence via a generalized Howe's method

Abstract

The paper investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability, are satisfied by the modalities then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe's method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store and input/output.

Equations

$${\alpha }^n\to \alpha \mathbf{N}\times {\alpha }^n\to \alpha {\alpha }^{\mathbf{N}}\to \alpha \mathbf{N}\times {\alpha }^{\mathbf{N}}\to \alpha .$$

$$\frac{}{\Gamma ,x:\tau ⊢x:\tau }\frac{}{\Gamma ⊢\ast :1}\frac{}{\Gamma ⊢Z:\mathbf{N}}\frac{\Gamma ⊢V:\mathbf{N}}{\Gamma ⊢S(V):\mathbf{N}}$$

$$\frac{\Gamma ⊢V:\tau }{\Gamma ⊢\text{return}(V):\tau }\frac{\Gamma ,x:\tau ⊢M:\rho }{\Gamma ⊢(\lambda x:\tau .M):\tau \to \rho }$$

$$\frac{\Gamma ⊢V:\tau \to \rho \Gamma ⊢W:\tau }{\Gamma ⊢VW:\rho }\frac{\Gamma ⊢V:(\tau \to \rho )\to (\tau \to \rho )}{\Gamma ⊢\text{fix}(V):\tau \to \rho }$$

$$\frac{\Gamma ⊢V:\mathbf{N}\Gamma ⊢M:\tau \Gamma ,x:\mathbf{N}⊢N:\tau }{\Gamma ⊢\text{ case }V\text{ of }\{Z\Rightarrow M;S(x)\Rightarrow N\}:\tau }\frac{\Gamma ⊢M:\tau \Gamma ,x:\tau ⊢N:\rho }{\Gamma ⊢\text{let }M\Rightarrow x\text{ in }N:\rho }$$

$$\frac{\sigma :{\alpha }^n\to \alpha \Gamma ⊢M_i:\tau }{\Gamma ⊢\sigma (M_0,M_1,\dots ,M_{n-1}):\tau }\frac{\sigma :{\alpha }^{\mathbf{N}}\to \alpha \Gamma ⊢V:\mathbf{N}\to \tau }{\Gamma ⊢\sigma (V):\tau }$$

$$\frac{\sigma :\mathbf{N}\times {\alpha }^n\to \alpha \Gamma ⊢V:\mathbf{N}\Gamma ⊢M_i:\tau }{\Gamma ⊢\sigma (V;M_0,M_1,\dots ,M_{n-1}):\tau }$$

$$\frac{\sigma :\mathbf{N}\times {\alpha }^{\mathbf{N}}\to \alpha \Gamma ⊢V:\mathbf{N}\Gamma ⊢W:\mathbf{N}\to \tau }{\Gamma ⊢\sigma (V;W):\tau }$$

$$(\lambda x:\tau .M)V⇝M[V/x]$$

$$\text{ case }Z\text{ of }\{Z\Rightarrow M_1;S(x)\Rightarrow M_2\}⇝M_1$$

$$\text{ case }S(V)\text{ of }\{Z\Rightarrow M_1;S(x)\Rightarrow M_2\}⇝M_2[V/x]$$

$$\text{ fix}(F)⇝\text{return }\lambda x:\tau .\text{let }F(\lambda y:\tau .\text{let fix }F\Rightarrow z\text{ in }zy)\Rightarrow w\text{ in }wx$$

$$\text{id}\{N\}=N$$

$$(S\circ (\text{let }(-)\Rightarrow x\text{ in }M))\{N\}=S\{\text{let }N\Rightarrow x\text{ in }M\}$$

$$(S,\text{let }N\Rightarrow x\text{ in }M)\rightarrowtail (S\circ (\text{let }(-)\Rightarrow x\text{ in }M),N)$$

$$(S,R)\rightarrowtail (S,R^{\prime })$$

$$(S\circ (\text{let }(-)\Rightarrow x\text{ in }M),\text{return }V)\rightarrowtail (S,M[V/x])$$

$$|S,M{|}_0$$

$$|S,M{|}_{n+1}$$

$$|-{|}_{(-)}:\text{Com}(\tau )\times \mathbb{N}\to \text{Tree}(\tau )$$

$$|M|:=\underset{n}{⨆}|M{|}_n.$$

$$V\models \varphi M\models \Phi$$

$$V\models \{n\}\iff V=\overline{n}.$$

$$W\models (V\mapsto \Phi )\iff WV\models \Phi .$$

$$(\varphi \mapsto \Psi ):=\bigwedge \{(V\mapsto \Psi )\mid V\in \text{Val}(\tau ),V\models \varphi \}$$

$$W\models (\varphi \mapsto \Psi )\iff \forall V\in \text{Val}(\tau ),V\models \varphi \text{implies}WV\models \Psi .$$

$$M\models \downarrow \varphi \iff \text{∣M∣ is a leaf V and V⊨ϕ}.$$

$$M\models {\mathsf{E}}_e\varphi \iff \text{∣M∣ is a node labelled with raisee}.$$

$$M\models ◊\varphi$$

$$M\models \square \varphi$$

$$M\models {\mathsf{P}}_{>q}\varphi$$

$${\mathsf{P}}_{>r}\varphi :=\bigvee \{{\mathsf{P}}_{>q}\varphi \mid q\in \mathbb{Q},r<q<1\}.$$

$${\mathsf{P}}_{\ge r}\varphi :=\bigwedge \{{\mathsf{P}}_{>q}\varphi \mid q\in \mathbb{Q},0\le q<r\}.$$

$$M\models (s\rightarrowtail s^{\prime })\varphi \iff$$

Full text

1 Introduction

Many tasks in software development and analysis rely on abstracting away from program syntax to an appropriate notion of program behaviour. For example, the goal of specification is to specify (constraints on) the behaviour of a program. Similarly, verification concerns validating that a program indeed exhibits the behaviour specified. Closely associated with the general concept of behaviour is the related concept of behavioural equivalence, under which two programs are deemed equivalent if they exhibit the same behaviour.

Studying the interrelated concepts of behaviour and equivalence is important from both theoretical and practical perspectives. On the theoretical side, these are fundamental notions, whose understanding sheds light not just on any particular programming language under consideration, but more generally on the question of how to mathematically model the process of computation. On the practical side, the engineering tasks of program specification, verification and synthesis all depend on having a precise mathematical model of program behaviour; and notions of program equivalence play a key role in applications, such as compiler optimisation, that involve program transformation.

For applications such as those described above to be possible, it is crucial that the mathematical notion of behaviour is appropriately chosen. For example, in the case of compiler transformations, it is essential that aspects of computational behaviour, such as execution time, that one specifically does not want preserved, are ignored. Whereas, for other applications, for example ones in which resources need to be quantified, it may be important to have a notion of behaviour in which execution time is taken into account. In general, therefore, there is no single all-encompassing approach to defining behaviour and equivalence. Nonetheless, as general desirability criteria, one would like to have definitions that are, on the one hand, mathematically natural and convenient to work with and, on the other, suitable for practical applications.

In the present paper, we explore and relate two complementary methodologies for defining notions of behaviour and equivalence, within a particular programming context: call-by-value functional programming with effects. The methodologies themselves make sense, however, within a more-or-less arbitrary programming context, so we introduce and motivate them at this greater generality.

Behavioural logic

The first methodology is to specify program behaviour via a formal logic, which we call a behavioural logic, whose formulas $\phi$ are constructed using operators that express primitive properties of program behaviour. Mathematically, one defines a satisfaction relation $M\models\phi$, expressing that program $M$ satisfies behavioural property $\phi$. The idea is that the logic should be designed in such a way that its formulas $\phi$ are capable of expressing all properties of programs that are bona fide properties of program behaviour (as opposed to, for example, properties of program syntax).

Given such a program logic, one derives a corresponding notion of behavioural equivalence. Two programs $M,N$ are said be logically equivalent if, for all formulas $\phi$, it holds that $M\models\phi$ iff $N\models\phi$; that is if they exhibit the same behaviour.

Bisimilarity

It is a remarkably general phenomenon that, in numerous computation contexts, program behaviour can be modelled as an interactive process, leading to a natural coinductive definition of program equivalence as bisimilarity: roughly speaking, the largest (equivalence) relation that relates interaction points only if their local behaviour is indistinguishable modulo the relation.

Having given such a mathematical definition of bisimilarity, one can derive an associated notion of behavioural property. Namely, a property of programs is behavioural if it respects bisimilarity; that is, whenever a program $M$ satisfies the property, then so does any bisimilar program $M^{\prime}$.

The above complementary approaches to defining behaviour and equivalence have been particularly prominent in concurrency theory. Indeed, the idea of bisimilarity as a notion of behavioural equivalence between systems was first introduced in that context, in the work of Milner and Park [26, 31]. The logical approach to defining behaviour emerged around the same time, with the characterisation, by Hennessy and Milner, of bisimilarity as the behavioural equivalence induced by an infinitary propositional modal logic, now known as Hennessy-Milner logic [9].

In the case of bisimilarity, Abramsky realised that a similar style of definition generalises to other programming contexts. In particular, he developed the notion of applicative bisimilarity for functional languages [2]. Subsequently, numerous variant notions of bisimilarity have been given across a plethora of computational contexts (for example, [43, 44, 7, 18]). To highlight one recent example, which is important for the present paper, Dal Lago, Gavazzo and Levy have provided a uniform generalisation of applicative bisimilarity to a functional programming language with effects [17].

A major goal of the present paper is to show that the logical approach to defining program behaviour can also be adapted very naturally to the context of functional programming languages with effects. In doing so, we establish that the corresponding behavioural equivalence coincides with effectful applicative bisimilarity in the style of Dal Lago et al. [17].

More precisely, we consider a typed call-by-value functional programming language with algebraic effects in the sense of Plotkin and Power [38]. 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 [27]. 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. That is, it is a call-by-value version of PCF [36], extended with effects. A very similar language is used by Plotkin and Power [38]; although, for technical convenience, we adopt an alternative (but equivalent) formulation using fine-grained call-by-value [22]. The language is defined precisely in Section 2, using an operational semantics that evaluates programs to effect trees [38, 14].

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 some given 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. For example, in the context of probabilistic computation, we have a modality $\mathsf{P}_{\!>q}$ for every rational $q\in[0,1)$, where the formula $\mathsf{P}_{\!>q}\,\phi$ is satisfied by a computation if the evaluation of the computation has a probability greater than $q$ of terminating with a return value satisfying $\phi$.

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 technical setting for this is that we have a signature $\Sigma$ 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 defines the meaning of the modality. For example, the modality $\mathsf{P}_{\!>q}$ is specified by the set of effect trees that have probability greater than $q$ of terminating if considered as a Markov chain. Several further examples and a detailed general explanation are given in Section 3.

In Section 4, we consider the relation of behavioural equivalence between programs determined by the logic. This equivalence directly relates to the notion of behaviour that is made explicit by the modalities. A fundamental well-behavedness property that any reasonable program equivalence should enjoy is that it should be a congruence with respect to the syntactic constructs of the programming language. (If an equivalence is not a congruence then there are aspects of program behaviour that are not distinguished by the equivalence but which can be separated within the programming language itself.) The major result of the paper about the logically induced behavioural equivalence is that it is indeed a congruence, as long as two conditions, openness and decomposability, hold of the collection $\mathcal{O}$ of modalities (Theorem 1). These two conditions do indeed hold for the natural sets $\mathcal{O}$ of modalities associated with the principal examples of algebraic effects.

As a second indication of the reasonableness of the logically defined behavioural equivalence, we establish that it has an alternative characterisation as an effect-sensitive version of Abramsky’s notion of applicative bisimilarity [2]. This is achieved, in Section 5, by using the modalities $\mathcal{O}$ in a logic-free context to define a relation of applicative $\mathcal{O}$-bisimilarity. The resulting equivalence relation is closely related to the effect-sensitive version of bisimilarity developed by Dal Lago et al. [17] for an untyped language with general algebraic effects. Our use of modalities as a uniform method for generating the bisimilarity relation is, however, novel. Theorem 2 shows that applicative $\mathcal{O}$-bisimilarity coincides with the logically defined relation of behavioural equivalence.

In addition to its conceptual value, establishing the coincidence of the logically defined equivalence with applicative $\mathcal{O}$-bisimilarity also serves an important technical purpose: this result is used crucially in the proof of Theorem 1. We adapt the well-known proof method of Howe [11, 12] to show that applicative $\mathcal{O}$-bisimilarity is a congruence. By the coincidence theorem, this means that the logically defined equivalence is indeed a congruence; establishing Theorem 1. Our adaptation of Howe’s method is presented in Section 6. Although the argument is technically involved, a similar adaptation of Howe’s method to a language with algebraic effects has been previously given by Dal Lago et al. [17]. Accordingly, this proof is not a main contribution of the present paper, and we give only an outline argument in the main body of the paper, with details deferred to Appendix A.

In the discussion thus far we have ignored one nuance within the development of Sections 3–6. In addition to working with the full behavioural logic, we also identify a positive fragment of the logic, which omits negation. Whereas the full logic defines an equivalence relation that coincides with applicative bisimilarity, the positive logic defines a preorder between programs that coincides with the coarser relation of applicative similarity, from which it follows that the equivalence relation determined by the positive logic coincides with mutual applicative similarity. In Section 7 we compare the above equivalence relations and preorders, and we relate them to contextual preorder and equivalence, which can also be naturally defined in terms of the set $\mathcal{O}$ of modalities. In general, applicative bisimilarity is contained in mutual applicative similarity which is contained in contextual equivalence. For some effects, however, these inclusions are strict. For example, as has been shown by Lassen [19] and Ong [30], there are examples involving nondeterminism that separate the equivalences. For the sake of completeness, we recall such separating examples in Section 7, with the novelty that we use the logical characterisations of bisimilarity and mutual similarity as a tool for proving and disproving the equivalences in question.

In cases in which the equivalences differ, there is a question of which (if any) of the equivalences should be taken as being the most fundamental. In the literature, contextual equivalence is often taken as the equivalence of choice for applicative languages. From this viewpoint, bisimilarity and mutual similarity are considered important for providing sound (but incomplete) proof methods for reasoning about contextual equivalence, which is the relation of ultimate interest. We would like to argue instead that the logical viewpoint makes a strong case for considering bisimilarity as being the primary equivalence. Every formula $\phi$ in the logic in this paper states a meaningful property of program behaviour. It is a truism that, when two programs are not bisimilar, there is some property of behaviour, expressible in the logic, that distinguishes them. If one takes the logic seriously, then the desirable property that $M\models\phi$ and $M\equiv N$ imply $N\models\phi$ holds only in the case that the equivalence relation is bisimilarity, because of its characterisation as the logically induced equivalence.

The above (almost trivial) argument of course relies on accepting arbitrary formulas $\phi$ as expressing behaviourally meaningful properties. Readers can read Section 3 and make up their own minds about this. Alternatively, one might take a more pragmatic viewpoint. Another reason for accepting a logic for expressing properties of programs is if it provides the expressivity needed to formulate proof principles for reasoning about programs. In Section 9, we show that our logic does indeed support such principles. Furthermore, they arise in the form of compositional proof rules that allow properties of a compound program to be proved by establishing appropriate properties of its constituent subprograms. In order to achieve this, we provide, in Section 8, a reformulation of our behavioural logic, which is of interest in its own right. This reformulation enjoys the property that the syntax of the logic is independent of the syntax of the programming language, which is not true of the logic of Section 3. This property is appealing, as one would like to be able to specify behaviour without knowing the syntax in which programs are written. More practically, the reformulation is used to formulate, in Section 9, the compositional proof principles referred to above. There is one significant qualification to add to this perspective. The infinitary propositional logics considered in the present paper are by no means suitable for serving as practical logics for specification and verification. Nevertheless, we view these logics as relevant to the development of more practical non-propositional but finitary logics, as they can potentially act as low-level ‘target’ logics into which high-level practical logics can be ‘compiled’. We elaborate further on this point in Section 9. However, the development of practical logics is left as a topic for future work.

Finally, in Section 10 we discuss other related and further work.

This paper is an extended and revised version of a conference paper [46], presented at the 27th European Symposium on Programming (ESOP). One principal difference from the conference version is that full proofs are included. Other extensions include: normal form results for the logic (Propositions 4.5 and 4.6); a significantly expanded presentation of the crucial decomposability properties in Section 4; explicit descriptions of the $\mathcal{O}$-relators determined by our running examples in Section 5; the comparison between bisimilarity, similarity and contextual equivalence in Section 7; and the discussion of compositional reasoning principles in Section 9.

2 A simple programming language

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 [36], extended with algebraic effects, resulting in a language similar to the one considered in Plotkin and Power [38]. In order to simplify the technical treatment of the language, we present it in the style of fine-grained call-by-value [22]. This means that we make a syntactic distinction between values and computations, separating the static and dynamic aspects of the language respectively. Furthermore, all sequencing of computations is performed using a single language construct, the 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 $\bf{1}$.

Types: $\tau,\rho::=~{}\bf{1}\mid\mathbf{N}\mid\rho\rightarrow\tau$

Contexts: $\Gamma::=~{}\emptyset\mid\Gamma,\,x:\tau$

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

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

Values: $V,W::=~{}*\mid Z\mid S(V)\mid\lambda x:\tau.M\mid x$

Computations: $M,N::=VW\mid\textbf{return }V\mid\textbf{let }M\Rightarrow x\textbf{ in }N\mid\textbf{fix}(V)$

$\hskip 85.35826pt\mid\textbf{case }V\textbf{ 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 types 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 let construct for sequencing; a fix construct for recursive definition333By defining $\textbf{fix}\,V$ to be a computation which reduces to a lambda term, it holds that the only values of function types are lambda terms.; and a case construct that branches according to whether its natural-number argument is zero or positive. The computation ‘$\textbf{let }M\Rightarrow x\textbf{ 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 then returned as the result of the **let ** computation.

To the pure functional language described above, we add effect operations. The collection of effect operations is specified by a set $\Sigma$ (the signature) of such operations, together with, for each $\sigma\in\Sigma$ an associated arity which takes one of the four forms below444These four forms of arity suffice for the examples we consider. Similar choices were made in [14, 37]. Going beyond such discrete arities is an interesting direction for future research; see Section 10.

[TABLE]

The notation here is chosen to be suggestive of the way in which such arities are used in the typing rules of Fig. 1, 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.

Computations:  $M,N::=\dots\mid\sigma(M_{0},M_{1},\dots,M_{n-1})\mid\sigma(V;M_{0},M_{1},\dots,M_{n-1})\mid\sigma(V)\mid\sigma(W;V)$

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

The typing rules for the language are given in Figure 1. Note that the choice of typing rule for an effect operation $\sigma\in\Sigma$ 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)$. Thus $\textit{Val}(\mathbf{N})=\{\overline{n}\,|\,n\in\mathbb{N}\}$.

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

Example 0** (Pure functional computation).**

This is the trivial case (from an effect point of view) in which the signature $\Sigma$ of effect operations is empty. The resulting language is a fine-grained call-by-value variant of PCF [36].

Example 1** (Error).**

We take a set of error labels $E$. For each $e\in E$ there is an effect operation $\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 operation $\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 operation $\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 operations, $\textit{read}:\alpha^{\mathbf{N}}\to\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 with 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 $\Sigma$, and with values and $\bot$ (nontermination) as the generators. This idea appears in Plotkin and Power [38], and our technical treatment follows the approach of Johann et al. [14], adapted to (fine-grained) 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 let at the top level.

[TABLE]

The behaviour of let is implemented using a system of stacks where:

Stacks: $S::=~{}\textit{id}\mid S\circ(\textbf{let }(-)\Rightarrow x\textbf{ in }M)$

We write $S\{N\}$ for the computation term obtained by ‘applying’ the stack $S$ to $N$, defined by:

[TABLE]

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:

[TABLE]

We define the notion of effect tree for an arbitrary set $X$, where $X$ is thought of as a set of abstract ‘values’.

Definition 2.1**.**

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

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\Sigma$ has arity $\alpha^{n}\rightarrow\alpha$. 4. 4.

A node labelled $\sigma$ with children $(t_{i})_{i\in\mathbb{N}}$, when $\sigma\in\Sigma$ 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\Sigma$ has arity $\mathbf{N}\times\alpha^{n}\rightarrow\alpha$. 6. 6.

A node labelled $\sigma_{m}$ where $m\in\mathbb{N}$ with children $(t_{i})_{i\in\mathbb{N}}$, when $\sigma\in\Sigma$ has arity $\mathbf{N}\times\alpha^{\mathbf{N}}\rightarrow\alpha$.

See Examples 2 and 4 later on in this section for examples of effect trees.

We write $TX$ for the set of trees over $X$. We define a partial ordering on $TX$ where $t_{1}\leq t_{2}$, if $t_{1}$ can be obtained by pruning $t_{2}$ by removing a possibly infinite number of subtrees of $t_{2}$ and putting leaf nodes labelled $\bot$ in their place. This forms an $\omega$-complete partial order, meaning that every ascending sequence $t_{1}\leq t_{2}\leq\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 such trees of values.

Given $f:X\to Y$ and a tree $t\in TX$, we write $t[x\mapsto f(x)]\in TY$ or $Tf(t)\in TY$ for the tree whose leaves $x\in X$ are renamed to $f(x)$. We have a function $\mu:TTX\to TX$, which takes a tree $r$ of trees and flattens it to a tree $\mu r\in TX$, by taking the tree labelling each non-$\bot$ leaf of $r$ to be the subtree rooted 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 the leaf labelled $x$ qua tree.

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 id, until the evaluation process (which is deterministic) terminates. If termination never happens the tree is $\bot$. If the evaluation process terminates at a configuration of the form $(\textit{id},\textbf{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\Sigma$. 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:

[TABLE]

It follows that $|S,M|_{n}\leq|S,M|_{n+1}$ in the given ordering on trees. We write

[TABLE]

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

[TABLE]

We illustrate the above definitions with a couple of examples of effect computations and their corresponding effect trees.

Example 2** (Nondeterminism).**

Nondeterministically generate a natural number:

$?N:=\textbf{let }\textbf{fix}(\lambda x:\mathbf{1}\to\mathbf{N}.\,\textit{or}(\lambda y:\mathbf{1}.\,Z\,,\,\lambda y:\mathbf{1}.\,\textbf{let }xy\Rightarrow z\textbf{ in }S(z)))\Rightarrow w\textbf{ in }w*$

or$\textstyle{\overline{0}}$or\textstyle{|?N|=}$$\textstyle{\overline{1}}or$\textstyle{\overline{2}}$

Example 4** (Global store).**

Save and load a value, returning its successor:

$V:=\lambda y:\mathbf{N}.\textit{update}_{l}(y;\textit{lookup}_{l}(\lambda x:\mathbf{N}.\,\textbf{return}(S(x))))\quad:\quad\mathbf{N}$ $\rightarrow\mathbf{N}$

\textstyle{\textit{update}_{l}(1)}$$\textstyle{|V\overline{1}|=}$$\textstyle{\textit{lookup}_{l}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\overline{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{0}$$\textstyle{\quad\overline{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1}$$\textstyle{\overline{3}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{2}$$\textstyle{\dots}$$\textstyle{\overline{n+1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{n}

In the second example above, we see that the resulting tree exhibits redundancies with respect to the expected model of computation with global store. Since the $\textit{update}_{l}$ operation sets the value of location $l$ to $1$, the ensuing $\textit{lookup}_{l}$ operation will retrieve the value $1$, and so execution will proceed down the branch labelled $1$ resulting in the return value $2$. The other infinitely many leaves of the tree are redundant. The issue here is that the operational semantics of the language has been defined independently of any implementation model for the effect operations. An effect tree provides a normal form that records in its nodes all effect operations that may potentially be performed during execution, and the dependencies between them. But nothing is stated about which effect operations will actually be performed in practice, and what effect they have if invoked. It is precisely this lack of specificity that allows the operational semantics to be defined in a uniform way depending only on the signature of effect operations and their arities.

In order to be able to reason about programs with effects (for example, to establish properties of or equivalences between them), it is necessary to supply the missing information about how effect operations behave when executed. As motivated in the introduction, we now proceed to do this by introducing a behavioural logic for expressing behavioural properties of our language.

3 Behavioural logic and modalities

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 $\Phi,\Psi,\dots$ for the latter. Our logic will thus have two satisfaction relations

[TABLE]

which respectively assert that “value $V$ enjoys the value property expressed by $\phi$” and “computation $M$ enjoys the computation property expressed by $\Phi$”.

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.555We call such formulas basic rather than atomic because they include formulas such as $(V\mapsto\Phi)$, discussed below, which are built from other formulas. 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:

[TABLE]

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\}$, every value formula corresponds to a subset of $\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\to\rho$, we want each basic formula to express a fundamental behavioural constraint on values (i.e., $\lambda$-abstractions) $W$ of type $\tau\to\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 $\Phi\in\textit{CF}\,(\rho)$, we include a basic value formula $(V\mapsto\Phi)\in\textit{VF}\,(\tau\to\rho)$ with the semantics:

[TABLE]

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 $\Psi\in\textit{CF}\,(\rho)$, the definition

[TABLE]

defines a formula whose derived semantics is

[TABLE]

In Section 8, we shall consider the possibility of changing the basic value formulas in $\textit{VF}\,(\tau\to\rho)$ to formulas $(\phi\mapsto\Psi)$.

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:

[TABLE]

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

[TABLE]

(Because $\textit{raise}_{e}$ is an operation of arity [math], a $\textit{raise}_{e}$ node in a tree has [math] 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 [math]-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 [math]-argument modalities subsumed as unary modalities with a redundant argument.

Example 2** (Nondeterminism).**

Define $\mathcal{O}=\{\Diamond,\,\Box\}$ with:

[TABLE]

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\leq q<1\}$ with:

[TABLE]

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\leq r<1$, we can define:

[TABLE]

Similarly, we can define non-strict threshold modalities, for $0<r\leq 1$, by:

[TABLE]

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

Given the set of locations $L$, we define the set of states by $\textit{State}:=\mathbb{N}^{L}$. The modalities are $\mathcal{O}=\{(s\rightarrowtail s^{\prime})\mid s,s^{\prime}\in\textit{State}\}$, where informally:

[TABLE]

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

[TABLE]

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

[TABLE]

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 s^{\prime})$ modality formally:

[TABLE]

In Section 9, we show an example of how to encode Hoare Logic in the above logic.

Example 5** (Input/output).**

Define an i/o-trace to be a word $w$ over the alphabet

[TABLE]

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

[TABLE]

The intuitive semantics of these modalities is as follows.

[TABLE]

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.

[TABLE]

The formal semantics of modalities is now easily defined by:

[TABLE]

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 a signature $\Sigma$ of effect operations, as in Section 2. We also assume a given 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$.

Definition 3.1** (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

[TABLE]

That is, every modality $o\in\mathcal{O}$ is mapped to a subset $\llbracket o\rrbracket\subseteq T\bf{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 now 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, where for the basic formulas we have:

[TABLE]

and for the other formulas we have:

[TABLE]

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.

The lemma below is standard. It states that every formula in infinitary propositional logic can be written in infinitary disjunctive normal form. (It can also be written in infinitary conjunctive normal form.)

Lemma 3.2**.**

Each formula $\phi\in\mathcal{V}$ (value or computation) is equivalent to a formula of the form $\bigvee_{I}\bigwedge_{J}\psi$ where for each $i\in I$ and $j\in J_{i}$ the formula $\psi_{i,j}$ is either a basic formula or the negation of a basic formula.

We omit the proof, which is both routine and standard.

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

Example 0** (Pure functional computation).**

We have $\mathcal{O}=\{{\downarrow}\}$. Define:

[TABLE]

Example 1** (Error).**

We have $\mathcal{O}=\{{\downarrow}\}\cup\{\mathsf{E}_{e}\mid e\in E\}$. Define:

[TABLE]

Example 2** (Nondeterminism).**

We have $\mathcal{O}=\{\Diamond,\,\Box\}$. Define:

[TABLE]

Example 3** (Probabilistic choice).**

$\mathcal{O}=\{\mathsf{P}_{>q}\mid q\in\mathbb{Q},\,0\leq q<1\}$. Define:

[TABLE]

Example 4** (Global store).**

$\mathcal{O}=\{(s\rightarrowtail s^{\prime})\mid s,s^{\prime}\in\textit{State}\}$. Define:

[TABLE]

Example 5** (Input/output).**

\mathcal{O}=\{{\langle w\rangle\!\!\downarrow},\,\langle w\rangle_{\!\dots}\mid\text{w an i/o-trace}\}. Define:

[TABLE]

In this section we have defined our logic expressing behavioural properties. We next proceed to derive the induced notion of behavioural equivalence between programs, as motivated in Section 1.

4 Behavioural equivalence

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 Section 3 is a congruence. In addition, we shall obtain a similar result for a coarser behavioural preorder determined by a natural positive fragment of $\mathcal{V}$, which we call $\mathcal{V}^{+}$. In addition to being natural in its own right, the preorder induced by the positive fragment $\mathcal{V}^{+}$ turns out to be an indispensable technical tool for establishing properties of the behavioural equivalence induced by the full logic $\mathcal{V}$.

Definition 4.1** (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. It is inductively defined using rules 1-5, 7 and 8 from Fig. 2.

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.2** (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:

[TABLE]

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, 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}^{+}}$). Since $\mathcal{V}^{+}$ is a subset of $\mathcal{V}$, it is apparent that $\equiv_{\mathcal{V}}$ is finer than $\equiv_{\mathcal{V}^{+}}$, as it considers more behavioural properties which could distinguish terms. For the same reason, it holds that $\sqsubseteq_{\mathcal{V}}\,\subseteq\,\,\sqsubseteq_{\mathcal{V}^{+}}$.

Before formulating the required notions to prove congruence of the behavioural equivalences, we shall make some observations about the preorders and discuss a possible simplification of the logic (Proposition 4.5).

Lemma 4.3**.**

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:

[TABLE]

Lemma 4.4**.**

For any $M_{0},M_{1}\in\textit{Com}(\tau)$, we have $M_{0}\sqsubseteq_{\mathcal{V}^{+}}M_{1}$ if and only if:

[TABLE]

Both these lemmas are a consequence of the fact that satisfaction of conjunctions and disjunctions are completely determined by satisfaction of the formulas over which the connectives are taken. As such, the logical preorder is completely determined by satisfaction of basic formulas. Similar characterisations, but replacing ‘implies’ and $\mathcal{V}^{+}$ with ‘if and only if’ and $\mathcal{V}$ respectively, hold for the behavioural equivalence $\equiv_{\mathcal{V}}$.

Proposition 4.5**.**

Let  $\mathcal{K}$ be the fragment of  $\mathcal{V}$ inductively defined by rules 1 to 6 from Fig. 2 (so computation formulas are not closed under propositional connectives), then the induced logical equivalence $\equiv_{\mathcal{K}}$ is the same as $\equiv_{\mathcal{V}}$.

Proof.

We prove that any value formula $\phi\in\mathcal{V}$ is equivalent to a value formula $\phi^{\prime}$ from $\mathcal{K}$. We do this by induction on types. For value formulas of natural numbers type, note that $\textit{VF}_{\mathcal{V}}(\mathbf{N})=\textit{VF}_{\mathcal{K}}(\mathbf{N})$, so the statement is trivially true by taking $\phi^{\prime}:=\phi$.

For value formulas of function type, assume $\phi$ is a basic formula $V\mapsto\Phi$, where by Lemma 3.2 we may assume w.l.o.g. that $\Phi$ is a disjunction over conjunctions over formulas $\Psi$ of the form $o\,\psi$ or $\neg o\,\psi$. We can now use the equivalences $(V\mapsto\bigvee_{I}\bigwedge_{J}\Psi)\equiv\bigvee_{I}\bigwedge_{J}(V\mapsto\Psi)$ and $(V\mapsto\neg o\,\psi)\equiv\neg(V\mapsto o\,\psi)$ to construct a formula $\phi^{\prime}\in\mathcal{K}$ equivalent to $\phi$, using the induction hypothesis to replace each occurrence of $o\,\psi$ with $o\,\psi^{\prime}$ where $\psi^{\prime}\in\mathcal{K}$ is equivalent to $\psi$. In the case that $\phi$ is not a basic formula, we can do an induction on its structure to find the desired $\phi^{\prime}$, where $(\bigvee_{I}\psi)^{\prime}:=\bigvee_{I}\psi^{\prime}$, $(\bigwedge_{I}\psi)^{\prime}:=\bigwedge_{I}\psi^{\prime}$, $(\neg\psi)^{\prime}:=\neg(\psi^{\prime})$, and basic formulas are handled as above.

So every value formula has an equivalent value formula in $\mathcal{K}$, so the logical preorder on value terms remains unchanged. To see that the logical equivalence on computation terms remains unchanged, simply use Lemma 4.4. ∎

Altering the proof slightly, we can derive a similar result for the positive logic.

Proposition 4.6**.**

Let  $\mathcal{K}^{+}$ be the fragment of  $\mathcal{V}^{+}$ defined by rules 1 to 5 from Fig. 2 (so computation formulas are not closed under propositional connectives), then the induced logical preorder  $\sqsubseteq_{\mathcal{K}^{+}}$ is the same as  $\sqsubseteq_{\mathcal{V}^{+}}$.

We next formulate the appropriate technical notion of (pre)congruence666A precongruence is a preorder enjoying the properties of a congruence relation apart from symmetry. 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 $\Gamma\vdash M\,\mathcal{R}^{\circ}N:\tau$ precisely when, for every well-typed vector of closed values $\overrightarrow{V}:\Gamma$, 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., Lassen and Pitts [19, 35] for further explanation.

Definition 4.7** (Compatibility).**

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

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}$, which can be divided into two properties.

Definition 4.8**.**

We say that $o\in\mathcal{O}$ is upwards closed if $\llbracket o\rrbracket$ is an upwards closed subset of $T\mathbf{1}$; i.e., if $t\in\llbracket o\rrbracket$ implies $t^{\prime}\in\llbracket o\rrbracket$ whenever $t\leq t^{\prime}$.

Definition 4.9**.**

The modality $o\in\mathcal{O}$ is Scott-open if $\llbracket o\rrbracket$ is an open set in the Scott topology on $T\mathbf{1}$; i.e., $\llbracket o\rrbracket$ is upwards closed and, whenever $t_{1}\leq t_{2}\leq\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$.

We now turn to the decomposability condition in Theorem 1, which will eventually be given in Definition 4.15 below, following the introduction of certain auxiliary relations that are required for the definition. Because the formulation is unavoidably technical, we first give some motivation for where we are heading.

The main purpose of the decomposability property is to enable us to prove that the positive behavioural preorder is preserved by the let term constructor. (This motivation will eventually manifest itself in case 5 in the proof of Lemma 6.4 in Appendix A.) The particular technical challenge presented by let is that it sequences effects. Semantically, the operation of effect sequencing is distilled into the monad multiplication map $\mu:TTX\to TX$ defined in Section 2. Accordingly, we formulate the required notion of decomposability as a property of $\mu$. It turns out that we need only consider $\mu$ in the case that $X$ is the singleton set $\{\ast\}$. Thus decomposability will involve trees of unit type, that is trees in $T\mathbf{1}$, as well as double trees, that is trees in $TT\mathbf{1}$. We shall define it as the property that the monad multiplication $\mu$ is order-preserving with respect to preorders $\curlyeqprec$ and $\preccurlyeq$ defined on double and single trees respectively.

The relation $\preccurlyeq$ on $T\mathbf{1}$ is a natural extension of the positive behavioural preorder $\sqsubseteq_{\mathcal{V}^{+}}$, at unit type, from a relation on computation terms to a relation $\preccurlyeq$ on arbitrary effect trees. To accommodate this perspective, we introduce a new notation, allowing us to apply a modality $o$ to an arbitrary subset of a set $X$ of values: for $A\subseteq X$ and $o\in\mathcal{O}$ we define

[TABLE]

We will often write $o(A)$ instead of $o_{X}(A)$ when $X$ is clear from the context. For instance, if $t\in TX$ then $t\in o(A)$ means $t\in o_{X}(A)$. One case of particular interest is when $A=X=\{\ast\}$, for which we note that $o(\{\ast\})=\llbracket o\rrbracket$. Using the extended interpretation of modalities, we similarly extend the satisfaction relation of type $\mathbf{1}$ positive computation formulas, from computation terms of type $\mathbf{1}$ to arbitrary $T\mathbf{1}$ computation trees.777In general, there are uncountably many trees, whereas there are only countably many computation terms. For each $\Phi\in\textit{CF}_{\mathcal{V}^{+}}\,(\mathbf{1})$, we define its denotation $\llbracket\Phi\rrbracket\subseteq T\mathbf{1}$ over unit type trees inductively, according to the following rules:888For a set $X$ of formulas, we denote $\bigvee X$ and $\bigwedge X$ for respectively the disjunction and conjunction over X.

[TABLE]

The above definition can be seen as an extension of the satisfaction relation on unit type computation terms, since for any computation term $M:\mathbf{1}$ and formula $\Phi\in\textit{CF}_{\mathcal{V}^{+}}(\mathbf{1})$ it holds that $M\models\Phi\Leftrightarrow|M|\in\llbracket\Phi\rrbracket$.

We can now define the required preorder between arbitrary trees of type $\mathbf{1}$.

Definition 4.10**.**

We define the preorder $\preccurlyeq$ on $T\mathbf{1}$ by:  for any two trees $t,t^{\prime}\in T\mathbf{1}$,

[TABLE]

It is immediate that $\preccurlyeq$ is a conservative extension of the positive behavioural preorder on computation terms of type $\mathbf{1}$ in the following sense:

Proposition 4.11**.**

For any $M,N\in\textit{Com}(\mathbf{1})$, it holds that $|M|\preccurlyeq|N|$ if and only if $M\sqsubseteq_{\mathcal{V}^{+}}N$.

We give some alternative characterisations of $\preccurlyeq$.

Proposition 4.12**.**

For any $t,t^{\prime}\in T\mathbf{1}$, the following three statements are equivalent:

$t\preccurlyeq t^{\prime}$. 2. 2.

$(t\preccurlyeq t^{\prime})\wedge(t[\in\emptyset]\preccurlyeq t^{\prime}[\in\emptyset])$. 3. 3.

$\forall o\in\mathcal{O},~{}(t\in o(\{\ast\})\Rightarrow t^{\prime}\in o(\{\ast\}))\,\wedge\,(t\in o(\emptyset)\Rightarrow t^{\prime}\in o(\emptyset))$.

Proof.

The equivalence (1) $\Leftrightarrow$ (3) follows from a straightforward induction on the structure of positive unit type computation formulas. Using the previous equivalence, the equivalence (1) $\Leftrightarrow$ (2) follows from the fact that $t[\in\emptyset]\in o(\{\ast\})\Leftrightarrow t\in o(\emptyset)$. ∎

In the examples given in this paper, the preorder can be characterised in a simpler way, where

[TABLE]

This is a consequence of the fact that each modality $o$ given in the examples satisfy one of the two following properties:

• (i)

$\forall t\in T\mathbf{1},t\notin o(\emptyset)$. The modalities with this property are: $\downarrow,\Diamond,\Box,\mathsf{P}_{>q},(s\rightarrowtail s^{\prime}),$ and $\langle w\rangle\!\downarrow$.

• (ii)

$\forall t\in T\mathbf{1},t\in o(\{\ast\})\Leftrightarrow t\in o(\emptyset)$. The modalities with this property are $\mathsf{E}_{e}$ and $\langle w\rangle_{\dots}$.

There do however exist sets of Scott open modalities for which the characterisation of $\preccurlyeq$ via (3) does not hold. For example, for $\Sigma=\{\textit{raise}:\alpha^{0}\rightarrow\alpha\}$ and $\mathcal{O}=\{o\}$ where $\llbracket o\rrbracket=\{\ast,\textit{raise}\}$.

We next define the relation $\curlyeqprec$ on double trees $TT\mathbf{1}$.

Definition 4.13**.**

We define the preorder $\curlyeqprec$ on $TT\mathbf{1}$ by:  for any two double trees $r,r^{\prime}\in TT\mathbf{1}$,

[TABLE]

We give some characterisations of $\curlyeqprec$. These use the notion of right-set, that is; for any relation $\mathcal{R}\subseteq X\times Y$ and subset $A\subseteq X$, we write ${{\mathcal{R}}^{\uparrow}A}:=\{y\in Y\,|\,\exists x\in A,x\,\mathcal{R}\,y\}$ for the right-set of $A$ under the relation $\mathcal{R}$.

Lemma 4.14**.**

If $\mathcal{O}$ is a set of upwards-closed modalities, then for all $r,r^{\prime}\in TT\mathbf{1}$, the following are equivalent:

$r\curlyeqprec\,r^{\prime}$. 2. 2.

$\forall A\subseteq T\mathbf{1},~{}r[{\in A}]\preccurlyeq r^{\prime}[{\in({{\preccurlyeq}^{\uparrow}A})}]$. 3. 3.

$\forall o\in\mathcal{O},\forall A\subseteq T\mathbf{1},~{}r\in o(A)\Rightarrow r^{\prime}\in o({{\preccurlyeq}^{\uparrow}A})$.

Proof.

(1) $\Rightarrow$ (2)   Let $r[{\in A}]\in o(\{\ast\})$, then since $A\subseteq({{\preccurlyeq}^{\uparrow}A})$ and $o$ is upwards closed, $r[{\in({{\preccurlyeq}^{\uparrow}A})}]\in o(\{\ast\})$, which means $r\in o({{\preccurlyeq}^{\uparrow}A})$. Let $\Phi_{A}:=\bigvee_{t\in A}((\bigwedge_{o\in\mathcal{O},t\in o(\{\ast\})}o(\top))\wedge(\bigwedge_{o\in\mathcal{O},t\in o(\emptyset)}o(\bot)))$, then $\llbracket\Phi_{A}\rrbracket=({{\preccurlyeq}^{\uparrow}A})$ as $\Phi_{A}$ perfectly replicates the condition of membership in ${{\preccurlyeq}^{\uparrow}A}$. So by (1) it holds that $r^{\prime}\in o({{\preccurlyeq}^{\uparrow}A})$, hence $r^{\prime}[{\in({{\preccurlyeq}^{\uparrow}A})}]\in o(\{\ast\})$. If $r[{\in A}]\in o(\emptyset)$, then $r\in o(\emptyset)$ hence $r^{\prime}\in o(\emptyset)$ (since $(\bigvee\emptyset)\in\textit{CF}_{\mathcal{V}^{+}}\,(\mathbf{1})$ and $\llbracket\bigvee\emptyset\rrbracket=\emptyset$), so $r^{\prime}[{\in({{\preccurlyeq}^{\uparrow}A})}]\in o(\emptyset)$. We can conclude that $r[{\in A}]\preccurlyeq r^{\prime}[{\in({{\preccurlyeq}^{\uparrow}A})}]$.

(2) $\Rightarrow$ (3)   If $r[{\in A}]\preccurlyeq r^{\prime}[{\in({{\preccurlyeq}^{\uparrow}A})}]$, then for any $o\in\mathcal{O}$ it holds that $r[{\in A}]\in o(\{\ast\})\Rightarrow r^{\prime}[{\in{{\preccurlyeq}^{\uparrow}A}}]\in o(\{\ast\})$, which is identical to the statement $r\in o(A)\Rightarrow r^{\prime}\in o({{\preccurlyeq}^{\uparrow}A})$.

(3) $\Rightarrow$ (1)   If $r\in o(\llbracket\Phi\rrbracket)$ with $\Phi\in\textit{CF}_{\mathcal{V}^{+}}\,(\mathbf{1})$, then by (3) it holds that $r^{\prime}\in o({{\preccurlyeq}^{\uparrow}\llbracket\Phi\rrbracket})$. By the definition of $\preccurlyeq$ it holds that $({{\preccurlyeq}^{\uparrow}\llbracket\Phi\rrbracket})\subseteq\llbracket\Phi\rrbracket$, and since $\preccurlyeq$ is reflexive $\llbracket\Phi\rrbracket\subseteq({{\preccurlyeq}^{\uparrow}\llbracket\Phi\rrbracket})$. Hence $({{\preccurlyeq}^{\uparrow}\llbracket\Phi\rrbracket})=\llbracket\Phi\rrbracket$ and we conclude that $r^{\prime}\in o(\llbracket\Phi\rrbracket)$. ∎

We can now finally define the promised notion of decomposability.

Definition 4.15** (Decomposability).**

We say that $\mathcal{O}$ is decomposable if, for all double trees $r,r^{\prime}\in TT\mathbf{1}$, $r\curlyeqprec\,r^{\prime}$ implies $\mu r\preccurlyeq\mu r^{\prime}$.

Since decomposability is such a technical notion, we give two lemmas providing alternative characterisations of it. The first gives a reformulation that is immediate in the case of our examples, where the statement $t\preccurlyeq t^{\prime}$ can be simplified via (3). The general case, however, requires a rather technical proof.

Lemma 4.16**.**

A set of upwards-closed modalities $\mathcal{O}$ is decomposable if and only if for all $r,r^{\prime}\in TT\mathbf{1}$, if $r\curlyeqprec\,r^{\prime}$, then  $\forall o\in\mathcal{O},~{}\mu r\in o(\{\ast\})\Rightarrow\mu r^{\prime}\in o(\{\ast\})$.

Proof.

We use the equivalences from Proposition 4.12.

($\Rightarrow$)   The result follows by observing that $\mu r\preccurlyeq\mu r^{\prime}$ implies $\forall o\in\mathcal{O},~{}\mu r\in o(\{\ast\})\Rightarrow{\mu r^{\prime}\in o(\{\ast\})}$.

($\Leftarrow$)   Assume:   (I) $\forall r,r^{\prime}\in TT\mathbf{1},~{}r\curlyeqprec\,r^{\prime}~{}\Rightarrow~{}(\forall o\in\mathcal{O},~{}\mu r\in o(\{\ast\})\Rightarrow\mu r^{\prime}\in o(\{\ast\}))$.

Take some $r,r^{\prime}\in TT\mathbf{1}$, and suppose that $r\curlyeqprec\,r^{\prime}$, hence with Lemma 4.14 it holds that:

(II) $\forall o\in\mathcal{O},A\subseteq T\mathbf{1},~{}r\in o(A)\Rightarrow r^{\prime}\in o({{\preccurlyeq}^{\uparrow}A})$.

We need to prove that $\mu r\preccurlyeq\mu r^{\prime}$. By (I) we derive that $\forall o\in\mathcal{O},~{}\mu r\in o(\{\ast\})\Rightarrow\mu r^{\prime}\in o(\{\ast\})$. To prove $\mu r\preccurlyeq\mu r^{\prime}$ we need only prove $\forall o\in\mathcal{O},~{}\mu r\in o(\emptyset)\Rightarrow\mu r^{\prime}\in o(\emptyset)$.

Assume $\mu r\in o^{\prime}(\emptyset)$ for $o^{\prime}\in\mathcal{O}$, then $\mu(r[t\mapsto t[{\in\emptyset}]])=(\mu r)[{\in\emptyset}]\in o^{\prime}(\{\ast\})$. We prove that ${r[t\mapsto t[{\in\emptyset}]]}\curlyeqprec~{}r^{\prime}[t^{\prime}\mapsto t^{\prime}[{\in\emptyset}]]$. Suppose for some $o\in\mathcal{O}$ and $A\subseteq T\mathbf{1}$, it holds that ${r[t\mapsto t[{\in\emptyset}]]}\in o(A)$. Let $B:=\{t\in T\mathbf{1}\mid t[{\in\emptyset}]\in A\}$, then $r\in o(B)$. By (II) it holds that $r^{\prime}\in o({{\preccurlyeq}^{\uparrow}B})$.

For $t^{\prime}\in\,({{\preccurlyeq}^{\uparrow}B})$, there is a $t\in B$ such that $t\preccurlyeq t^{\prime}$. Since $t\in B$, $t[{\in\emptyset}]\in A$ and hence $t^{\prime}[{\in\emptyset}]\in({{\preccurlyeq}^{\uparrow}A})$. So $({{\preccurlyeq}^{\uparrow}B})\subseteq\{t^{\prime}\in T\mathbf{1}\mid t^{\prime}[{\in\emptyset}]\in({{\preccurlyeq}^{\uparrow}A})\}$, and we can use upwards closure of $o^{\prime}$ to derive ${r^{\prime}[t^{\prime}\mapsto t^{\prime}[{\in\emptyset}]]}\in o({{\preccurlyeq}^{\uparrow}A})$. Hence by Lemma 4.14, $r[t\mapsto t[{\in\emptyset}]]\curlyeqprec\,r^{\prime}[t^{\prime}\mapsto t^{\prime}[{\in\emptyset}]]$.

We can apply (I) to derive $\mu(r[t\mapsto t[{\in\emptyset}]])\preccurlyeq\mu(r^{\prime}[t^{\prime}\mapsto t^{\prime}[{\in\emptyset}]])$. So since $\mu(r[t\mapsto t[{\in\emptyset}]])=(\mu r)[{\in\emptyset}]\in o^{\prime}(\{\ast\})$, it holds that and $\mu(r^{\prime}[t^{\prime}\mapsto t^{\prime}[{\in\emptyset}]])\in o^{\prime}(\{\ast\})$ and hence $\mu r^{\prime}\in o^{\prime}(\emptyset)$. We conclude that $\mu r\preccurlyeq\mu r^{\prime}$, so we are finished. ∎

The second reformulation of decomposability shows that it is equivalent to being able to ‘decompose’ statements of the form $\mu r\in o(\{\ast\})$ into a collection of modal properties of $r$.

Lemma 4.17**.**

A set of upwards-closed modalities $\mathcal{O}$ is decomposable if and only if for any $r\in TT\mathbf{1}$ and $o\in\mathcal{O}$ such that $\mu r\in o(\{\ast\})$, there is a collection of pairs $\{(o_{i},\Phi_{i})\}_{i\in I}$, with each $o_{i}\in\mathcal{O}$ and $\Phi_{i}\in\textit{CF}_{\mathcal{V}^{+}}\,(\mathbf{1})$, satisfying the following two properties:

$\forall i\in I,~{}r\in o_{i}(\llbracket\Phi_{i}\rrbracket)$. 2. 2.

$\forall r^{\prime}\in TT\mathbf{1},~{}(\forall i\in I,~{}r^{\prime}\in o_{i}(\llbracket\Phi_{i}\rrbracket))~{}\Rightarrow~{}\mu r^{\prime}\in o(\{\ast\})$.

Proof.

We use the equivalent statement for decomposability established in Lemma 4.16.

($\Rightarrow$) Assume decomposability, and that for some $r\in TT\mathbf{1}$ and $o\in\mathcal{O}$, it holds that $\mu r\in o(\{\ast\})$. For any $A\subseteq TT\mathbf{1}$ such that $r\in A$, choose a pair $(o^{\prime}_{A},\Phi^{\prime}_{A})$ where $o^{\prime}_{A}\in\mathcal{O}$ and $\Phi^{\prime}_{A}\in\textit{CF}_{\mathcal{V}^{+}}\,(\mathbf{1})$ such that $o^{\prime}_{A}(\llbracket\Phi^{\prime}_{A}\rrbracket)=A$, if such a pair exists. All these chosen pairs together form our desired collection. Since for any such $A$, $r\in A=o^{\prime}_{A}(\llbracket\Phi^{\prime}_{A}\rrbracket)$, this collection satisfies condition (1). For any $r^{\prime}\in TT\mathbf{1}$, if $r^{\prime}\in o^{\prime}_{A}(\llbracket\Phi^{\prime}_{A}\rrbracket)=A$ for any pair in the collection, then for any $r\in A\subseteq TT\mathbf{1}$ for which there is a pair $o^{\prime\prime},\Phi^{\prime\prime}$ such that $o^{\prime\prime}(\llbracket\Phi^{\prime\prime}\rrbracket)=A$, it holds that $r^{\prime}\in A$. So $r\curlyeqprec\,r^{\prime}$. Hence by decomposability, $\forall o^{\prime\prime}\in\mathcal{O},\mu r\in o^{\prime\prime}(\{\ast\})\Rightarrow\mu r^{\prime}\in o^{\prime\prime}(\{\ast\})$, so in particular $r^{\prime}\in o(\{\ast\})$, and thus condition (2) holds.

($\Leftarrow$) Assume the statement given in the lemma, we need to prove decomposability. For some $r,r^{\prime}\in TT\mathbf{1}$, suppose that $r\curlyeqprec\,r^{\prime}$. Now let $o\in\mathcal{O}$ such that $\mu r\in o(\{\ast\})$, then there is a collection of pairs $\{(o_{i},\Phi_{i})\}_{i\in I}$ satisfying the properties given above. So by property (1), $\forall i\in I,~{}r\in o_{i}(\llbracket\Phi_{i}\rrbracket)$, and since $r\curlyeqprec\,r^{\prime}$ it holds that $r^{\prime}\in o_{i}(\llbracket\Phi_{i}\rrbracket)$. By property (2) we conclude that $\mu r^{\prime}\in o(\{\ast\})$ which is what we needed to prove. ∎

Below, we shall show that all our running examples satisfy the decomposability property. In all cases we can do this by establishing a stronger property that is easier to verify. This strengthened notion of decomposability is obtained by simplifying the property given in Lemma 4.17.

Definition 4.18** (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 o(\{\ast\})$, there exists a collection $\{(o_{i},o_{i}^{\prime})\}_{i\in I}$ of pairs of modalities such that:

$\forall i\in I,~{}r\in o_{i}(o_{i}^{\prime}(\{\ast\}))\,$; and 2. 2.

for every $r^{\prime}\in TT\mathbf{1}$, if for all $i\in I$, $r^{\prime}\in o_{i}(o_{i}^{\prime}(\{\ast\}))$ then $\mu r^{\prime}\in o(\{\ast\})\,$.

Proposition 4.19**.**

If $\mathcal{O}$ is strongly decomposable set of upwards closed modalities, then $\mathcal{O}$ is decomposable.

Proof.

Using Lemma 4.17, this result is a simple consequence of the fact that for any $o_{i}\in\mathcal{O}$, $o_{i}(\top)\in\textit{CF}_{\mathcal{V}^{+}}\,(\mathbf{1})$ and $\llbracket o_{i}(\top)\rrbracket=o_{i}(\{\ast\})$. ∎

Not all decomposable sets of Scott open modalities are strongly decomposable. Take for instance $\mathcal{O}:=\{\downarrow,\widehat{\Box}\}$ for the signature $\Sigma=\{\textit{or}:\alpha^{2}\rightarrow\alpha\}$, where $\llbracket{\downarrow}\rrbracket:=\{\,*\,\}$ and $\llbracket\widehat{\Box}\rrbracket:=(\llbracket\Box\rrbracket-\{\,*\,\})$.

We end this section by again looking at our running examples, and showing, in each case, that the identified collection $\mathcal{O}$ only has Scott-open (hence upwards closed) modalities and is 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\,\downarrow\!(\downarrow\!(\{\ast\}))$, 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 strong decomposability holds since: $\mu r\in\llbracket\downarrow\rrbracket\Leftrightarrow r\in\,\downarrow\!(\downarrow\!(\{\ast\}))$ like in the previous example, and:

$\mu r\in\llbracket\mathsf{E}_{e}\rrbracket\quad\Leftrightarrow\quad r\in\mathsf{E}_{e}(\mathsf{E}_{e}(\{\ast\}))~{}\vee~{}r\in\,\downarrow\!(\mathsf{E}_{e}(\{\ast\}))$.

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

Example 2** (Nondeterminism).**

We have $\mathcal{O}=\{\Diamond\}$ for angelic nondeterminism and $\mathcal{O}=\{\Box\}$ for demonic nondeterminism. The Scott-openness of \llbracket{\Diamond}\rrbracket=\{t\mid\text{t$has some$ leaf}\} holds 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\text{t$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$ for that $i$. Strong decomposability holds because:

$\mu r\in\llbracket\Diamond\rrbracket~{}\Leftrightarrow~{}r\in\Diamond(\Diamond(\{\ast\}))\quad\text{and}\quad\mu r\in\llbracket\Box\rrbracket~{}\Leftrightarrow~{}r\in\Box(\Box(\{\ast\})\enspace.$

The former states that $r$ has as a leaf a tree $t$, which itself has a leaf $*$. The latter states that $r$ is finite and all leaves are finite trees $t$ that have only $*$ leaves. We can conclude that $\{\Diamond\}$ and $\{\Box\}$ are both strongly decomposable sets of Scott open modalities. Moreover, it is obvious that their union $\{\Diamond,\Box\}$, for neutral nondeterminism, is a strongly decomposable set of Scott open modalities too.

Example 3** (Probabilistic choice).**

$\mathcal{O}=\{\mathsf{P}_{>q}\mid q\in\mathbb{Q},\,0\leq q<1\}$. For the Scott-openness of \llbracket\mathsf{P}_{>q}\rrbracket=\{t\mid\mathbf{P}(\,\text{t$terminates with a$ leaf}\,)>q\}, note that \mathbf{P}(\,\text{\sqcup_{i}t_{i}$terminates with a$ 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$.

For strong decomposability, suppose $\mu r\in\mathsf{P}_{>q}(\{\ast\})\,$. However, \mathbf{P}(\,\text{\mu r$terminates with a$* leaf}\,) equals the integral of the (monotone decreasing) function $f_{r}(x)=\textit{sup}\{y\in[0,1]\mid r\in\mathsf{P}_{>y}(\mathsf{P}_{>x}(\{\ast\}))\}$ from $[0,1]$ to $[0,1]$. Informally, $f_{r}(x)$ is the probability that $r$ returns a tree in the set $\llbracket\mathsf{P}_{>x}\rrbracket$. Since $\int_{0}^{1}f_{r}(x)>q$, we can find a monotone decreasing rational step function below $f_{r}$ whose integral is also greater than $q$. This rational step function can be specified by rational numbers $0<a_{0}<\dots<a_{n}<1$ and $1>b_{0}>\dots>b_{n}>0$ satisfying $b_{i}<f_{r}(a_{i})$ and $a_{0}b_{0}+\sum_{i=1}^{n}(a_{i}-a_{i-1})b_{i})>q\,$. Then the collection of pairs of modalities $\{(\mathsf{P}_{>a_{i}},\mathsf{P}_{>b_{i}})\}_{i=1}^{n}$ satisfies the properties required by strong decomposability.

Example 4** (Global store).**

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

$\mu r\in\llbracket s\rightarrowtail s^{\prime}\rrbracket\quad\Leftrightarrow\quad\exists s^{\prime\prime}\in\textit{State},\,r\in(s\rightarrowtail s^{\prime\prime})((s^{\prime\prime}\rightarrowtail s^{\prime})(\{\ast\}))$.

Which just means that for some $s^{\prime\prime}$, it holds that $\textit{exec}(r,s)=(t,s^{\prime\prime})$ and $\textit{exec}(t,s^{\prime\prime})=(*,s^{\prime})$.

Example 5** (Input/output).**

We have \mathcal{O}=\{{\langle w\rangle\!\!\downarrow},\,\langle w\rangle_{\!\dots}\mid\text{w 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:

$\mu r\in\llbracket\langle w\rangle\!\!\downarrow\rrbracket\quad\Leftrightarrow\quad\exists v,u$ i/o-traces$,~{}vu=w~{}\wedge~{}r\in\langle v\rangle\!\!\downarrow\!(\langle u\rangle\!\!\downarrow\!(\{\ast\}))$.

Which means $r$ follows trace $v$ returning $t$, and $t$ follows trace $u$ returning $*$.

$\mu r\in\llbracket\langle w\rangle_{\!\dots}\rrbracket\;\Leftrightarrow\quad r\in\langle w\rangle_{\!\dots}(\langle\rangle_{\!\dots}(\{\ast\}))~{}\vee~{}(\exists v,u,~{}vu=w~{}\wedge~{}r\in\langle v\rangle\!\!\downarrow(\langle u\rangle_{\!\dots}(\{\ast\})))$.

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

In Example 2 above, we used the obvious fact that the property of being strongly decomposable is preserved under union. Similarly, if all modalities are upwards-closed, then by Lemma 4.17, the property of being decomposable is preserved under union.

Lemma 4.20**.**

If $\,\mathcal{O}_{0}$ and $\mathcal{O}_{1}$ are decomposable sets of upwards closed modalities for the same signature $\Sigma$, then $\mathcal{O}_{0}\cup\mathcal{O}_{1}$ is decomposable.

In order to prove Theorem 1, we need to relate the behavioural equivalence $\equiv_{\mathcal{V}}$ with a modality-defined notion of applicative bisimilarity. As motivated in the introduction, the connection between these two equivalences is interesting on its own. We will spend the next two sections defining this notion of bisimilarity, establishing the connection with behavioural equivalence and proving that the two relations are compatible. From Section 7 and onwards, we will return to only studying the behavioural equivalence.

5 Applicative $\mathcal{O}$-(bi)similarity

In this section, we define this notion of applicative bisimilarity based on a set of modalities $\mathcal{O}$, and establish that it is equal to the behavioural equivalence $\equiv_{\mathcal{V}}$. Central to such a definition lies the concept of a relator [49, 21], which we use to lift a relation on value terms to a relation on computation terms. Later on in this section, we will prove that this relator, if based on a decomposable set of Scott open modalities $\mathcal{O}$, satisfies the right properties in order to prove the compatibility of bisimilarity in Section 6.

Let $\mathcal{O}$ be some set of modalities for an effect signature $\Sigma$. We define a relator based on $\mathcal{O}$.

Definition 5.1** ($\mathcal{O}$-relator).**

The $\mathcal{O}$-relator lifts for each two sets $X$ and $Y$ a relation $\mathcal{R}\subseteq X\times Y$ to a relation $\mathcal{O}(\mathcal{R})\subseteq TX\times TY$, such that

[TABLE]

Remember that ${{\mathcal{R}}^{\uparrow}A}:=\{y\in Y\mid\exists x\in A,x\,\mathcal{R}\,y\}$, and $t\in o(A)$ means $t[\in A]\in\llbracket o\rrbracket$. By Proposition 4.12 it holds that $\mathcal{O}(\textit{id}_{\mathbf{1}})=(\preccurlyeq)$, and by Lemma 4.14 we know that $\mathcal{O}(\preccurlyeq)=\,\curlyeqprec$.

We will use this relator to define an $\mathcal{O}$-tailored variant of Abramsky’s applicative similarity [3]. First however, we describe the specific $\mathcal{O}$-relators that arise for each of our running examples.

Example 0** (Pure functional computation).**

The statement $t\,\{{\downarrow}\}(\mathcal{R})\,r$ holds if and only if:

When $t$ evaluates to $x\in X$ then $r$ evaluates to a $y\in Y$ such that $x\,\mathcal{R}\,y$.

Example 1** (Error).**

The statement $t~{}(\{{\downarrow}\}\cup\{\mathsf{E}_{e}\mid e\in E\})(\mathcal{R})~{}r$ holds precisely when the following two statements hold:

When $t$ evaluates to $x\in X$ then $r$ evaluates to a $y\in Y$ such that $x\,\mathcal{R}\,y$. 2. -

When $t$ raises an error $e\in E$ (meaning it is node $\textit{raise}_{e}$), then $r$ raises the same error $e$.

Example 2** (Nondeterminism).**

$t~{}\{\Diamond,\,\Box\}(\mathcal{R})~{}r$ holds precisely when the following statements hold:

If $x\in X$ is a leaf of $t$, then $r$ has a leaf $y\in Y$ such that $x\,\mathcal{R}\,y$. 2. -

If $t$ is finite and has no $\bot$ leaf, then $r$ is finite and has no $\bot$-leaf. 3. -

If $t$ is finite, has no $\bot$ leaf, and $y\in Y$ is a leaf of $r$, then $t$ has a leaf $x\in X$ such that $x\,\mathcal{R}\,y$.

Example 3** (Probabilistic choice).**

It holds that $t~{}\{\mathsf{P}_{>q}\mid q\in\mathbb{Q},\,0\leq q<1\}(\mathcal{R})~{}r$ if and only if:

For any $A\subseteq X$, the probability of $t$ terminating with an element of $A$ is at most the probability of $r$ terminating with a $y$ related to some element of $A$ (meaning there is an $x\in A$ such that $x\,\mathcal{R}\,y$).

Example 4** (Global store).**

The statement $t~{}\{(s\rightarrowtail s^{\prime})\mid s,s^{\prime}\in\textit{State}\}(\mathcal{R})~{}r$ holds if:

For any $s\in\textit{State}$, if $\textit{exec}(t,s)=(x,s^{\prime})$ then there is a $y\in Y$ such that $\textit{exec}(r,s)=(y,s^{\prime})$ and $x\,\mathcal{R}\,y$.

Example 5** (Input/output).**

$t~{}\{{\langle w\rangle\!\!\downarrow},\,\langle w\rangle_{\!\dots}\mid w\text{ an i/o-trace}\}(\mathcal{R})~{}r$ holds precisely when the following two statements hold:

If $t$ has $w$ as initial execution trace, then $r$ has $w$ as an initial execution trace. 2. -

If $t$ has execution trace $w$ terminating with $x\in X$, then $r$ has trace $w$ terminating with some $y\in Y$ such that $x\,\mathcal{R}\,y$.

In each of the examples above, we obtain an $\mathcal{O}$-relator that acts in line with expectations, based on the explicit definitions of relators for different effects in the paper by Dal Lago et al. [17]. In our case, these relators have been obtained in a uniform way from the corresponding sets of modalities $\mathcal{O}$.

A direct comparison with definitions in the paper [17] is slightly involved, because our relators act on the set of effect trees, given by applying the effect-tree monad $T$, whereas those in the paper [17] are defined using effect-dependent monads $M$. For example, for probabilistic choice the distribution monad is used. Despite this difference, there is still a tight relationship between the two approaches. The tree monad $T$ is the free-continuous-algebra monad over the effect signature $\Sigma$. There is thus an induced $\rho_{X}:TX\to MX$, mapping trees to elements of the effect-specific monad $MX$. It then holds, for each effect example, that

[TABLE]

where $\Gamma$ is the relevant relator from the paper [17] and $\mathcal{O}$ is the corresponding set of modalities from this paper.

Following the paper [17], we use the relation-lifting operation of Definition 5.1 to define notions of applicative similarity and bisimilarity. We assume that all modalities of $\mathcal{O}$ are upwards closed.

Definition 5.2** (Similarity).**

An applicative $\mathcal{O}$-simulation is 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:

$V\,\mathcal{R}^{v}_{\mathbf{N}}\,W~{}\implies~{}(V=W)$ . 2. 2.

$M\,\mathcal{R}^{c}_{\tau}\,N~{}\implies~{}|M|$ $\mathcal{O}(\mathcal{R}^{v}_{\tau})$ $|N|$ . 3. 3.

$V\,\mathcal{R}^{v}_{\rho\rightarrow\tau}\,W~{}\implies~{}\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 5.3** (Bisimilarity).**

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

Applicative $\mathcal{O}$-similarity and $\mathcal{O}$-bisimilarity may not exist for all sets of modalities $\mathcal{O}$. But, if all modalities of $\mathcal{O}$ are upwards closed (as asserted above), their existence is guaranteed. Though this fact can be proven directly from relational properties established in Lemma 5.6, we can also see it as a consequence of Theorem 2.

Lemma 5.4**.**

Applicative $\mathcal{O}$-bisimilarity is identical to the relation of applicative $(\mathcal{O}\cap\mathcal{O}^{\mathsf{op}})$-similarity, where $\mathcal{O}^{\mathsf{op}}(\mathcal{R}):=(\mathcal{O}(\mathcal{R}^{\mathsf{op}}))^{\mathsf{op}}$, so $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|$, so $\mathcal{R}$ is an $\mathcal{O}\cap\mathcal{O}^{\mathsf{op}}$-simulation.

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 an $\mathcal{O}\cap\mathcal{O}^{\mathsf{op}}$-simulation. So $\mathcal{R}=\mathcal{R}\cup\mathcal{R}^{\mathsf{op}}$ and hence $\mathcal{R}$ is a symmetric $\mathcal{O}$-simulation. ∎

For brevity, we will leave out the word “applicative” from here on out. The key result now is that the maximal relation, the $\mathcal{O}$-similarity is, given our assertion that all modalities are upwards closed, the same object as our logical preorder. We first give a short Lemma.

Lemma 5.5** (Characteristic formulas).**

For any fragment $\mathcal{L}$ of $\,\mathcal{V}$ closed under countable conjunction, it holds that for each value $V$ there is a formula $\chi^{\mathcal{L}}_{V}\in\mathcal{L}$ such that $W\models_{\mathcal{L}}\chi^{\mathcal{L}}_{V}\Leftrightarrow V\sqsubseteq_{\mathcal{L}}W$. Similarly, for every computation $M$, there is a computation formula ${\chi}^{\mathcal{L}}_{M}\in\mathcal{L}$ such that $N\models_{\mathcal{L}}{\chi}^{\mathcal{L}}_{M}\Leftrightarrow M\sqsubseteq_{\mathcal{L}}N$.

Proof.

We prove the statement for values $V$. 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\}}(U\mapsto\phi^{U})$ it holds that $V\not\sqsubseteq_{\mathcal{L}}U\Leftrightarrow U\not\models\chi_{V}$, which is what we want. ∎

As in the proof above, we usually omit the superscript $\mathcal{L}$ when clear from the context. Note that when $\mathcal{L}$ is the full logic $\mathcal{V}$, it holds that

[TABLE]

and similarly for value formulas.

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.

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 o(A)$. Taking the following formula $\phi_{A}:=\bigvee_{a\in A}\chi_{a}$ (where $\chi_{a}$ as in Lemma 5.5), then $b\models\phi_{A}\Leftrightarrow\exists a\in A,a\sqsubseteq^{v}_{\tau}b\Leftrightarrow b\in{{(\sqsubseteq^{v}_{\tau})}^{\uparrow}A}$ and $\forall a\in A,a\models\phi_{A}$. So $|M|[\models\phi_{A}]\geq|M|[{\in A}]$, hence since $o$ is upwards closed, $|M|[\models\phi_{A}]\in\llbracket o\rrbracket$. By $M\sqsubseteq^{c}_{\tau}N$ we have $|N|[\models\phi_{A}]\in\llbracket o\rrbracket$ and hence $|N|\in o({{(\sqsubseteq^{v}_{\tau})}^{\uparrow}A})$. We conclude that $|M|\,\mathcal{O}(\sqsubseteq^{v}_{\tau})\,|N|$. 3. 3.

Function values of $\rho\rightarrow\tau$. This step follows from Lemma 4.3 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)$.

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 4.4. 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)\,\mid\,a\models\phi\}}\subseteq\textit{Val}(\tau)$, then $|M|\in o(A_{\phi})$ hence by $M\,\mathcal{R}^{c}_{\tau}\,N$ and the simulation property, we derive $|N|\in o({{(\mathcal{R}^{v}_{\tau})}^{\uparrow}A_{\phi}})$. By the 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]\geq|N|[{\in{{(\mathcal{R}^{v}_{\tau})}^{\uparrow}A_{\phi}}}]$, so by upwards closure of $o$ we have $|N|[\models\phi]\in\llbracket o\rrbracket$ 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 4.3. Assume $V\models(U\mapsto\Phi)$ where $U\in\textit{Val}(\rho)$ and $\Phi\in\textit{CF}\,(\tau)$, so $VU\models\Phi$. By $V\,\mathcal{R}^{v}_{\rho\rightarrow\tau}\,W$ we have $VU\;\mathcal{R}^{c}_{\tau}\;WU$ and by the induction hypothesis we have $\mathcal{R}^{c}_{\tau}\subseteq(\sqsubseteq^{c}_{\tau})$, so $VU\sqsubseteq^{c}_{\tau}WU$. Hence $WU\models\Phi$ meaning $W\models(U\mapsto\Phi)$. We can conclude that $V\sqsubseteq^{v}_{\rho\rightarrow\tau}W$. 4. 4.

Values of $\bf{1}$. If $V\,\mathcal{R}^{v}_{\bf{1}}\,W$ then $V=*=W$ hence $V\sqsubseteq^{v}_{\bf{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. ∎

Adapting the proof slightly, we can find the connection between full behavioural equivalence and $\mathcal{O}$-bisimilarity.

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 5.5, that for any $V$, there is a formula $\chi_{V}$ such that $W\models\chi_{V}\Leftrightarrow V\equiv_{\mathcal{V}}W$. Using these observations and the appropriate adjustments to Lemma 4.3 and 4.4, the proof of this result is as in Theorem 2(A), proving $\equiv_{\mathcal{V}}$ is a symmetric $\mathcal{O}$-simulation and contains any other symmetric $\mathcal{O}$-simulation. ∎

Given Theorem 2(b), it is straightforward to observe an expressive completeness result with respect to the notion of behavioural property induced by $\mathcal{O}$-bisimilarity (as adumbrated in Section 1). A subset $S\subseteq\textit{Com}(\tau)$ (respectively $S\subseteq\textit{Val}(\tau)$) may be called behavioural if it respects bisimilarity; that is, in the case of computations, if $M\in S$ and $M$ is bisimilar to $M^{\prime}$ then $M^{\prime}\in S$. It follows from Theorem 2(b) that the behavioural subsets coincide with the logically definable subsets. Namely, $S\subseteq\textit{Com}(\tau)$ is behavioural if and only if there exists a formula $\Phi\in\textit{CF}\,(\tau)$ such that $S=\{M\mid M\models\Phi\}$; and similarly, any $S\subseteq\textit{Val}(\tau)$ is behavioural if and only if there exists a formula $\phi\in\textit{VF}\,(\tau)$ such that $S=\{V\mid V\models\phi\}\,$. The proof is straightforward, given the observation that every behavioural $S$ is a union of equivalence classes under bisimilarity. Hence, for example, $\Phi$ may be defined as an infinite disjunction

[TABLE]

using the characteristic formulas obtained in (4) above.

5.1 Relator properties

In this subsection, we identify abstract properties of our relation lifting $\mathcal{O}(\mathcal{R})$, which will be used in our application of Howe’s method, in Section 6. The necessary properties were identified in the paper [17]. 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 indeed a relator in the sense of Levy [21].

Lemma 5.6**.**

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

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

$\forall\mathcal{R}\subseteq X\times Y,\forall\mathcal{S}\subseteq Y\times Z,\,\,\mathcal{O}(\mathcal{R})\,\mathcal{O}(\mathcal{S})\subseteq\mathcal{O}(\mathcal{R}\mathcal{S})$, where $\mathcal{R}\mathcal{S}\subseteq X\times Z$ is relation composition. 3. 3.

$\forall\mathcal{R}\subseteq X\times Y,\forall\mathcal{S}\subseteq X\times Y,\,\,\mathcal{R}\subseteq\mathcal{S}\Rightarrow\mathcal{O}(\mathcal{R})\subseteq\mathcal{O}(\mathcal{S})$. 4. 4.

$\forall f:X\to Z,g:Y\to 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\,\mid\,f(x)\,\mathcal{R}\,g(y)\}$ 999In general, given $h:X\to Y$, $A\subseteq X$, and $B\subseteq Y$, we write $h(A):=\{h(x)\mid x\in X\}$ and $h^{-1}(B):=\{x\in X\mid{h(x)\in B}\}$..

Proof.

We prove each property separately.

For any set $A\subseteq X$ we have $A\subseteq({{\mathcal{R}}^{\uparrow}A})$ by reflexivity of $\mathcal{R}$. So for any $t\in TX$, if $t\in o(A)$ then by upwards closure of $o$ we have $t\in o({{\mathcal{R}}^{\uparrow}A})$. We conclude that $t\,\mathcal{O}(\mathcal{R})\,t$. 2. 2.

We can see this by observing that ${{(\mathcal{R}\mathcal{S})}^{\uparrow}A}=\{z\in Z\mid\exists x\in X,y\in Y,x\,\mathcal{R}\,y\,\mathcal{S}\,z\}={{\mathcal{S}}^{\uparrow}({{\mathcal{R}}^{\uparrow}A})}$, and with $t\,\mathcal{O}(\mathcal{R})\,r\,\mathcal{O}(\mathcal{S})\,l$ it holds that $t\in o(A)\Rightarrow r\in o({{\mathcal{R}}^{\uparrow}A})\Rightarrow l\in o({{\mathcal{S}}^{\uparrow}({{\mathcal{R}}^{\uparrow}A})})$. 3. 3.

With $\mathcal{R}\subseteq\mathcal{S}$ it holds that ${{\mathcal{R}}^{\uparrow}A}\subseteq{{\mathcal{S}}^{\uparrow}A}$ for any set $A\subseteq X$. Assume $t\,\mathcal{O}(\mathcal{R})\,r$ and $t\in o(A)$, then $r\in o({{\mathcal{R}}^{\uparrow}A})$. Hence with $r[{\in{{\mathcal{S}}^{\uparrow}A}}]\geq r[{\in{{\mathcal{R}}^{\uparrow}A}}]$ and by upwards closure of $o$, $r\in o({{\mathcal{S}}^{\uparrow}A})$. 4. 4.

If $t\,\mathcal{O}((f\times g)^{-1}\mathcal{R})\,r$ then for all $A\subseteq X$ and $o\in\mathcal{O}$, $t\in o(A)\Rightarrow r\in o({{((f\times g)^{-1}\mathcal{R})}^{\uparrow}A})\Rightarrow r\in o(g^{-1}({{\mathcal{R}}^{\uparrow}f(A)})$. Assume that for some $B$ we have $Tf(t)\in o(B)$, then $t\in o(f^{-1}(B))$ so $r\in o(g^{-1}({{\mathcal{R}}^{\uparrow}f(f^{-1}(B))}))$. Considering that $f(f^{-1}(B))\subseteq B$ and $o$ is upwards closed, we derive that $r\in o(g^{-1}({{\mathcal{R}}^{\uparrow}B}))$ and hence $Tg(r)\in o({{\mathcal{R}}^{\uparrow}B})$. This is for all such $B$ and $o$, so we can conclude that $Tf(t)\,\mathcal{O}(\mathcal{R})\,Tg(r)$.

Now assume $Tf(t)\,\mathcal{O}(\mathcal{R})\,Tg(r)$ and $t\in o(A)$, then since $Tf(t)\in o(f(A))$ we have $Tg(r)\in o({{\mathcal{R}}^{\uparrow}f(A)})$ so $r\in o(g^{-1}({{\mathcal{R}}^{\uparrow}f(A)}))$. This is for all such $A$ and $o$, hence $t\,\mathcal{O}((f\times g)^{-1}\mathcal{R})\,r$.

∎

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

Lemma 5.7**.**

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

[TABLE]

Proof.

Let $\mathcal{R}\subseteq X\times Y$ and $\mathcal{S}\subseteq A\times B$. Assume: (i) $\forall x,y,x\,\mathcal{R}\,y\Rightarrow f(x)\,\mathcal{S}\,g(y)$ and (ii) $t\,\mathcal{O}(\mathcal{R})\,r$.

Take $o\in\mathcal{O}$ and $K\subseteq TA$ such that $t[x\mapsto f(x)]\in o(K)$. Take $L=f^{-1}(K)$, then $t\in o(L)$. So by (ii), $r\in o({{\mathcal{R}}^{\uparrow}L})$. For $y\in({{\mathcal{R}}^{\uparrow}L})$, there is an $x\in L$ such that $x\,\mathcal{R}\,y$, hence by (i) we have $f(x)\,\mathcal{S}\,g(y)$. Since $x\in L$ means $f(x)\in K$, it holds that $g(y)\in({{\mathcal{S}}^{\uparrow}K})$, hence $({{\mathcal{R}}^{\uparrow}L})\subseteq g^{-1}({{\mathcal{S}}^{\uparrow}K})$. Using upwards closure of $o$, $r\in o(g^{-1}({{\mathcal{S}}^{\uparrow}K}))$, and hence $r[y\mapsto g(y)]\in o({{\mathcal{S}}^{\uparrow}K})$. Since this is for all $o\in\mathcal{O}$ and $K\subseteq TA$ with $t[x\mapsto f(x)]\in o(K)$, we can conclude that $t[x\mapsto f(x)]\,\mathcal{O}(\mathcal{S})\,r[y\mapsto g(y)]$. ∎

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

Lemma 5.8**.**

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

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

Proof.

We prove the properties separately.

Note that $\eta(x)\in o(A)$ either means $x\in A$ and $\ast\in\llbracket o\rrbracket$, or $\bot\in\llbracket o\rrbracket$. By upwards closure, if $\bot\in\llbracket o\rrbracket$ then $\llbracket o\rrbracket=T\mathbf{1}$. If $x\in A$ then $y\in{{\mathcal{R}}^{\uparrow}A}$. Either way, $\eta(y)\in o({{\mathcal{R}}^{\uparrow}A})$. 2. 2.

Take $t\,\mathcal{O}(\mathcal{O}(\mathcal{R}))\,r$ and $(\mu t)\in o(K)$ where $o\in\mathcal{O}$. Take $A\subseteq T\mathbf{1}$ and $\gamma\in\mathcal{O}$ such that ${t[a\mapsto a[{\in K}]]}\in\gamma(A)$. Let $S:=\{a\,\mid\,a[{\in K}]\in A\}$, then $t\in\gamma(S)$. By $t\,\mathcal{O}(\mathcal{O}(\mathcal{R}))\,r$ we get $r\in\gamma({{\mathcal{O}(\mathcal{R})}^{\uparrow}S})$.

In the following paragraph we prove that for $b\in({{\mathcal{O}(\mathcal{R})}^{\uparrow}S})$, $b[{\in{{\mathcal{R}}^{\uparrow}K}}]\in({{\preccurlyeq}^{\uparrow}A})$, using characterisation 3 of $\preccurlyeq$ from Proposition 4.12.

For $b\in({{\mathcal{O}(\mathcal{R})}^{\uparrow}S})$, there is an $a\in S$ such that $a[{\in K}]\in A$ and $a\,\mathcal{O}(\mathcal{R})\,b$. If $a[{\in K}]\in\delta(\{\ast\})$ for some $\delta\in\mathcal{O}$, then $a\in\delta(K)$, so $b\in\delta({{\mathcal{R}}^{\uparrow}K})$ and hence $b[{\in{{\mathcal{R}}^{\uparrow}K}}]\in\delta(\{\ast\})$. If $a[{\in K}]\in\delta(\emptyset)$ for some $\delta\in\mathcal{O}$, then $a\in\delta(\emptyset)$, so we have $b\in\delta({{\mathcal{R}}^{\uparrow}\emptyset})$. Since ${{\mathcal{R}}^{\uparrow}\emptyset}=\emptyset$, $b\in\delta(\emptyset)$ and hence $b[{\in{{\mathcal{R}}^{\uparrow}K}}]\in\delta(\emptyset)$. With the previous two derivations, we see that $a[{\in K}]\preccurlyeq b[{\in{{\mathcal{R}}^{\uparrow}K}}]$, hence $b[{\in{{\mathcal{R}}^{\uparrow}K}}]\in({{\preccurlyeq}^{\uparrow}A})$ since $a[{\in K}]\in A$. So the following inclusion holds:

[TABLE]

By upwards closure of $\gamma$ and $r\in\gamma({{\mathcal{O}(\mathcal{R})}^{\uparrow}S})$ we get $r\in\gamma(\{b\,\mid\,b[{\in{{\mathcal{R}}^{\uparrow}K}}]\in({{\preccurlyeq}^{\uparrow}A})\})$. So we have derived that $(t[a\mapsto a[{\in K}]]\in\gamma(A))\Rightarrow(r[b\mapsto b[{\in{{\mathcal{R}}^{\uparrow}K}}]]\in\gamma({{\preccurlyeq}^{\uparrow}A}))$ for all $\gamma$ and $A$. By Lemma 4.14, $t[a\mapsto a[{\in K}]]\curlyeqprec r[b\mapsto b[{\in{{\mathcal{R}}^{\uparrow}K}}]]$, hence by decomposability we get $(\mu t)[{\in K}]={\mu(t[a\mapsto a[{\in K}]])}\preccurlyeq\mu(r[b\mapsto b[{\in{{\mathcal{R}}^{\uparrow}K}}]])=(\mu r)[{\in{{\mathcal{R}}^{\uparrow}K}}]$. Hence with $\mu t\in o(K)$ assumed at the beginning, we get $\mu t\in o({{\mathcal{R}}^{\uparrow}K})$, and we conclude $\mu t\,\mathcal{O}(\mathcal{R})\,\mu r$.

∎

Finally, the following properties show that relators behave well with respect to the order on trees.

Lemma 5.9**.**

If $\,\mathcal{O}$ only contains Scott open modalities, then for $\mathcal{R}\subseteq X\times Y$:

If $\,\mathcal{R}$ is reflexive, then for any $t\in TX,r\in TY$ it holds that $t\leq r\Rightarrow t\,\mathcal{O}(\mathcal{R})\,r$. 2. 2.

For any two sequences $u_{0}\leq u_{1}\leq u_{2}\leq\dots$ from $TX$ and $v_{0}\leq v_{1}\leq v_{2}\leq\dots$ from $TY$:

$\forall n,(u_{n}\,\mathcal{O}(\mathcal{R})\,v_{n})~{}\Rightarrow~{}(\sqcup_{n}u_{n})\,\mathcal{O}(\mathcal{R})\,(\sqcup_{n}v_{n})$**

Proof.

We separate the proofs by property.

If $\mathcal{R}$ is reflexive then $\mathcal{O}(\mathcal{R})$ is reflexive by Lemma 5.6. Now for $t\leq r$, if $t\in o(A)$ then since $t[{\in A}]\leq r[{\in A}]$ we have $r\in o(A)$. By reflexivity $r\,\mathcal{O}(\mathcal{R})\,r$, so $r\in o({{\mathcal{R}}^{\uparrow}A})$. 2. 2.

Take $A\subseteq X$ and $o\in\mathcal{O}$ such that $(\sqcup_{n}u_{n})\in o(A)$. Now $(\sqcup_{n}u_{n})[{\in A}]=\sqcup_{n}(u_{n}[{\in A}])$ so by Scott openness, there is an $m$ such that $u_{m}\in o(A)$. Using the assumption we derive $v_{m}\in o({{\mathcal{R}}^{\uparrow}A})$. Note that $v_{m}\leq\sqcup_{n}v_{n}$, hence $v_{m}[{\in{{\mathcal{R}}^{\uparrow}A}}]\leq\sqcup_{n}v_{n}[{\in{{\mathcal{R}}^{\uparrow}A}}]$, so since $o$ is Scott open we conclude that $(\sqcup_{n}v_{n})\in o({{\mathcal{R}}^{\uparrow}A})$.

∎

The lemmas above list the core properties of the relator, which are satisfied when our set $\mathcal{O}$ is decomposable and contains only Scott open modalities. The results below follow from those above, specifically the next result combines Lemma 5.8 with the fact that $\mathcal{O}(\text{id}_{\mathbf{1}})=\,\preccurlyeq$ and $\mathcal{O}(\preccurlyeq)=\curlyeqprec$.

Corollary 5.10**.**

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

[TABLE]

Lastly, we verify that sequencing and the algebraic effect operations interact in the appropriate way with the relator action.

Corollary 5.11**.**

If $\,\mathcal{O}$ is a decomposable set of upwards closed modalities, then lifted relations are preserved by Kleisli lifting and effect operations:

Given $f:X\to TZ$, $g:Y\to TW$, $\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)$**

Proof.

We prove the properties separately.

Using Lemma 5.7 on the assumptions we get $t[x\mapsto f(x)]\,\mathcal{O}(\mathcal{O}(\mathcal{S}))\,r[y\mapsto g(y)]$. We can then apply property 2 of Lemma 5.8 to get the correct result. 2. 2.

We apply the previous property to the following data; $t=r=\sigma(0,1,2,\dots)\in T\mathbb{N}$, $f(n)=u_{n}$, $g(n)=v_{n}$ for all $n\in\mathbb{N}$, and $\mathcal{R}=\textit{id}_{\mathbb{N}}$. The conclusion follows directly.

∎

Point 2 of Corollary 5.11 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$ of effect operations $\sigma$. So it states that any lifted relation is preserved under any of the predefined algebraic effects (assuming equality between any possible natural numbers arguments given by the arity). The next section focusses on proving Theorem 1 using a generalisation of Howe’s method.

6 Howe’s method

In this section, we apply Howe’s method [11, 12] to establish the compatibility of applicative $\mathcal{O}$-similarity and $\mathcal{O}$-bisimilarity, and hence compatibility of the positive behavioural preorder and full behavioural equivalence. 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 use of the relator properties from Section 5, closely following the approach of Dal Lago et al. [17]. We will only give an outline of the proof, focussing on the main steps. Detailed proofs can be found in Appendix A.

Recall from Section 4 that, for any closed relation $\mathcal{R}$, we can define the open extension $\mathcal{R}^{\circ}$ as $\Gamma\vdash M\,\mathcal{R}^{\circ}\,N:\tau\Leftrightarrow\forall\overrightarrow{V}:\Gamma,M[\overrightarrow{V}]\,\mathcal{R}\,N[\overrightarrow{V}]$. We define two more closure operations.

Definition 6.1**.**

Taking an open relation $\mathcal{R}$, we define the compatible refinement $\widehat{\mathcal{R}}$ using the derivation rules in Fig. 4. For a closed relation $\mathcal{R}$ we define the Howe closure $\mathcal{R}^{\bullet}$ as the smallest open relation $\mathcal{S}$ closed under the rules:

[TABLE]

Note that $\mathcal{R}$ is compatible if and only if $\,\widehat{\mathcal{R}}\subseteq\mathcal{R}$. The Howe closure can also be expressed as the least solution for $\mathcal{S}$ of the equation $\mathcal{S}=\widehat{\mathcal{S}}\mathcal{R}^{\circ}$, or of the inclusion $\widehat{\mathcal{S}}\mathcal{R}^{\circ}\subseteq\mathcal{S}$.

The following result contains the main properties of the Howe closure we are interested in, e.g. from Lassen [19].

Lemma 6.2**.**

If  $\mathcal{R}$ is reflexive, then:

$\mathcal{R}^{\bullet}$* is compatible, hence reflexive.* 2. 2.

$\mathcal{R}^{\circ}\subseteq\mathcal{R}^{\bullet}$. 3. 3.

If $x:\rho\vdash A\,\mathcal{R}^{\bullet}B$ and $V,W:\rho$ such that $V\,\mathcal{R}^{\bullet}\,W$, then $A[V]\,\mathcal{R}^{\bullet}\,B[W]$

The main step of the Howe’s method proof is establishing the following result.

Proposition 6.3**.**

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

This is proven by checking the simulation properties of Definition 5.2 one by one. The most difficulty arises when trying to prove property 2, which is done inductively using the following lemma, and uses most of the relator properties from Subsection 5.1.

Lemma 6.4** (Key Lemma).**

For any $n\in\mathbb{N}$, given two closed computation terms $A$ and $B$, if $A\sqsubseteq^{\bullet}B$ then $|A|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|B|$.

Having established the Key Lemma, we can use Lemma 5.9, implying $(\forall n\in\mathbb{N},\,|A|_{n}\,{\mathcal{O}(\sqsubseteq^{\bullet})}\,|B|)\Rightarrow|A|\,\mathcal{O}(\sqsubseteq^{\bullet})\,|B|$, to derive property 2 of $\mathcal{O}$-simulations and finalise the proof of Proposition 6.3. The complete proofs of the previous lemmas and Proposition 6.3 can be found in Appendix A.

Using Proposition 6.3, we can derive the compatibility of applicative $\mathcal{O}$-similarity and $\mathcal{O}$-bisimilarity.

Theorem 3** (A).**

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

Proof.

Before we start the proof, we observe the following general result. If a compatible relation $\mathcal{R}$ is contained in a closed relation $\mathcal{S}$ when limited to closed terms, then $\mathcal{R}\subseteq\mathcal{S}^{\circ}$ since:

[TABLE]

We write $\sqsubseteq_{s}$ for the relation of $\mathcal{O}$-similarity. Since $\sqsubseteq_{s}$ is an $\mathcal{O}$-simulation, we know by Proposition 6.3 that $\sqsubseteq_{s}^{\bullet}$ limited to closed terms is one as well, and hence is contained in the largest $\mathcal{O}$-simulation $\sqsubseteq_{s}$. By Lemma 6.2 it holds that $\sqsubseteq_{s}^{\bullet}$ is compatible, and by the observation before we know it is contained in the open extension $\sqsubseteq_{s}^{\circ}$. Again by Lemma 6.2, we also know that $\sqsubseteq_{s}^{\circ}$ is contained in $\sqsubseteq_{s}^{\bullet}$. We can conclude that $\sqsubseteq_{s}^{\circ}$ is equal to the Howe closure $\sqsubseteq_{s}^{\bullet}$, which is compatible. ∎

To prove that $\mathcal{O}$-bisimilarity is compatible, we need another result from Lassen [19] (a proof is also given in Appendix A).

Lemma 6.5**.**

If  $\mathcal{R}^{\circ}$ is symmetric and reflexive, then $\mathcal{R}^{\bullet*}$ (the transitive closure of $\mathcal{R}^{\bullet}$) is symmetric.

Given these facts, we can derive the following.

Theorem 3** (B).**

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

Proof.

We write $\mathcal{O}$-bisimilarity as $\sqsubseteq_{b}$. From Proposition 6.3 we know that $\sqsubseteq_{b}^{\bullet}$ on closed terms is an $\mathcal{O}$-simulation. Using property 2 of Lemma 5.6, we can verify that the transitive closure $\sqsubseteq_{b}^{\bullet*}$ is an $\mathcal{O}$-simulation as well. 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*}$ (due to Lemma 6.2 and the same reasoning from the previous proof). Again by Lemma 6.2, it holds that $(\sqsubseteq_{b}^{\circ})\subseteq(\sqsubseteq_{b}^{\bullet})\subseteq(\sqsubseteq_{b}^{\bullet*})$, hence $(\sqsubseteq_{b}^{\bullet*})=(\sqsubseteq_{b}^{\circ})$. We can conclude that $\sqsubseteq_{b}^{\circ}$ is compatible. ∎

Note that Theorem 1 is an immediate consequence of Theorems 2 and 3. As such, we have finished the proof of compatibility of the full behavioural equivalence and positive behavioural preorder.

7 Comparing equivalences

Our development thus far has focused on two main relations for comparing programs. The first is the behavioural equivalence ${\equiv_{\mathcal{V}}}$ defined via the full logic with negation and characterised as $\mathcal{O}$-bisimilarity. The second is the positive behavioural preorder ${\sqsubseteq_{\mathcal{V}^{+}}}$, defined via the negation-free logic and characterised as $\mathcal{O}$-similarity. The latter preorder induces the equivalence relation ${\equiv_{\mathcal{V}^{+}}}$ of mutual $\mathcal{O}$-similarity.

As discussed after Definition 4.2, there is an inclusion ${\equiv_{\mathcal{V}}}\subseteq{\equiv_{\mathcal{V}^{+}}}$. That is, $\mathcal{O}$-bisimilarity implies mutual $\mathcal{O}$-similarity. It is a standard fact in concurrency theory that ordinary mutual similarity is in general a strictly coarser relation than bisimilarity. A similar fact holds in the context of the present paper: it is possible that the inclusion ${\equiv_{\mathcal{V}}}\subseteq{\equiv_{\mathcal{V}^{+}}}$ is strict. We illustrate this with an example, adapted from Lassen’s PhD thesis [19, page 92], for which the two relations do not coincide. (Ong gives another example of a similar phenomenon [30].)

Example 7.1** (Separating the full and positive behavioural equivalence, cf. [19]).**

We take $\Sigma:=\{\textit{or}:\alpha^{2}\rightarrow\alpha\}$ and $\mathcal{O}:=\{\Diamond,\Box\}$ from Example 2. Let $\Omega:\mathbf{1}$ be some always diverging computation term. We consider the following two computation terms of type $(\mathbf{1}\to\mathbf{1})$:

[TABLE]

We make use of our logics $\mathcal{V}$ and $\mathcal{V}^{+}$ to give simple proofs that $M\equiv_{\mathcal{V}^{+}}N$ but $M\not\equiv_{\mathcal{V}}N$.

By definition, $M\equiv_{\mathcal{V}^{+}}N$ if the two terms satisfy the same positive computation formulas of type $(\mathbf{1}\to\mathbf{1})$. Note that $\Diamond(\bot)$ and $\Box(\bot)$ are not satisfied by any terms, $\Diamond(\phi)\vee\Box(\phi)$ is satisfied precisely if $\Diamond(\phi)$ is, and $\Diamond(\phi)\wedge\Box(\phi)$ is satisfied precisely if $\Box(\phi)$ is. Moreover, $(V\mapsto\Phi)\wedge(V\mapsto\Psi)$ and $(V\mapsto\Phi)\vee(V\mapsto\Psi)$ are equivalent to $(V\mapsto(\Phi\wedge\Psi))$ and $(V\mapsto(\Phi\vee\Psi))$ respectively. By these observations and Lemma 4.4, we can reduce the set of formulas we need to check to establish equivalence between two computation terms of type $(\mathbf{1}\to\mathbf{1})$ to:

[TABLE]

The terms $M$ and $N$ both satisfy the same formulas from this set, namely $\Diamond(\top),\Box(\top),\Diamond(\ast\mapsto\Diamond(\top)),$ and $\Diamond(\ast\mapsto\Box(\top))$. We conclude that $M\equiv_{\mathcal{V}^{+}}N$.

The terms $M$ and $N$ are not however equivalent under full behavioural equivalence, since $N$ satisfies the formula $\Diamond(\ast\mapsto(\Diamond(\top)\wedge\neg\Box(\top)))$, but $M$ does not. (This formula says of a computation of type $(\mathbf{1}\to\mathbf{1})$ that it may return a lambda term which, when applied to argument $*$, results in a nondeterministic computation that may diverge and may also terminate.) Thus $M\not\equiv_{\mathcal{V}}N$.

It is also instructive to compare ${\equiv_{\mathcal{V}}}$ and $\equiv_{\mathcal{V}^{+}}$ to contextual equivalence, which is often taken to be the default equivalence for applicative programming languages. For the language of this paper, the collection $\mathcal{O}$ of modalities used to define our logics serves a further purpose: via the preorder $\preccurlyeq$ on unit-type computation trees from Section 4, it gives rise to a natural definition of contextual preorder between terms of the same type and aspect (value or computation). The idea is that two terms $M,N$ of the same type $\tau$ and aspect are related by the contextual preorder $\sqsubseteq_{\text{ctxt}}$ if for any context $C(-)$ of unit type, accepting terms of type $\tau$ of the relevant aspect, we have $|C(M)|\preccurlyeq|C(N)|$.101010If one expands the use of $\preccurlyeq$ in this definition as in statement 3 of Proposition 4.12, one obtains a definition of contextual preorder in terms of basic unit-type ‘observations’ of the form $o(\{*\})$ and $o(\emptyset)$. The same definition can be given more elegantly using compatibility.

Definition 7.2** (Contextual preorder/equivalence).**

The contextual preorder relation $\sqsubseteq_{\text{ctxt}}$ is the largest compatible preorder satisfying:

[TABLE]

The relation $\equiv_{\text{ctxt}}$ of contextual equivalence is the equivalence relation determined by $\sqsubseteq_{\text{ctxt}}$ (i.e., the intersection of $\sqsubseteq_{\text{ctxt}}$ and its converse).

If $\mathcal{O}$ is a decomposable set of Scott-open modalities then, by Theorem 1 and Proposition 4.11, ${\sqsubseteq_{\mathcal{V}^{+}}}$ is a compatible preorder satisfying condition (5) above. Hence, there is an inclusion of relations ${\sqsubseteq_{\mathcal{V}^{+}}}\subseteq{\sqsubseteq_{\text{ctxt}}}$. We thus have a chain of inclusions between equivalence relations.

[TABLE]

Having already shown the left-hand inclusion to be strict in general, we now show that the right-hand inclusion can also be strict. This is again based on an example from Lassen [19].

Example 7.3** (Separating contextual equivalence and positive behavioural equivalence, c.f. [19]).**

We take $\Sigma:=\{\textit{or}:\alpha^{2}\rightarrow\alpha\}$ and $\mathcal{O}:=\{\Diamond\}$ from Example 2, that is we consider angelic nondeterminism.

The example we give differs marginally from Lassen [19, page 90], in that one of the terms involved does not exhibit any effectful behaviour. Let $\textit{id}:\mathbf{N}\to\mathbf{N}$ be the value term given by the identity function $\lambda x:\mathbf{N}.(\textbf{return }x)$. We can define approximations of this identity function, using a term $\textit{apid}:\mathbf{N}\to(\mathbf{N}\to\mathbf{N})$ such that for any two natural numbers $n,m\in\mathbb{N}$:

[TABLE]

So for any natural number $n\in\mathbb{N}$, ‘$\textit{apid}\,\,\overline{n}$’ returns the $n$-th approximation of the identity function.

Given the computation term $?N$ of type $\mathbf{N}$ from Example 2 at the end of Section 2, which nondeterministically returns any natural number, we define the nondeterministic approximation of the identity function:

[TABLE]

This term nondeterministically returns any approximation of the identity function. It holds that $M$ is contextually equivalent to $\textbf{return}(\textit{id})$ under the angelic interpretation of nondeterminism, since if a context holding the function terminates, it will have in the process of computation only fed the function a finite number of arguments. As such, in any context, there is always a large enough approximation of the identity which cannot be distinguished from the identity function. This outline argument that $M\equiv_{\text{ctxt}}\textbf{return}(\textit{id})$ can be made precise along the lines of Lassen [19, Example 6.4.4].

However, $M$ and $\textbf{return}(\textit{id})$ are distinguished by the positive logic, since $M$ cannot return the identity function itself. Specifically, the formula $\Diamond(\bigwedge_{n\in\mathbb{N}}\overline{n}\mapsto\Diamond(\{n\}))$ is satisfied by $\textbf{return}(\textit{id})$ but not by $M$. Thus $M\not\equiv_{\mathcal{V}^{+}}\textbf{return}(\textit{id})$.

It is an interesting question whether our modal behavioural logic can be used to better understand the relationship between applicative (bi)similarity and contextual equivalence/preorder. For example, in the case of effects for which the relations differ (such as nondeterminism), can the logic be restricted to characterise contextual equivalence/preorder?

8 Pure behavioural logic

In this section, we 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 [42]. Formulas ($\phi$ and $\Phi$) express properties of individual programs, through satisfaction relations ($V\models\phi$ and $M\models\Phi$). 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\Psi)$ at function type, which mentions the programming language value $V$.

This issue can be addressed, by replacing the basic value formula $(V\mapsto\Psi)$ with the alternative $(\phi\mapsto\Psi)$, already mentioned in Section 3. Such a change also has a practical motivation. The formula $(\phi\mapsto\Psi)$ declares a precondition and postcondition for function application, supporting a useful specification style. It also supports the expression of various other properties that are natural from the point of view of program specification. For example, using negation, we can define the dual formula $\neg(\phi\mapsto\neg\Phi)$, with the resulting semantics111111Given compatibility of $\sqsubseteq_{\mathcal{V}^{+}}$, this formula is equivalent to $\bigvee_{\{V\mid V\models\phi\}}\chi_{V}\mapsto\Psi$, where $\chi_{V}$ is from Lemma 5.5. As such, it may also be formulated without the use of negation in the positive behavioural logic $\mathcal{V}^{+}$.:

[TABLE]

Further examples of the usefulness of the pure behavioural logic will be given in Section 9.

Definition 8.1**.**

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

[TABLE]

The semantics is modified by defining $W\models(\phi\mapsto\Psi)$ using formula (2) of Section 3.

[TABLE]

With the definition of $(\phi\mapsto\Psi)$ within $\mathcal{V}$, given in (1) of Section 3, we can see $\mathcal{F}$ as a fragment of $\mathcal{V}$ (and $\mathcal{F}^{+}$ a fragment of $\mathcal{V}^{+}$), resulting in the following fact.

Lemma 8.2**.**

Any formula of  $\mathcal{F}$ and  $\mathcal{F}^{+}$ is equivalent to some formula of  $\mathcal{V}$ and  $\mathcal{V}^{+}$ respectively.

Moreover, once we have established compatibility, we have the following result.

Proposition 8.3**.**

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 logics $\mathcal{V}^{+}$ and $\mathcal{F}^{+}$ are equi-expressive.

Proof.

Lemma 8.2 tells us we can translate any formula from $\mathcal{F}$ into an equivalent formula from $\mathcal{V}$. For the reverse translation, whose correctness proof is more interesting, we give more detail. Every value (respectively computation) formula, $\phi$ (respectively $\Phi$), of $\mathcal{V}$ is inductively translated to a corresponding formula $\widehat{\phi}$ (respectively $\widehat{\Phi}$) of $\mathcal{F}$. We do this by induction on the structure of the formula, where we define the following translation:

[TABLE]

where, in the last case, $\psi_{V}$ is the formula $\chi_{V}^{\mathcal{F}}$ from Lemma 5.5. Hence: $V\models_{\mathcal{F}}\psi_{V}$; and, for any $\psi$, if $V\models_{\mathcal{F}}\psi$ then $\psi_{V}\to\psi$ (meaning that $V^{\prime}\models_{\mathcal{F}}\psi_{V}$ implies $V^{\prime}\models_{\mathcal{F}}\psi$, for all $V^{\prime}$).

One now proves, by induction on types, followed by an induction on formulas $\phi$ (or $\Phi$) of this type, that the $\mathcal{F}$-semantics of $\widehat{\phi}$ (resp. $\widehat{\Phi}$) coincides with the $\mathcal{V}$-semantics of ${\phi}$ (resp. ${\Phi}$). This induction is obvious in all cases except for formula $\widehat{(V\mapsto\Phi)}$ of a function type, for which we need to show that: $W\models_{\mathcal{F}}\psi_{V}\,\mapsto\,\widehat{\Phi}$ if and only if $WV\models_{\mathcal{F}}\widehat{\Phi}$.

For the interesting right-to-left implication, suppose that $WV\models_{\mathcal{F}}\widehat{\Phi}$, and consider any $V^{\prime}$ satisfying $V^{\prime}\models_{\mathcal{F}}\psi_{V}$. By the induction hypothesis, using the defining property of $\psi_{V}$, we have that $V^{\prime}\equiv_{\mathcal{V}}V$. It then follows from the compatibility of $\equiv_{\mathcal{V}}$ that $WV^{\prime}\equiv_{\mathcal{V}}WV$, whence $WV^{\prime}\equiv_{\mathcal{F}}WV$, again by the induction hypothesis. Thus it follows from $WV\models_{\mathcal{F}}\widehat{\Phi}$ that $WV^{\prime}\models_{\mathcal{F}}\widehat{\Phi}$, as required.

The proof in the case of the positive logics is similar. ∎

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

Corollary 8.4**.**

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}}$, $\sqsubseteq_{\mathcal{F}^{+}}$, and $\equiv_{\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, it is the presence of general recursion in the programming language (via the fix operator) that has thwarted attempts to give direct proofs of compatibility for the pure-logic-induced preorder and equivalence.

9 Reasoning with the logic

The behavioural logics considered in this paper are designed for the purpose of formalising 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. Furthermore, practical idioms for expressing effect-related properties can also be translated into logical combinations of modal formulas.

We illustrate this last point, by showing how Hoare triples, the standard formalism for specifying programs with global store, compile into our propositional logic with $(s\rightarrowtail s^{\prime})$ modalities, for the language with lookup and update operations (Example 4). Take for example the statement $\{l=z\}M\{l^{\prime}=z!\}$, where $l,l^{\prime}\in L$ are two locations, and $z$ is an auxiliary variable ranging over the natural numbers, and $M$ is a unit-type computation term. This statement asserts that after executing $M$, the location $l^{\prime}$ will contain the factorial of whatever number was stored at $l$ before starting the computation. In the case of the total-correctness version of Hoare logic, in which $M$ is required to terminate, the property stated by the Hoare triple is equivalent to:121212For $P(x)$ some property on $X$, we write $\bigvee_{a\in X,P(a)}\phi_{a}$ for $\bigvee\{\phi_{a}\mid a\in X,P(a)\}$. If the predicate is always true, we write $\bigvee_{a\in X}\phi_{a}$. We use a similar notation for $\bigwedge$.

[TABLE]

where the formula on the right expresses the combined effect of the precondition and postcondition. Similarly, the partial correctness interpretation, under which termination is not guaranteed, is captured by:

[TABLE]

Such compilations of high-level formulas (for example, Hoare triples) into low-level formulas (the infinitary propositional modal logic) are cumbersome. Nevertheless, they serve two purposes. The first is that translatability into the infinitary logic serves as a test for any proposed high-level specification syntax, as the existence of such a translation guarantees that the syntax expresses only behaviourally meaningful properties. The second purpose is that the propositional modal logic can potentially serve as a guideline for the extraction of compositional proof rules for the high-level logic. This is based on an interesting fact: such compositional proof rules are available for the infinitary propositional modal logic itself. Interestingly, this property is intimately related to the notion of strong decomposability defined in Section 4. We now expand on this point.

We consider a format for a style of compositional proof rule for programs whose outermost constructor is a sequential composition: $\textbf{let }M\Rightarrow x\textbf{ in }N\,$. The proof rule we consider is specified by a modality $o\in\mathcal{O}$ together with a family of pairs of modalities: $\{(o_{i},o^{\prime}_{i})\}_{i\in I}\,$. This data determines the let proof rule below, which makes use of the pure behavioural logic $\mathcal{F}$ from Section 8.

[TABLE]

In this rule, the modalities $o$, $o_{i}$ and $o^{\prime}_{i}$ and their index set $I$ have been determined by the specifying data. The other components of the rule may be instantiated arbitrarily, thus the rule is parametric with respect to terms $M$ and $N$ and the formulas $\phi$, $\phi_{i}$ and $\psi_{i}$. The rule is compositional in the sense that its premises require properties to be established of $M$ and $N$ separately.

Definition 9.1**.**

A let proof rule (6) is said to be sound if, for all types $\rho,\,\tau$, computation terms $\vdash M\colon\rho$ and $x\colon\rho\vdash N\colon\tau$, and value formulas $\phi\in\textit{VF}(\tau)$ and $\{\psi_{i}\in\textit{VF}(\rho)\}_{i\in I}$, the following implication holds:

[TABLE]

The modalities $o$ and $\{(o_{i},o^{\prime}_{i})\}_{i\in I}\,$ required to specify a let proof rule are reminiscent of the definition of strong decomposability 4.18. In fact, there is a precise connection. Whenever $\mathcal{O}$ is a strongly decomposable set of Scott open modalities, the set of sound let proof rules is complete in the sense of the proposition below, which informally states that every true modal property of a let term can be proved from properties of its component terms by means of a suitably chosen sound let proof rule.

Proposition 9.2**.**

Suppose that $\mathcal{O}$ is a strongly decomposable set of Scott open modalities. Suppose also that $\textbf{let }M^{\prime}\Rightarrow x\textbf{ in }N^{\prime}\models o\,\phi^{\prime}$ holds (where $\vdash M^{\prime}\colon\rho^{\prime}$ and $x\colon\rho^{\prime}\vdash N^{\prime}\colon\tau^{\prime}$). Then there is a sound let proof rule (6) for $o$, with premise modalities $\{(o_{i},o^{\prime}_{i})\}_{i\in I}\,$, such that

[TABLE]

for some choice of value formulas $\{\psi^{\prime}_{i}\in\textit{VF}(\rho^{\prime})\}_{i\in I}\,$.

Proof.

Assume that $\mathcal{O}$ is strongly decomposable and $\textbf{let }M^{\prime}\Rightarrow x\textbf{ in }N^{\prime}\models o\,\phi^{\prime}$. By the operational semantics, $|\textbf{let }M^{\prime}\Rightarrow x\textbf{ in }N^{\prime}|=\mu(|M^{\prime}|[V\mapsto|N^{\prime}[V/x]|])$, so

[TABLE]

By strong decomposability, there is a collection $\{(o_{i},o^{\prime}_{i})\}_{i\in I}$ of pairs of modalities such that: (1) $\forall i\in I,|M^{\prime}|[V\mapsto|N^{\prime}[V/x]|[\models\phi^{\prime}]]\in o_{i}(o^{\prime}_{i}(\{\ast\}))$, and (2) $\forall r\in TT\mathbf{1}$, if $\forall i\in I,r\in o_{i}(o^{\prime}_{i}(\{\ast\}))$ then $\mu r\in o(\{\ast\})$. We prove that this collection $\{(o_{i},o^{\prime}_{i})\}_{i\in I}$ specifies the desired let proof rule for $o$.

Soundness: To prove that the proof rule is sound, consider types $\rho$ and $\tau$, terms $\vdash M\colon\rho$ and $x\colon\rho\vdash N\colon\tau$, and value formulas $\phi\in\textit{VF}(\tau)$ and $\{\psi_{i}\in\textit{VF}(\rho)\}_{i\in I}$ such that:

[TABLE]

Let $r=|M|[V\mapsto|N[V/x]|[\models\phi]]\in TT\mathbf{1}$. For any $i\in I$ and $V$ such that $V\models\psi_{i}$, we have $|N[V/x]|[\models\phi]\in o^{\prime}_{i}(\{\ast\})$. We have by monotonicity and because $|M|[\models\psi_{i}]\in o_{i}(\{\ast\})$, that $r\in o_{i}(o^{\prime}_{i}(\{\ast\}))\,$. This holds for all $i\in I$, so by property (2) of strong decomposability (given above), $\mu r\in o(\{\ast\})$, hence $|\textbf{let }M\Rightarrow x\textbf{ in }N|[\models\phi]\in o(\{\ast\})$ and we conclude that $\textbf{let }M\Rightarrow x\textbf{ in }N\models o\,\phi$.

Completeness: We now prove that suitable value formulas $\{\psi^{\prime}_{i}\in\textit{VF}(\rho^{\prime})\}_{i\in I}\,$ exist, allowing us to use the rule as a method for proving that $\textbf{let }M^{\prime}\Rightarrow x\textbf{ in }N^{\prime}\models o\,\phi^{\prime}$. For any $i\in I$, define

[TABLE]

where $\chi_{V}$ is the characteristic function for $V$, as given by Lemma 5.5, but translated into the pure logic $\mathcal{F}$ using Proposition 8.3. So if $W\models\chi_{V}$ then $V\sqsubseteq_{\mathcal{V}}W$, and since $N^{\prime}[V/x]\models o^{\prime}_{i}\,\phi^{\prime}$ and $\sqsubseteq_{\mathcal{V}}$ is compatible, $N^{\prime}[W/x]\models o^{\prime}_{i}\,\phi^{\prime}$. Hence, whenever $W\models\psi^{\prime}_{i}$, we have that $N^{\prime}[W/x]\models o^{\prime}_{i}\,\phi^{\prime}$, so $\lambda x\colon\rho^{\prime}.\,N\models\psi^{\prime}_{i}\mapsto o^{\prime}_{i}\,\phi^{\prime}$.

By the definition of $\psi^{\prime}_{i}$ and the observation above, it holds that, for any closed value term $W\colon\rho^{\prime}$, $W\models\psi$ if and only if $|N^{\prime}[W/x]|[\models\phi^{\prime}]\in o^{\prime}_{i}(\{\ast\})$. By property (1) above of strong decomposability, $|M^{\prime}|[V\mapsto|N^{\prime}[V/x]|[\models\phi^{\prime}]]\in o_{i}(o^{\prime}_{i}(\{\ast\}))$, so $|M^{\prime}|[\models\psi^{\prime}]\in o_{i}(\{\ast\})$, and hence $M^{\prime}\models o_{i}(\psi^{\prime})$. ∎

We remark that Proposition 9.2 also works if we restrict to the logic $\mathcal{F}^{+}$ of positive pure formulas.

We illustrate Proposition 9.2, by giving examples of complete collections of sound let proof rules in the case of two of our example effects: global store, and probabilistic choice. For global store, such a collection is given by let proof rules of the form:

[TABLE]

For probabilistic choice, such a collection of rules is:

[TABLE]

where each rule in the collection is specified by some $n\geq 1$ and rationals $0<a_{0}<\dots<a_{n}<1$ and $1>b_{0}>\dots>b_{n}>0$ satisfying $a_{0}b_{0}+\sum_{i=1}^{n}(a_{i}-a_{i-1})b_{i}\geq q\,$. Completeness can be derived from Proposition 9.2, using the fact that such collections $\{(\mathsf{P}_{>a_{i}},\mathsf{P}_{>b_{i}})\}_{i=1}^{n}$ arise in the proof of strong decomposability for the probability modalities in Section 4.

The above discussion concerns compositional proof rules for the let construction of the programming language. Compositional proof rules are available for the other program constructors too. For example, it turns out to be a consequence of Proposition 9.2 that compositional proof rules are available for the algebraic effect operations. Indeed such rules can be derived from the let proof rules by recasting the effect operations in terms of their generic effects in the sense of Plotkin and Power [38]; for example for a binary operation:

[TABLE]

Carrying this out in full generality would be excessively technical for this late point in the paper. So instead we illustrate the end result by giving examples of the proof rules one obtains for a selection of the effect operations in our running examples.

In the case of nondeterminism, the only effect operation is nondeterministic choice. For this, one obtains separate rules for the $\Diamond$ and $\Box$ modalities.

[TABLE]

For a second example, in the case of global store, one obtains the following rules for the $\textit{lookup}_{l}$ and $\textit{update}_{l}$ operations.

[TABLE]

In all cases the rules are sound as expected, and also complete in the following sense. Every valid assertion stating that a program whose outermost constructor is an effect operation satisfies a modal property can be derived by one of the compositional proof rules. For example, if it is true that $\textit{update}_{l}(V;M)\models(s\rightarrowtail s^{\prime})\,\phi$ then there exists $n$ such that $V\models\{n\}$ and $M\models(s[l:=n]\rightarrowtail s^{\prime})\,\phi$. (Indeed, let $n$ be such that $V$ is is the numeral $\overline{n}$.)

There is much that is preliminary in the above account of compositional reasoning principles. As we have already discussed, for reasoning to be practical one needs an expressive finitary program logic, and one needs the compositional principles in the proof rules to also be expressible using the finitary language. For example, in the case of global store, one would not use low-level modalities of the form $(s\rightarrowtail s^{\prime})$ where $s,s^{\prime}$ are individual states, but rather of the form $(P\rightarrowtail Q)$ where $P$ and $Q$ are formulas in an appropriate logic for expressing general preconditions and postconditions constraining states. Also, one would reformulate the proof rules above to directly deal with such a practical language for preconditions and postconditions. Nonetheless, the general point remains that such more practical constructions can be compiled down into our infinitary propositional logic and its primitive modalities. In the end, in the case of global store, one will end up with a logic looking very much like an extension of Hoare logic to a higher-order language (e.g., there will be some similarities with Hoare Type Theory [29]).

Another issue we have not addressed in the discussion above is that, in general, the verification of interesting programs will involve proving properties of open terms (with free variables) rather than just the closed terms considered above. For this reason, one needs a proof system that deals with sequents of the form

[TABLE]

where we write $V{\,::\,}\phi$ and $M{\,::\,}\Phi$ as syntactic assertions representing the statements $V\models\phi$ and $M\models\Phi$. The sequents above state that properties $\psi$ and $\Psi$ hold of $V$ and $M$, conditional on properties $\phi_{1},\dots,\phi_{n}$ of the free variables. For example, with such sequents, there is then a natural proof rule for $\lambda$-abstraction:

[TABLE]

Summarising the above considerations, while the infinitary modal propositional logic of the present paper is not itself a practical vehicle for specification and verification, it may potentially inform the design of expressive finitary logics suitable for practical specification and reasoning with effects. In this regard, the compositional rules for the infinitary logic may provide templates for such rules in the practical logics. Moreover, the propositional logic suggests a general sequent-based format for verification, whose mature realisation should be something like an expressive refinement-type system for algebraic effects, supporting compositional verification. The development of such a system is a goal for future research.

The discussion thus far has concerned reasoning to establish assertions of the form $M\models\Phi$ stating that an individual program satisfies a property of programs. Another important side of reasoning is establishing equivalences $M\equiv N$ between programs. Although a main motivation for introducing the behavioural logic was as a means for defining equivalence between programs, we do not primarily view it as a tool for establishing or reasoning about equivalences. Indeed, in regard to equivalences, the logic is most easily used as a means for establishing non-equivalences between programs. In order to show that $M\not\equiv N$, one just needs to exhibit a property $\Phi$ that is satisfied by one of $M,N$ but not the other. Examples of such arguments were given in Examples 7.1 and 7.3. Using the logic as a means for proving that two terms are equivalent is trickier since it requires showing that the terms satisfy the same set of logical formulas. Again, one example of such an argument has been given in Example 7.1, where two terms were shown to be equivalent with respect to mutual similarity, by showing that they satisfy the same positive formulas. We now give one further example of such an argument, as a means of illustrating a general point.

The general point is that the logical properties of programs, as captured by the modalities and their interaction with the effect operations, suffice to establish the usual equalities between algebraic terms comprising of effect operations, which are central to Plotkin and Power’s approach to algebraic effects [38]. For the present paper, we illustrate this using one of the equations for global store as an example. For any value term $\emptyset\vdash\lambda x\colon\!\mathbf{N}.\,M:\mathbf{N}\to\tau$, we prove the following equivalence between computation terms of type $\tau$:

[TABLE]

By Lemma 4.4, we need only check that both sides of the equation satisfy the same formulas of the form $(s\rightarrowtail s^{\prime})\,\phi\,$. To show this, we argue using the proof principles discussed above for the $\textit{lookup}_{l}$ and $\textit{update}_{l}$ operations.

[TABLE]

The above derivation and others like it illustrate an alternative to taking equations between algebraic terms as the basic data defining the behaviour of algebraic effects, which is the mainstream approach in the theory of algebraic effects. Instead one can take the modal behavioural properties of effects and their associated proof principles as primitive, and then derive the equations. Indeed the latter is the natural approach if one views the equations as expressing empirical truths about computational behaviour rather than as a priori axiomatic facts.

10 Discussion and related work

In this paper we have introduced an infinitary propositional logic for expressing properties of programs with algebraic effects, with the principal aim of using the logic to define behavioural equivalence for effectful programs. Although our logics exhibit certain similarities in form with the endogenous logic developed in Abramsky’s domain theory in logical form [3], our motivation and approach are 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 for defining behavioural equivalence.

In the literature, logics for effects have primarily been considered for the purpose of reasoning about programs with effects. We review the main approaches to such logics.

Pitts’ evaluation logic was an early logic for general computational effects [34]. Evaluation logic has built-in $\Box$ and $\Diamond$ modalities, which can be given natural interpretations for some effects, but whose interpretation in the case of other effects is rather forced. In the light of the general theory of modalities in the present paper, it would be natural to reconsider evaluation logic with the built-in $\Box$ and $\Diamond$ modalities replaced with effect-specific modalities, as in Section 3. It is left for future work to assess the extent to which this provides a useful basis for a program logic for effects.

The logic for algebraic effects, of Plotkin and Pretnar [40], axiomatises effectful behaviour by means of an equational theory over a signature of effect operations, following the algebraic approach to effects advocated by Plotkin and Power [39]. Although we also have effect operations in the present paper, we do not take equational axioms as primitive. Instead, it is the choice of the set $\mathcal{O}$ of modalities that determines the equational properties that the effect operations satisfy, as discussed in Section 9. A different kind of modality is also present in the logic of Plotkin and Pretnar [40]. Their operation modalities are generated by the signature $\Sigma$, with each modality being associated with a single effect operation. It is our view that the behavioural modalities of the present paper provide a more natural vocabulary for specifying and reasoning about program behaviour, as discussed in Section 9. It is possible that a reformulation of Plotkin and Pretnar’s logic for algebraic effects, using behavioural modalities instead of operation modalities, might provide a more usable framework for specification and verification of programs with algebraic effects.

A different approach to logics for effects has been proposed by Goncharov, Mossakowski and Schröder [28, 6]. 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 to be as adaptable across as wide a range of effects as the approach of the present paper.

The $F^{*}$ project [47] takes a complementary approach to reasoning about effects, under which an effectful programming language is embedded within a powerful general purpose theorem proving environment based on dependent type theory. The framework supports a generalisation of Hoare-logic-style reasoning, based on preconditions and postconditions, which is applicable to those effects that can be given associated Dijkstra monads [48, 47, 4, 25]. Indeed, an underlying philosophy of the $F^{*}$ project is to identify, for each eligible effect, the relevant form of precondition, postcondition and composition principle related to them. In contrast, in the logic of the present paper, the precondition-postcondition style arises naturally for global store, as it is built into the format of the store modality $(s\rightarrowtail s^{\prime})$; whereas other modalities provide different specification formats that nonetheless support compositional proof methods, as discussed in Section 9. In principle, this latter view is more general, as there is no a priori reason to force specifications into a precondition-postcondition format. In particular, for effects, such as input/output, in which there is observable mid-execution behaviour, it is not clear that such a format is the most useful (although it can be achieved; see, for example Penninckx et al. [32] and Maillard et al. [24]).

Examples in Sections 7 and 9 show how our logic can be used directly for reasoning about program equivalence. Its main practical use in this regard is as a method of establishing non-equivalence: the non-equivalence of $M$ and $N$ can be shown by exhibiting a single logical property that distinguishes between them. In this regard, there is a useful complementarity underpinning the coincidence of logical equivalence and bisimilarity. For, in contrast, a principal virtue of bisimilarity is that it provides practical reasoning techniques for establishing equivalences between programs that do hold. (Such techniques include exhibiting bisimilarities and ‘up-to’ methods [43, 45].) The relationship with other techniques for reasoning about equivalences between applicative and effectful programs, such as logical relations [33, 35, 5, 14, 15, 10], which are often directed towards contextual equivalence, is a question for future investigation.

In addition to the question of reasoning about equivalences and non-equivalences, the formulation of our logic as a language of formulas expressing behavioural properties, raises the question of its potential usefulness as a vehicle for reasoning about properties of programs. As discussed in Section 9, we view the infinitary propositional logic of this paper as providing a low-level language, into which practical high-level finitary logics for expressing program properties can potentially be compiled. In order to be sufficiently expressive, such a logic may well incorporate full first-order classical logic (including negation), as well as logical constructs such as the definition of relations as least or greatest fixed points, all of which are translatable into the logic of the present paper. For such an expressive logic, bisimilarity is likely to be the only program equivalence that supports the interchangeability property ($M\models\phi$ and $M\equiv N$ imply $N\models\phi$) discussed in Section 1. We view the development of such high-level logics and their compositional reasoning principles, aimed at practical specification and verification, as a particularly promising topic for future research.

We end the paper with a brief discussion of some of the choices made in the present paper, and of their extensions and limitations. The work in this paper has been carried out for fine-grained call-by-value [22], 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 [20]. Similarly, they can be adapted to other type constructions such as sums, products, recursive types, and polymorphism, all of which will be addressed in the second authors forthcoming PhD thesis. A more challenging direction for development, is to generalise the theory to permit algebraic operations with more general arities than the possibilities allowed in the present paper. Such a generalisation is needed to include effects such as local and/or higher-order store. This is nontrivial at several levels. For example, the notion of effect tree requires nontrivial modification. Also, the relevant notion of bisimilarity (so-called environmental bisimilarity [44, 16]) is much more subtle and probably requires a logic whose formulas express relations rather than properties.

The central notion of modality, in the present paper, was adapted from the notion of observation in Johann et al. [14]. The crucial change is from sets of trees of type $\mathbf{N}$ (observations) to a set of unit-type trees (modalities). This change allows value formulas to be lifted to computation formulas, analogously to predicate lifting in coalgebra (cf., e.g., Jacobs [13]), which is a key characteristic of our modalities. The properties of Scott-openness and decomposability play a similar role in the present paper to the role they play in Johann et al. [14]. However, the notion of decomposability for modalities (Definition 4.15) is substantially more subtle than the corresponding notion for observations in Johann et al. [14].

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. (A related observation appears in Lopez and Simpson [23].) In recent work, the second author has shown that this situation can be rescued by changing to a quantitative logic, with a corresponding notion of quantitative modality [51].

In Hasuo [8], a general framework for quantitative effect-specific modalities is proposed, where modalities are given by structure maps $TA\to A$ for algebras for a monad $T$, with $A$ being an object of (potentially quantitative) truth values. From a semantic perspective, the Scott-open modalities of the present paper can be equivalently described as continuous functions from $T\mathbb{S}\to\mathbb{S}$, where $\mathbb{S}$ is the two element Sierpinski-space domain $\{\bot,\top\}$. In general, they are not, however, algebras for the tree monad $T$. We leave a thorough comparison of the approach of the present paper (and its quantitative generalisation) with the proposed framework of Hasuo [8] for future work.

One topic we have not touched upon in the paper is extending the programming language with handlers, which are powerful control operators associated with algebraic effects [41]. If added to the language in unrestricted form, handlers violate the usual equations associated with algebraic effects. Nevertheless, it is interesting to consider if our modalities can be used, on the one hand, to reason about handlers, and, on the other, to help constrain handlers to ‘safe’ usages that respect the expected program equivalences. For example, various operators from concurrency can be defined using handlers [1, 50], and it would be interesting to see if this allows the usual Hennessy-Milner logic to be subsumed in our setting.

Acknowledgements.

We thank Francesco Gavazzo, Aliaume Lopez and the anonymous conference and journal reviewers for helpful discussions and comments.

Appendix A Howe’s method proof

In this appendix, we give the details that were left out from the Howe’s method proof in Section 6. The results in this appendix are indexed according to whether they were previously stated in Section 6 or are only stated here. Remember the definitions of the Howe closure given in Definition 6.1. We first look at some preliminary results, mostly from Lassen [19].

See 6.2

Proof.

This proof is adapted from [19, Lemma 3.8.2]. We prove the properties separately.

Since $\mathcal{R}$ is reflexive, so is $\mathcal{R}^{\circ}$. Hence $\widehat{\mathcal{R}}^{\bullet}=\widehat{\mathcal{R}}^{\bullet}\textit{id}\subseteq\widehat{\mathcal{R}}^{\bullet}\mathcal{R}^{\circ}=\mathcal{R}^{\bullet}$. 2. 2.

Note that the compatible refinement of a reflexive relation is reflexive (since the compatible refinement rules line up with the typing rules). Hence $\widehat{\mathcal{R}^{\bullet}}$ is reflexive, since $\mathcal{R}^{\bullet}$ is. So $\mathcal{R}^{\circ}=\textit{id}~{}\mathcal{R}^{\circ}\subseteq\widehat{\mathcal{R}^{\bullet}}\mathcal{R}^{\circ}=\mathcal{R}^{\bullet}$. 3. 3.

This requires an induction on the shape of $A$ (which may be a value or a computation). If $\{x\}\vdash A\,\mathcal{R}^{\bullet}\,B$ then by HC or HV we have $\{x\}\vdash A\,\widehat{\mathcal{R}^{\bullet}}\,C$ and $\{x\}\vdash C\,\mathcal{R}^{\circ}\,B$. So we know $C[W]\,\mathcal{R}^{\circ}\,B[W]$. We need to prove, $A[V]\,\widehat{\mathcal{R}^{\bullet}}\,C[W]$. In each of the cases of $A$, $\{x\}\vdash A\,\widehat{\mathcal{R}^{\bullet}}\,C$ is derived from rule Cn for some number $n$. This rule has as its premise some sequence of relations $A_{i}\,\mathcal{R}^{\bullet}\,C_{i}$. By induction hypothesis we have $A_{i}[V]\,\mathcal{R}^{\bullet}\,C_{i}[W]$, this is also trivially true in the base cases $n\in\{1,2\}$ since then the sequence is empty. Using Cn we can then derive that $A[V]\,\widehat{\mathcal{R}^{\bullet}}\,C[W]$. Hence by HV or HC we get $A[V]\,\mathcal{R}^{\bullet}\,B[W]$. One can verify that this argument works for each of the cases of Cn.

∎

We can also say something about composing the Howe closure with the original relation, which by Lemma 5.6 works well with our relator.

Lemma A.1**.**

If  $\mathcal{R}$ is a preorder relation on closed terms, then we have:

If $A\,\mathcal{R}^{\bullet}\,B$ and $B\,\mathcal{R}^{\circ}\,C$, then $A\,\mathcal{R}^{\bullet}\,C$. 2. 2.

For closed terms $M,N,K$ such that $|M|\,\mathcal{O}(\mathcal{R}^{\bullet})\,|N|$ and $|N|\,\mathcal{O}(\mathcal{R})\,|K|$ we have $|M|\,\mathcal{O}(\mathcal{R}^{\bullet})\,|K|$.

Proof.

We proof the properties individually.

We use that $\mathcal{R}$ is transitive, hence $\mathcal{R}^{\circ}$ is transitive meaning $\mathcal{R}^{\circ}\mathcal{R}^{\circ}\subseteq\mathcal{R}^{\circ}$. Hence with $\mathcal{R}^{\bullet}=\widehat{\mathcal{R}}^{\bullet}\mathcal{R}^{\circ}$ we have $\mathcal{R}^{\bullet}\mathcal{R}^{\circ}=(\widehat{\mathcal{R}}^{\bullet}\mathcal{R}^{\circ})\mathcal{R}^{\circ}\subseteq\widehat{\mathcal{R}}^{\bullet}\mathcal{R}^{\circ}=\mathcal{R}^{\bullet}$. 2. 2.

This follows from applying Lemma 5.6 to the previous statement.

∎

Lastly, we prove the result needed to deal with the $\mathcal{O}$-bisimilarity.

See 6.5

Proof.

This proof is taken from [19, Lemma 3.8.2(4)]. Looking at the compatible refinement rules, it is not difficult to see $\widehat{\mathcal{S}^{op}}=\widehat{\mathcal{S}}^{op}$ for any relation $\mathcal{S}$. From Lemma 6.2 we know that $\mathcal{R}^{\circ}\subseteq\mathcal{R}^{\bullet}$, and $\mathcal{R}^{\bullet}$ is compatible hence $\widehat{\mathcal{R}^{\bullet*}}\subseteq\mathcal{R}^{\bullet*}$. So we get that:

[TABLE]

[TABLE]

Hence $\mathcal{R}^{\bullet*op}$ is a solution for $\mathcal{S}$ to the inclusion $\widehat{\mathcal{S}}\mathcal{R}^{\circ}\subseteq\mathcal{S}$. Since $\mathcal{R}^{\bullet}$ is the least solution, we have $\mathcal{R}^{\bullet}\subseteq\mathcal{R}^{\bullet*op}$. So if $A\,\mathcal{R}^{\bullet*}\,B$, then $A=C_{0}\,\mathcal{R}^{\bullet}\,C_{1}\,\mathcal{R}^{\bullet}\dots\mathcal{R}^{\bullet}\,C_{n-1}=B$ for some choice of sequence $\{C_{i}\}_{i\in I}$, so we can derive that $A=C_{0}\,\mathcal{R}^{\bullet*op}\,C_{1}\,\mathcal{R}^{\bullet*op}\,\dots\,\mathcal{R}^{\bullet*op}\,C_{n-1}=B$ meaning $A\,\mathcal{R}^{\bullet*op}\,B$. We conclude that $B\,\mathcal{R}^{\bullet*}\,A$, so $\mathcal{R}^{\bullet*}$ is symmetric. ∎

Now we specifically take $\mathcal{R}$ to be a pre-order $\mathcal{O}$-simulation $\sqsubseteq$. We assume $\mathcal{O}$ to be a decomposable set of Scott open modalities. The lemmas stated before are satisfied, hence we know that $(\sqsubseteq^{\circ})\subseteq(\sqsubseteq^{\bullet})$ by Lemma 6.2. We prove that $\sqsubseteq^{\bullet}$ is an $\mathcal{O}$-simulation, starting with condition 1 of Definition 5.2:

Lemma A.2**.**

If for $V,W:\mathbf{N}$ we have $V\sqsubseteq^{\bullet}W$, then $V=W$.

Proof.

For a value term $V$ of type $\mathbf{N}$, we have that $V=\overline{n}$ for some natural number $n$. Assume $\overline{n}~{}\sqsubseteq^{\bullet}W$, then for some $L$ we have $\overline{n}~{}\widehat{\sqsubseteq^{\bullet}}L$ and $L\sqsubseteq W$. The latter means $L=W$ by property 1 of $\mathcal{O}$-simulations, so $\overline{n}~{}\sqsubseteq^{\bullet}W\Rightarrow\overline{n}~{}\widehat{\sqsubseteq^{\bullet}}W$. If $n=0$ and hence $\overline{n}=Z$, then $\overline{n}~{}\widehat{\sqsubseteq^{\bullet}}W$ must have been derived from C2, so $W=Z=\overline{n}$. As an induction step, we assume $\overline{n}~{}\sqsubseteq^{\bullet}W\Rightarrow\overline{n}=W$ and $\overline{n+1}~{}\sqsubseteq^{\bullet}W^{\prime}$. We derive $S(\overline{n})~{}\widehat{\sqsubseteq^{\bullet}}W^{\prime}$ which must be from C3 hence $W^{\prime}=S(K)$ where $\overline{n}~{}\sqsubseteq^{\bullet}K$. So by assumption $\overline{n}=K$ which means $\overline{n+1}=W^{\prime}$. We can conclude by induction that $V=\overline{n}~{}\sqsubseteq^{\bullet}W\Rightarrow V=W$. ∎

So condition 1 of Definition 5.2 holds. Condition 3 is satisfied by compatibility of $\sqsubseteq^{\bullet}$ (shown in Lemma 6.2), specifically by rule C6 of compatibility. Condition 2 is the most difficult to prove and requires an induction on the reduction relation of terms. In the order of trees, $|M|_{n}\leq|M|_{n+1}$ and $|M|=\bigsqcup_{n}|M|_{n}$. So by the properties in Lemma 5.9 we have:

[TABLE]

Now for the important result, following the techniques used in [17].

See 6.4

Proof.

We do an induction on $n$.

Base case, where $n=0$, which means $|A|_{n}=\bot$. So we have $|A|_{0}=\bot\leq|B|$. By Lemma 6.2 we know $\sqsubseteq^{\bullet}$ is reflexive, so using Lemma 5.9 we get $|A|_{0}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|B|$.

Induction step $(n+1)$. We assume as the Induction Hypothesis that for any two terms $A^{\prime}$ and $B^{\prime}$, if $A^{\prime}\sqsubseteq^{\bullet}B^{\prime}$ and $k\leq n$ we have $|A^{\prime}|_{k}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|B^{\prime}|$. We want to prove $|A|_{n+1}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|B|$.

By HC in Definition 6.1, there is a $C$ such that $A\,\widehat{\sqsubseteq^{\bullet}}\,C$ and $C\sqsubseteq B$. Since $\sqsubseteq$ is an $\mathcal{O}$-simulation, we have $|C|\,\mathcal{O}(\sqsubseteq)\,|B|$. So we aim to prove that $|A|_{n+1}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|C|$ such that by Lemma A.1 we get $|A|_{n+1}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|B|$. To prove this, we do a case distinction on the shape of $A$ to derive: $\forall A,A\,\widehat{\sqsubseteq^{\bullet}}\,C\Rightarrow|A|_{n+1}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|C|$.

$A=\textbf{return}(V):\tau$, we have $|A|_{n+1}=\eta(V)$ and $\textbf{return}(V)\,\widehat{\sqsubseteq^{\bullet}}\,C$. This is only possible from rule C4, meaning $C=\textbf{return}(W)$ and $V\sqsubseteq^{\bullet}W$. By Lemma 5.8 we have $\eta(V)\,\mathcal{O}(\sqsubseteq^{\bullet})\,\eta(W)$, hence $|A|_{n+1}=|\textbf{return}(V)|_{n+1}=\eta(V)\,\mathcal{O}(\sqsubseteq^{\bullet})\,\eta(W)=|\textbf{return}(W)|=|C|$. That concludes this case. 2. 2.

$A=(\lambda x:\tau.M)\,V:\rho$, hence $|A|_{n+1}=|M[V/x]|_{n}$. We have $(\lambda x:\tau.M)\,V\,\widehat{\sqsubseteq^{\bullet}}\,C$ which can only be concluded from C6. Hence $C=WU$ for some value terms $W$ and $U$, with $(\lambda x:\tau.M)\sqsubseteq^{\bullet}W$ and $V\sqsubseteq^{\bullet}U$. Now $(\lambda x:\tau.M)\sqsubseteq^{\bullet}W$ can only be from a combination of rule HV with C5, hence we have $\{x\}\vdash M\sqsubseteq^{\bullet}L$ and $\lambda x:\tau.L\sqsubseteq W$. From $\{x\}\vdash M\sqsubseteq^{\bullet}L$, $V\sqsubseteq^{\bullet}U$ and Lemma 6.2 we get $M[V/x]\sqsubseteq^{\bullet}L[U/x]$, hence by the induction hypothesis, $|M[V/x]|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|L[U/x]|$. Since $\lambda x:\tau.L\sqsubseteq W$, we have $(\lambda x:\tau.L)\,U\sqsubseteq WU=C$, hence with $|(\lambda x:\tau.L)\,U|=|L[U/x]|$ it holds that $|L[U/x]|\,\mathcal{O}(\sqsubseteq)\,|WU|=|C|$, so by Lemma A.1, $|(\lambda x:\tau.M)\,V]|_{n+1}=|M[V/x]|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|C|$. 3. 3.

$A=\textbf{fix}(F):\rho\rightarrow\tau$, we have $\textbf{fix}(F)\,\widehat{\sqsubseteq^{\bullet}}\,C$ which can only be concluded from C7, hence $C=\textbf{fix}(F^{\prime})$ and $F\sqsubseteq^{\bullet}F^{\prime}$. Take $f:(\rho\rightarrow\tau)\rightarrow(\rho\rightarrow\tau)\vdash N:\rho\rightarrow\tau$ to be the following term:

[TABLE]

This value term has been specifically chosen such that $\textbf{fix}(G)$ reduces in one step to $N[G/f]$ for any term $G$, so $|\textbf{fix}(G)|_{n+1}=|N[G/f]|_{n}$. We have $N\sqsubseteq^{\bullet}N$ by reflexivity, hence with $F\sqsubseteq^{\bullet}F^{\prime}$ and Lemma 6.2 we get $N[F]\sqsubseteq^{\bullet}N[F^{\prime}/f]$. Hence $|\textbf{fix}(F)|_{n+1}=|N[F/f]|_{n}\,{\mathcal{O}(\sqsubseteq^{\bullet})}\,|N[F^{\prime}/f]|=|\textbf{fix}(F^{\prime})|=|C|$ by the induction hypothesis. 4. 4.

$A=\textbf{case }V\textbf{ of }\{Z\Rightarrow M;S(x)\Rightarrow N\}:\tau$, then $A\,\widehat{\sqsubseteq^{\bullet}}\,C$ can only be concluded from C8, hence $C=\textbf{case }V^{\prime}\textbf{ of }\{Z\Rightarrow M^{\prime};S(x)\Rightarrow N^{\prime}\}$ for some terms $V^{\prime}$, $M^{\prime}$, and $N^{\prime}$ where $V\sqsubseteq^{\bullet}V^{\prime}$, $M\sqsubseteq^{\bullet}M^{\prime}$, and $\{x\}\vdash N\sqsubseteq^{\bullet}N^{\prime}$. Since $V\sqsubseteq^{\bullet}V^{\prime}$ we have $V=V^{\prime}$ by Lemma A.2. We do a case distinction on $V$.

1. (a)

If $V=Z=V^{\prime}$, then $|A|_{n+1}=|M|_{n}$ by the reduction relation. Using the induction hypothesis on $M\sqsubseteq^{\bullet}M^{\prime}$ we have $|M|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|M^{\prime}|=|\textbf{case }Z\textbf{ of }\{Z\Rightarrow M^{\prime};S(x)\Rightarrow N^{\prime}\}|=|C|$, so we are finished. 2. (b)

If $V=S(W)=V^{\prime}$, then $|A|_{n+1}=|N[W/x]|_{n}$. By $\{x\}\vdash N\sqsubseteq^{\bullet}N^{\prime}$ we have $N[W/x]\sqsubseteq^{\bullet}N^{\prime}[W/x]$ (Lemma 6.2), hence by the induction hypothesis,

$|A|_{n+1}=|N[W/x]|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|N^{\prime}[W/x]|=|C|$. 5. 5.

$A=\textbf{let }M\Rightarrow x\textbf{ in }N:\rho$. Looking at the $\mathbf{let}$-term, one can observe that we have the following upper bound

[TABLE]

The only derivation of $A\,\widehat{\sqsubseteq^{\bullet}}\,C$ is by C9, from which we know that $C=\textbf{let }M^{\prime}\Rightarrow x\textbf{ in }N^{\prime}$ for some terms $M^{\prime}$ and $N^{\prime}$, where $M\sqsubseteq^{\bullet}M^{\prime}$ and $\{x\}\vdash N\sqsubseteq^{\bullet}N^{\prime}$. Using the above observation we know that $|A|_{n+1}\leq|M|_{n}[L\mapsto|N[L/x]|_{n}]$ and $|C|=|M^{\prime}|[L\mapsto|N^{\prime}[L/x]|]$. Using property 1 of Corollary 5.11, we want to prove that $|M|_{n}[L\mapsto|N[L/x]|_{n}]\;\mathcal{O}(\sqsubseteq^{\bullet})\;|M^{\prime}|[L\mapsto|N^{\prime}[L/x]|]$.

Note that for all $L\sqsubseteq^{\bullet}L^{\prime}$ it holds by $\{x\}\vdash N\sqsubseteq^{\bullet}N^{\prime}$ and Lemma 6.2 that $N[L/x]\sqsubseteq^{\bullet}N^{\prime}[L^{\prime}/x]$. Hence by the induction hypothesis: $|N[L/x]|_{n}\;\mathcal{O}(\sqsubseteq^{\bullet})\;|N^{\prime}[L^{\prime}/x]|$. Define function $f,g:\mathit{Val}(\tau)\to T\mathit{Com}(\rho)$ where $f(L):=|N[L/x]|_{n}$ and $g(L^{\prime}):=|N^{\prime}[L^{\prime}/x]|$. We also have by the induction hypothesis on $M\sqsubseteq^{\bullet}M^{\prime}$ that $|M|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|M^{\prime}|$. Take $t=|M|_{n}$ and $r=|M^{\prime}|$. So we can use property 1 of Corollary 5.11 on $f$, $g$, $t$, and $r$ to conclude that $|A|_{n+1}\leq$

[TABLE]

Using a combination of property 1 of Lemma 5.9 to prove $|A|_{n+1}\,\mathcal{O}(\mathit{id})\,t[L\mapsto f(L)]$, and property 2 of Lemma 5.6 we can derive $|A|_{n+1}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|C|$. 6. 6.

$A=\sigma(M_{0},M_{1},\dots,M_{m-1}):\tau$ where $\sigma:\alpha^{m}\rightarrow\alpha$. The statement $A\,\widehat{\sqsubseteq^{\bullet}}\,C$ can only follow from CA, hence $C=\sigma(M_{0}^{\prime},M_{1}^{\prime},\dots,M^{\prime}_{m-1})$ where for all $i$, $M_{i}\sqsubseteq^{\bullet}M_{i}^{\prime}$. By the induction hypothesis, $|M_{i}|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|M_{i}^{\prime}|$, hence $|A|_{n+1}=\sigma\{i\mapsto|M_{i}|_{n}\}\,\mathcal{O}(\sqsubseteq^{\bullet})\,\sigma\{i\mapsto|M_{i}^{\prime}|\}=|C|$ by property 2 of Corollary 5.11. 7. 7.

$A=\sigma(V):\tau$ where $\sigma:\alpha^{\mathbf{N}}\rightarrow\alpha$. The statement $A\,\widehat{\sqsubseteq^{\bullet}}\,C$ follows only from CB, hence $C=\sigma(V^{\prime})$ where $V\sqsubseteq^{\bullet}V^{\prime}$ meaning for any $\overline{m}:\mathbf{N}$ we have $V\overline{m}\sqsubseteq^{\bullet}V^{\prime}\overline{m}$. By the induction hypothesis, $|V\overline{m}|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|V^{\prime}\overline{m}|$, hence $|A|_{n+1}=\sigma\{m\mapsto|V\overline{m}|_{n}\}\,\mathcal{O}(\sqsubseteq^{\bullet})\,\sigma\{m\mapsto|V^{\prime}\overline{m}|\}=|C|$ by property 2 of Corollary 5.11. 8. 8.

$A=\sigma(V,t):\tau$ where either $t=(M_{0},\dots,M_{n-1})$ or $t=W$. Very similar to the previous cases, from either CC or CD we have $C=\sigma(V^{\prime},t^{\prime})$ where $t\sqsubseteq^{\bullet}t^{\prime}$ and $V\sqsubseteq^{\bullet}V^{\prime}$ hence $V=V^{\prime}:\mathbf{N}$ by Lemma A.2. The rest follows by repeating the proof in the previous cases depending on what shape $t$ is.

∎

We can conclude that $M\sqsubseteq^{\bullet}N\Rightarrow|M|_{n}\,\mathcal{O}(\sqsubseteq^{\bullet})\,|N|$ for any $n$. Hence with $|M|=\sqcup_{n}|M|_{n}$ and Lemma 5.9 we can finally conclude $|M|\,\mathcal{O}(\sqsubseteq^{\bullet})\,|N|$. Hence the relation $\sqsubseteq^{\bullet}$ satisfies all conditions of Definition 5.2, resulting in the following proposition.

See 6.3

Proof.

By Lemma A.2, $\sqsubseteq^{\bullet}$ satisfies condition (1) of being an $\mathcal{O}$-simulation. By Lemma 6.4 and $|M|=\sqcup_{n}|M|_{n}$ for any term $M$, it satisfies condition (2). By compatibility it satisfies condition (3). We conclude that $\sqsubseteq^{\bullet}$ is an $\mathcal{O}$-simulation. ∎

The Howe’s method proof is finalised in Section 6 with Theorem 3 A and B and their proofs.