Till Mossakowski

Lutz Schröder

Sergey Goncharov

To appear in Formal Aspects of Computing

Keywords: monads for effects, dynamic logic, observational equivalence, completeness

For a number of programming languages, among them Eiffel, C, Java, and Ruby, Hoare-style logics and dynamic logics have been developed. In these logics, pre-and postconditions are typically formulated using potentially effectful programs. In order to ensure that these pre-and postconditions behave like logical formulae (that is, enjoy some kind of referential transparency), a notion of purity is needed. Here, we introduce a generic framework for reasoning about purity and effects. Effects are modelled abstractly and axiomatically, using Moggi's idea of encapsulation of effects as monads. We introduce a dynamic logic (from which, as usual, a Hoare logic can be derived) whose logical formulae are pure programs in a strong sense. We formulate a set of proof rules for this logic, and prove it to be complete with respect to a categorical semantics. Using dynamic logic, we then develop a relaxed notion of purity which allows for observationally neutral effects such writing on newly allocated memory.

Introduction

Design and programming by contract reduces software errors by providing specifications of Hoare-style pre-and postconditions and invariants along with the program. Originating in the Eiffel language [START_REF] Meyer | Eiffel: The Language[END_REF], this paradigm has become a guiding design principle for a number of languages, including Sather [START_REF] Stephen | The Sather language[END_REF], Lisaac [START_REF] Sonntag | Lisaac: the power of simplicity at work for operating system[END_REF], Nice [START_REF] Bonniot | The Nice user's manual[END_REF], and D [START_REF] Bright | The D programming language[END_REF]. Moreover, for many existing languages, among them C, C++, Java, JavaScript, Scheme, Perl, Python, and Ruby, libraries, preprocessors and other tools have been developed that support programming by contract; for example, the Java modelling language JML comes with extended static analysis [START_REF] Cok | ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system[END_REF] and verification [START_REF] Van Den | The LOOP compiler for java and JML[END_REF] tools. Contracts in a higher-order functional setting are treated in [START_REF] Bruce | Contracts for higher-order functions[END_REF]. Unlike Hoare's original logic [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] and unlike some known formalisations of Hoare-logics in theorem provers like Isabelle and PVS [START_REF] Huisman | Java program verification in higher order logic with PVS and Isabelle[END_REF][START_REF] David Von | Hoare logic for java in isabelle/HOL[END_REF][START_REF] Nipkow | Hoare logics in Isabelle/HOL[END_REF], most of these languages do not have a separate language for expressing pre-and postconditions. Instead, these are expressed in a pure subset of the programming language itself (this idea originates from JML [START_REF] Gary | Preliminary design of JML: A behavioral interface specification language for Java[END_REF]). The restriction to a pure subset is necessary since specifications should not have side-effects; this serves both conceptual clarity and the possibility of run-time testing (which could easily yield wrong results if specifications could change the behaviour of a program).

Purity in this sense is closely related to referential transparency. Informally, pure programs have the following properties.

1. Discardability: Pure computations can be left out from a sequence of computation steps without changing its behaviour; 2. Determinism: Pure programs always return the same value; 3. Interchangeability: Pure programs can be interchanged with each other, that is, the order does not matter.

Of course, these properties depend on a suitable notion of observational equivalence of programs that explains the term "without changing its behaviour". The observational equivalence in turn depends on the specific set of possible operations; for example, allocating a new memory cell and writing a value into it will not be observable in Java, while in C, it can be observed if the integer representation of the memory cell's address is guessed or known by chance and converted from an integer to a pointer, an operation which is not available in Java.

The Hoare logics for the above-mentioned languages, while all following essentially the same style, may vary in subtle but important details. This greatly complicates the study of properties of such logics. Consequently, the goal of this paper is to formalise these notions and provide logical rules for Hoare-style reasoning in a way that abstracts from the details of the particular languages. The abstraction is achieved by encapsulating notions of effect and computation as monads, as originally suggested by Moggi [START_REF] Moggi | Notions of computation and monads[END_REF] and used in the design of the functional programming language Haskell [START_REF] Peyton-Jones | Haskell 98 Language and Libraries -The Revised Report[END_REF] as well as in programming semantics, e.g. for Java [START_REF] Jacobs | Coalgebras and Monads in the Semantics of Java[END_REF]. In earlier work [START_REF] Schröder | Monad-independent Hoare logic in HASCASL[END_REF][START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF], we have developed a dynamic logic for generic side effects whose semantics is defined in terms of monads; in particular, we have given a sound proof calculus for this logic. 1 Here, we extend the proof calculus to a calculus which is strongly complete for the generic part of the calculus and linear sequential programs2 . This setting is sufficient for our treatment of observational purity. Our logic is related to Pitts' evaluation logic [START_REF] Pitts | Evaluation logic[END_REF], which in turn essentially puts the language-specific logic of [START_REF] Boehm | Side effects and aliasing can have simple axiomatic descriptions[END_REF] on a generic basis. Both these logics omit loops, like the restricted logic considered here, but unlike the full logic of [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF].

In more detail, the definition of our dynamic logic is based on a strict notion of purity where the above requirements for referential transparency (discardability, determinism, interchangeability) are postulated to hold as actual equalities. Once we have the logic available, we can define a weaker notion of observational purity where referential transparency holds only up to observational equivalence in the logic. We thus arrive at a practically usable notion of purity, which in particular allows harmless side-effects such as creating and writing on new references. This generic concept of observational purity is related to the programming language specific notion put forward in [START_REF] Naumann | Observational purity and encapsulation[END_REF]. An interesting point here is that as a byproduct of our completeness proof, we obtain the existence of fully abstract categorical models, where observational equalities hold on the nose, and in particular all observationally pure functions are pure in the original strict sense.

Besides the specification and verification of monadic programs, our logic serves also the specification of monads, i.e. notions of side effect and purity. That is, effects may be described in an axiomatic manner, which abstracts away from particular details of the implementation, and moreover allows for loose specifications that deliberately leave open particular design decisions.

This paper is an extended version of [START_REF] Mossakowski | A generic complete dynamic logic for reasoning about purity and effects[END_REF]. It is organised as follows. Sect. 2 recalls Moggi's approach of encapsulating computational effects as monads. Sect. 3 introduces syntax and semantics of monad-based dynamic logic. A suitable proof calculus is provided in Sect. 4, including its soundness proof. The basic logic cannot be directly applied to e.g. Java, because it makes too many distinctions. Hence, Sect. 5 introduces observational equivalence and purity. Sect. 6 provides a completeness proof for the proof calculus, using a fully abstract term model. Sect. 7 concludes the paper.

Monads for Computations

The presence of computational effects, e.g. state, store, exceptions, input, output, non-determinism, or backtracking, substantially complicates reasoning about programs. Dealing with such features has in the past typically required dedicated logics, designed specifically for a particular combination of effects. In seminal work by Moggi [START_REF] Moggi | Notions of computation and monads[END_REF], monads have been established as a unifying framework for modelling computational effects (including in particular all effects mentioned above) in an elegant way.

Intuitively, a monad associates to each type A a type T A of computations of type A; a function with side effects that takes inputs of type A and returns values of type B is, then, just a function of type A → T B. This approach abstracts from particular notions of computation such as store, non-determinism, non-termination etc.; a surprisingly large amount of reasoning can be carried out without commitment to a particular type of side effect. A monad on a given category C can be defined as a Kleisli triple T = (T, η, * ), where T : Ob C → Ob C is a function, the unit η is a family of morphisms η A : A → T A, and * assigns to each morphism f :

A → T B a morphism f * : T A → T B such that η * A = id T A , f * η A = f, and g * f * = (g * f ) * .
This description is equivalent to the more familiar one [START_REF] Lane | Categories for the Working Mathematician[END_REF].

In order to support a language with finitary operations and multi-variable contexts (see below), one needs a further ingredient: a monad is called strong if it is equipped with a natural transformation

t A,B : A × T B → T (A × B)
called strength, subject to certain coherence conditions (see e.g. [START_REF] Moggi | Notions of computation and monads[END_REF]).

Example 2.1 ( [START_REF] Moggi | Notions of computation and monads[END_REF]). Computationally relevant monads on Set (all monads on Set are strong [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF][START_REF] Moggi | Notions of computation and monads[END_REF]) include the following.

1. Stateful computations with non-termination: T A = S →? (A × S), where S is a fixed set of states and →? denotes the partial function type.

2. Non-determinism: T A = P(A), where P is the covariant power set functor.

Exceptions:

T A = A + E, where E is a fixed set of exceptions. 4. a) Interactive input: T A is the smallest fixed point of γ → A + (U → γ), where U is a set of input values. b) Interactive output: T A is the smallest fixed point of γ → A + (U × γ), where U is a set of output values.
5. Non-deterministic stateful computations: T A = (S → P(A × S)), where, again, S is a fixed set of states (here, we can use the total function arrow since the binding operator can treat undefinedness as the empty set of results).

6. These monads can also be combined. E.g. non-deterministic stateful computations are obtained as T A = S → P(A × S). A monad for Java has been defined as follows [START_REF] Jacobs | Coalgebras and Monads in the Semantics of Java[END_REF] JA = S → (A × S + E × S + 1), with S the set of states and E the set of exceptions. A state typically will comprise a stack, a heap, and a heap pointer, that is,

S = V * × (Loc → V ) × Loc × • • •
where V is a set of values and Loc a set of locations. While Java will provide an operation new : J Loc that allocates a new location, C will additionally provide a coercion operation int2loc : Int → Loc (written e.g. as "( * char)" in C, if characters are stored).

Monad-Based Dynamic Logic

In program specification, dynamic logic as introduced in [Pra76] and extended to monadic computations in [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF] has a number of advantages over less expressive formalisms such as Hoare logic, among them the ability to express both partial and total correctness in a natural way and the possibility of reusing a state, say for statements of the nature 'what would happen if'. Here, we examine the infrastructure that is needed in order to develop generic monad-based dynamic logic, and illustrate that this does indeed make sense when instantiated to typical concrete computational monads.

Syntax

We begin by fixing the syntax of monad-based dynamic logic (MDL). Given a set Sort of basic types, the set of types over Sort is generated by

A ::= 1 | Ω | P A | T A | A × A | Sort. Γ £ p : T Ω Γ £ Pp : P Ω (P) Γ £ p : P A Γ £ p : T A Figure 1.
Term language for monad-based dynamic logic

The type T A contains the monadic programs over A; P A is a subtype of T A containing pure programs. The type of Booleans is denoted Ω; consequently, we take P Ω as the type of formulae of monad-based dynamic logic.

A signature Σ = (Sort, F ) consists of a set Sort of basic types and a set F of operation symbols f : A → B, where A and B are types over Sort. Examples of such operation symbols are new : T Loc and int2loc : Int → Loc as explained above. We make the general assumption that the operations in the signature have T -free argument types, more precisely, types containing neither T nor P . The term language over a signature Σ and a context Γ of typed variables is given in Fig. 1. A judgement Γ £ t : A means that in context Γ, term t has type A. The symbol stands for true, ⊥ for false. We let metavariables t etc. range over terms, a and b over (plain) formulae, i.e. terms of type Ω, ϕ, ψ, χ over monadic formulae, i.e. terms of type P Ω, and p, q etc. over programs, i.e. terms whose type is of the form T A. We use ≡ to denote syntactic equality of terms, formulae and contexts. The term ret t is an effectless computation that just returns the value t. In the term do x ← p; q, the variable x is locally bound in q (but not in p), the interpretation being 'perform computation p, bind the result to x, and then perform computation q(x)'. Repeated bindings such as do x 1 ← p 1 , . . . , x n ← p n ; q are somewhat inaccurately denoted in the form do x ← p; q. Term fragments of the form x ← p are called program sequences. The operations fst and snd are the projection functions for binary products. We treat n-ary products as iterated binary products; then projections π n i can easily be defined in terms of fst and snd.

The term forming operation P : T Ω → P Ω is a closure operator. The monadic formula Pp intuitively expresses that all terminating runs of p return . Note that P does not behave like a modal operator; in particular, for ϕ : P Ω, we will have ϕ ⇐⇒ Pϕ. However, P serves to define modalities: For ϕ : P Ω, we let [x ← p] ϕ abbreviate the monadic formula P do x ← p; ϕ, and omit x if it does not occur in ϕ. The monadic formula x ← p ϕ abbreviates ¬[x ← p] ¬ϕ. Both in do-terms and within modal operators, we implicitly identify terms up to α-equivalence.

Besides the specification and verification of monadic programs, MDL serves also the (potentially loose) specification of monads, i.e. notions of side effect.

The running example of [START_REF] Schröder | Monad-independent Hoare logic in HASCASL[END_REF][START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF] involves references and non-determinism; numerous further examples can be found in [START_REF] Walter | Monadic dynamic logic: Application and implementation[END_REF], including the Java monad and a parsing monad, as well as a queue monad over a fixed set U of entries. Here, we present the specification of a monad for dynamic references. It is axiomatised using Hoare triples for total correctness

[ϕ] p [ψ]
by interpreting them as partial correctness plus termination:

ϕ ⇒ ( p ∧ [p] ψ).
The implication ϕ ⇒ p is called the termination part, and the implication ϕ ⇒ [p] ψ is called the partial correctness part of the Hoare triple.

Example 3.1. We assume, for any basic type A, a (basic) type Ref A of references to objects of type A and an equality operation = : A × A → Ω, the latter axiomatised by reflexivity x = x and the substitution schema

(var) [[x 1 : A 1 , . . . , x n : A n £ x i : A i ]] = π n i (app) f : A → B ∈ Σ [[Γ £ t : A]] = h [[Γ £ f (t) : B]] = [[f ]] • h (1) [[Γ £ * : 1]] = ! (pair) [[Γ £ t : A]] = h 1 [[Γ £ u : B]] = h 2 [[Γ £ t, u : A × B]] = h 1 , h 2 (fst) [[Γ £ t : A × B]] = h [[Γ £ fst(t) : A]] = π 1 • h (snd) [[Γ £ t : A × B]] = h [[Γ £ snd(t) : A]] = π 2 • h (do) [[Γ £ p : T A]] = h 1 [[Γ, x : A £ q : T B]] = h 2 [[Γ £ do x ← p; q : T B]] = h * 2 • t [[Γ]],[[A]] • id, h 1 (ret) [[Γ £ t : A]] = h [[Γ £ ret t : P A]] = η [[A]] • h (P) [[Γ £ p : T Ω]] = h [[Γ £ Pp : P Ω]] = P • h (P) [[Γ £ p : P A]] = h [[Γ £ p : T A]] = ι A • h ( ) [[Γ £ : Ω]] = (⊥) [[Γ £ ⊥ : Ω]] = ⊥ (¬) [[Γ £ a : Ω]] = h [[Γ £ ¬a : Ω]] = ¬(h)
similarly for ∧, ∨, ⇒, ⇐⇒ ret (x = y) ⇒ (ϕ ⇔ ϕ[y/x]) for every formula ϕ (schematic axiomatisations are unproblematic in our framework, as we prove strong completeness below). The specification of dynamic references is then as follows.

* : Ref A → P A := : (Ref A) × A → T 1 new : A → T (Ref A) [ ]r := x [x = *r] (read-write) [x = *r] s := y [x = *r ∨ r = s] (read-write-other) [ ] r ← new x [x = *r] (read-new) [x = *r] s ← new y [x = *r ∨ ¬r = s] (read-new-other) [ ] r ← new x; p; s ← new y [¬r = s] (new-distinct)
The operation * reads the value from the location specified by the reference, while := assigns a new value to the location, and new creates a new location. Note that the profile of * ensures that reading is pure. The first axiom expresses that after assignment, the assigned value can be read; the second one that assignment for a particular location does not affect the other locations. The next two axioms state similar properties for the new operation, and the last axiom ensures that two newly created locations are distinct.

Semantics

MDL is interpreted over a strong monad T on a cartesian category C3 with additional structure as follows. There is a distinguished internal Boolean algebra object Ω; note that this is equivalent to hom-sets into Ω coherently carrying a Boolean algebra structure, i.e. the hom-functor hom( , Ω) factoring through Boolean algebras. In order to enforce a Boolean logic, we additionally require that (id

A × : A × 1 → A × Ω, id A × ⊥ : A × 1 → A × Ω
) is an episink. Moreover, T needs to be equipped with a strong submonad P, with functor part P (the inclusion is denoted ι : P → T ); we require that P A consists of pure computations as defined further below. 4 Finally, we need a left inverse P : T Ω → P Ω of the inclusion ι : P Ω → T Ω. It will be axiomatised uniquely later on (cf. Prop. 3.11).

Remark 3.2. In a distributive category, one obtains the Boolean algebra structure by defining Ω as 1 + 1. E.g., every topos is distributive, and in a classical topos, the subobject classifier is just 1 + 1. In a category with equalisers, there is also a canonical choice for the subfunctor P , namely to take P A as the subobject of T A determined by purity as defined below. Then the P arrow is uniquely determined if it exists (see Prop. 3.11 below).

We then interpret the basic sorts as objects in C. This is easily extended to all types, giving an interpretation [[A]] for each type A. Basic operations f : A → B are interpreted as morphisms

[[A]] → [[B]
], and terms x 1 : A 1 , . . . , x n :

A n £ t : A as morphisms [[t]] : [[A 1 × • • • × A n ]] → [[A]
], using the cartesian structure for pairing and projections, the monad for do and ret, and the Boolean algebra structure on Ω for the Boolean connectives as shown in Fig. 2. (Note that there is no particular rule for sequential composition within P : the fact that P is a submonad guarantees closedness under sequential composition). Observe, that logical connectives are also applicable to P Ω. For instance p ∧ q is an alias for (do x ← p; y ← q; ret x ∧ y). The fact that P Ω inherits Boolean algebra structure from Ω strongly relies on the definition of P [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF]. Equations between terms are interpreted as equations between the corresponding morphisms; this will be used in a series of definitions below (we often leave the context implicit).

The following lemma has a straightforward proof:

Lemma 3.3 (Substitution). Let Γ and ∆ ≡ ȳ : B be contexts, let Γ £ t : B, and let ∆ £ s : C. Then [[Γ £ s[ t/ȳ] : C]] = [[∆ £ s : C]] • [[Γ £ t : B]].

Purity

MDL formulae will be interpreted as computations of type P Ω (i.e. morphisms from the object interpreting the context into the object P Ω). They are expected to have no side-effect, although they may e.g. read the state (if a notion of state is present in the monad). We now will abstractly capture the three conditions for purity listed in Sect. 1. The first condition, namely that computations can be left out from a sequence of computation steps without changing its behaviour, is captured as follows:

Definition 3.4. In a monad given as above, a program p :

T A is called discardable [Thi97] if (do y ← p; ret * ) = ret * .
The following properties from [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF] substantiate the claim that discardability actually captures the stated intention: If p is discardable, then (do p; q) = q for each program q. Moreover, if p, q : T 1, then (do q; p) = q.

For the monads described in Example 2.1, discardability of p means:

1. State monad: p possibly reads the state, but does not change it; 2. Non-determinism: p returns at least one value; 3. Exceptions: p terminates normally; 4. In-/Output: p does not read/write; 5. Nondeterministic state monad: p possibly reads the state, but does not change it; 6. Java monad: p only reads the state and terminates normally.

The second condition concerns determinism: pure programs always return the same value. This is captured as follows

: A program p : T A is called copyable [Füh02, Thi97] if (do x ← p; y ← p; ret x, y ) = do x ← p; ret x, x .
Although copyability alone is not of much interest, we detail what copyability of p means in our example monads:

1. State monad: p is idempotent in the sense that applying its state transformation twice is the same as applying it once, and the returned values are the same;

2. Non-determinism: p returns at most one value; 3. Exceptions: p is always copyable;

4. In-/Output: p does not read/write; 5. Nondeterministic state monad: p is idempotent and deterministic; 6. Java monad: p is idempotent.

The third condition is interchangeability: Pure programs can be interchanged with each other, that is, the order does not matter. Hence, p is pure if it is both discardable and copyable, and commutes with all such programs q, that is, (do x ← p; y ← q; ret x, y ) = do y ← q; x ← p; ret x, y .

The last condition follows from the first two for simple monads, on which we focus here; cf. Prop. 4.8.

For the monads described in Example 2.1, purity of p means the expected things:

1. State monad: p possibly reads the state, but does not change it; 2. Non-determinism: p is deterministic, i.e. returns precisely one value; 3. Exceptions: p terminates normally; 4. In-/Output: p does not read/write; 5. Nondeterministic state monad: p is deterministic and only reads the state, but does not change it; 6. Java monad: p only reads the state and terminates normally.

The equation for discardability can be interpreted as a pair of arrows dis 0 , dis 1 : T

[[A]] → T [[1]]; we require that ι [[A]] : P [[A]] → T [[A]] equalises this pair. (We do not require that ι [[A]]
is the equaliser, for the reconstruction of this equaliser in the term model would require a coercion of provably pure terms of type T A to type P A, which means that term formation rules would need to interact with proof rules.) A similar requirement holds for copyability; i.e. we require that P A contains only pure programs.

The Logic

We will want to regard programs that return truth values as monadic formulae with side effects in a modal logic setting. A basic notion we need for such formulae is that of global validity, which we denote explicitly by a 'global box' G : Definition 3.5. Given a term p : T Ω, G p abbreviates the equation p = do p; ret .

If p is discardable, then G p simplifies to p = ret ; otherwise, the equation above ensures that the right hand side has the same side-effect as p. We say that an MDL formula ϕ is valid in a model T, and write T |= ϕ, if G ϕ; this is usually expressed by just writing ϕ. As usual, by T |= Φ for a set Φ of MDL formulae we mean that T |= ϕ for all ϕ ∈ Φ, and by Φ |= ψ that T |= Φ implies T |= ψ for all T.

In our example monads, satisfaction of G ϕ amounts to the following:

• State monad: successful execution of ϕ from any initial state yields ;

• Non-determinism: ϕ yields at most the value (or none at all);

• Exceptions: ϕ yields whenever it terminates normally;

• Input/output: the value eventually produced by ϕ after some combination of inputs is always ;

• Non-deterministic state monad: execution of ϕ from any initial state yields at most the value ;

• Java monad: successful execution of ϕ from any initial state yields whenever it terminates normally.

A related notion is that of global dynamic judgements of the form [ [x ← p] ] a, which intuitively state that a holds after x ← p, where a : Ω is a truth-valued term in variables x. The idea is to work with formulae that have all side effects shoved to the outside, so that the usual logical rules apply to the remaining part. Definition 3.6. Given a program sequence x ← p and a formula a of type Ω, the notation [ [x ← p] ] a abbreviates the equation

(do x ← p; ret x, a ) = do x ← p; ret x, . Definition 3.7. A monad is called simple if G do x ← p; ret a implies [ [x ← p] ] a.
(The converse implication holds universally.) Roughly, an algebraic monad [START_REF] Lane | Categories for the Working Mathematician[END_REF] is simple if, in each of its equations, the two sides contain the same variables. All monads of Example 2.1 are simple. The continuation monad and the abelian group monad are not simple. In the sequel, all monads are assumed to be simple.

We adapt the axiomatic definition of the dynamic modal operators from [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF] to the simplified setting of simple monads: Definition 3.8. T is said to admit dynamic logic, if for each q : T Ω and each x ← p containing x i : Ω,

[ [x ← p; a ← Pq] ] (x i ⇒ a) iff [ [x ← p; a ← q] ] (x i ⇒ a).
This definition essentially axiomatises P via its interaction with global dynamic judgements. In order to gain some intuitive understanding, let us assume that we are working in a non-deterministic state monad. Note that purity of Pq is enforced by its type; this means that in a given state, Pq returns either or ⊥ (but not both -it is deterministic). Hence, the above definition expresses that in any given state (p can be used to move to that state), Pq holds iff all executions of q (starting from the given state) return true.

For the next proposition, it is important to recall the difference between the local box [x ← p] ϕ (a monadic value of type P Ω that may be used in formation of monadic terms) and the global box [ [x ← p] ] a (a global equation between certain monadic terms). Proposition 3.9. If a simple monad T admits dynamic logic, then

[ [x ← p; a ← [ȳ ← q] ϕ] ] (x i ⇒ a) iff [ [x ← p; ȳ ← q; a ← ϕ] ] (x i ⇒ a),
i.e. T admits dynamic logic in the sense of [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF].

Proof. Follows from Def. 3.8 using rules (ctr) and (ctr-) of the calculus of global dynamic judgements in [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF].

Thus, the operator [ȳ ← q] in a sense serves to predict all positive statements to be made about the result ȳ after executing the computations q in a given state; the formal content of the latter phrase is reflected in the quantification over program sequences x ← p to be executed before q.

Example 3.10. All monads described in Example 2.1 admit dynamic logic, with the meaning of the dynamic modal operators made explicit below. A typical example that fails to admit dynamic logic is the continuation monad λX. While at first sight, items 2-4 look uninteresting from the perspective of dynamic logic, it should be kept in mind that all these monads may be combined with 'dynamic' monads such as the state monad, as exemplified for the cases of the non-determinism monad in item 5 and the Java monad in item 6.

(X → R) → R [SM04a].
As stated in Sect. 3.2, P Ω is a Boolean algebra; hence, it is equipped with a partial order. For simple monads, this partial order is given by

ϕ ≤ ψ iff [ [a ← ϕ; b ← ψ] ] (a ⇒ b) Rules: (nec) ϕ [x ← p] ϕ
x not free in assumptions (mp) ϕ ⇒ ψ; ϕ ψ Axioms:

(K) [x ← p] (ϕ ⇒ ψ) ⇒ [x ← p] ϕ ⇒ [x ← p] ψ (seqP) [x ← p; y ← q] ϕ ⇐⇒ [x ← p] [y ← q] ϕ (ctrP) [x ← p; y ← q] ϕ ⇐⇒ [y ← (do x ← p; q)] ϕ (x / ∈ F V (ϕ)) (retP) [x ← ret t] ϕ ⇐⇒ ϕ[t/x] (dis) [x ← p] ψ ⇐⇒ ψ p : P A, x not free in ψ (copy) [x ← p; y ← p] ψ ⇐⇒ [x ← p] ψ[x/y] p : P A (P) [a ← Pp] ret (t ⇒ a) ⇐⇒ [a ← p] ret (t ⇒ a) p : T Ω (unit) [x ← ϕ] ret x ⇐⇒ ϕ (CC) ϕ[t/x] ⇐⇒ ϕ[u/x] for (t = u) ∈ CC (cong⇔) ret (t ⇔ u) ⇒ (ϕ[t/x] ⇐⇒ ϕ[u/x]) (taut)
ret a a : Ω a tautology CC = {fst x, y = x; snd x, y = y; fst(x), snd(x) = x; x : 1 = * } Proposition 3.11. The monadic formula Pp is the greatest monadic formula ϕ : P Ω such that

[ [a ← ϕ; b ← p] ] (a ⇒ b). Proposition 3.12. [ [x ← p] ] a iff G [x ← p]

A Calculus for Dynamic Logic

Figure 3 shows a proof calculus for MDL. The calculus differs from the one in [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF] in that the rules for the diamond are omitted, because in classical logic, Q can be defined as ¬P¬. Moreover, Axioms (P) (resembling the implicit definition of P in the formula for admission of dynamic logic), (dis) and (copy) (expressing purity of terms of type P A), (unit), and the congruence axioms (cong⇔), (cong=) and (CC) have been added. The axiom schema (CC) throws in the standard equations for tupling, projections, and * , i.e. the internal equations of cartesian categories. The usual logical connectives are lifted to P Ω by defining e.g.

ϕ ⇒ ψ := [a ← ϕ; b ← ψ] ret (a ⇒ b) : P Ω,
which by (PMDL) below is equivalent to

do a ← ϕ; b ← ψ; ret (a ⇒ b).
We write Φ ψ if a monadic formula is derivable in the calculus from a set Φ of axioms. Proof. Rules (nec) and (mp) and axioms (K), (seqP), (ctrP), and (retP) are proved to be sound in [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF], which carries over to our definition of admission of dynamic logic by Prop. 3.9 and the observation that the proof in [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF] does not use the partial cartesian closed structure of the category. We now cover the remaining axioms:

Axiom (P): We prove soundness for the special case that t is a variable x; the general case then follows with the substitution lemma 3.3. We prove that ψ ≡ [a ← Pϕ] (x ⇒ a) has the defining property of the right hand side, i.e.

[ [ȳ ← q; b ← ψ] ] (y i ⇒ b) iff [ [ȳ ← q; a ← ϕ; b ← ret (x ⇒ a)] ] (y i ⇒ b).
We calculate

[ [ȳ ← q; b ← [a ← Pϕ] (x ⇒ a)] ] (y i ⇒ b) ⇐⇒ [ [ȳ ← q; a ← Pϕ; b ← ret (x ⇒ a)] ] (y i ⇒ b) ⇐⇒ [ [ȳ ← q; a ← Pϕ] ] (y i ⇒ x ⇒ a) ⇐⇒ [ [ȳ ← q; a ← ϕ] ] (y i ⇒ x ⇒ a) ⇐⇒ [ [ȳ ← q; a ← ϕ; b ← ret (x ⇒ a)] ] (y i ⇒ b),
exploiting that we can use the defining property of P with monadic formulae instead of just variables before the implication sign, and omitting some propositional reasoning. Axiom (unit): By the η-rule for global dynamic judgements [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF],

[ [ȳ ← q; a ← ϕ] ] (y i ⇒ a) iff [ [ȳ ← q; x ← ϕ; a ← ret x] ] (y i ⇒ a),
i.e. ϕ has the defining property of the left hand side [x ← ϕ] ret x. Axiom (CC): immediate from the soundness of CC for cartesian categories.

Axiom (taut): if a is a tautology, then [[Γ £ a : Ω]] = , since hom([[Γ]], Ω) is a Boolean algebra. Thus, [[Γ £ ret a : P Ω]] = η Ω • , i.e. ret a is valid.
Axiom (dis): by the (dis) rule of the calculus for global dynamic judgements in simple monads [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF],

[ [ȳ ← p; a ← ψ] ] (y i ⇒ a) iff [ [ȳ ← p; x ← ϕ; a ← ψ] ] (y i ⇒ a),
i.e. the right hand side has the defining property of the left hand side. Axiom (copy): by the structural rules for pure programs [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF],

[ [ȳ ← p; x ← ϕ; y ← ϕ; a ← ψ] ] (y i ⇒ a) iff [ [ȳ ← p; x ← ϕ; a ← ψ[x/y]] ] (y i ⇒ a).
The left hand side is, by the defining property of [x ← ϕ; y ← ϕ] ψ, equivalent to

[ [ȳ ← p; a ← [x ← ϕ; y ← ϕ] ψ] ] (y i ⇒ a),
i.e. the left hand side of axiom (copy) has the defining property of the right hand side. Axiom (cong⇔): We prove the soundness of the special case ret (x ⇐⇒ y) ⇒ (ϕ ⇐⇒ ϕ[y/x]); soundness of the full (cong⇔) axiom schema then follows with the substitution lemma 3.3. By applying the episink property twice, we obtain that

( 1 × 1 id×h / / 1 × Ω ∼ = Ω × 1 id×k / / Ω × Ω ) h,
(ϕ ⇔ ψ) ⇒ ([x ← ϕ] χ ⇔ [x ← ψ] χ) (Pdef) Pp ⇐⇒ [x ← p] ret x (PMDL) ϕ ⇐⇒ Pϕ (doP) [x ← p] Pq ⇐⇒ P do x ← p; q (K3) ret a =⇒ [p] ret a are derivable.
Proof. (congP): The premise of the implication decodes to

[x ← ϕ; y ← ψ] ret (x ⇔ y),
and the conclusion can be rewritten to

[x ← ϕ; y ← ψ] χ ⇔ [x ← ϕ; y ← ψ] χ[y/x]
using α-equivalence, (seqP), and (dis). Formula (congP) then follows by propositional reasoning with (K) and (cong⇔). Formula (Pdef) follows from axioms (unit) and (P). From (Pdef), we obtain (PMDL), again using (unit).

(doP): [x ← p] Pq is by (seqP) and (unit) equivalent to [x ← p; y ← Pq] ret y, which by (P) is equivalent to [x ← p; y ← q] ret y. By (ctrP), this is equivalent to [y ← (do x ← p; q)] ret y. Again by (P), this is equivalent to [y ← (P do x ← p; q)] ret y, which by (unit) is equivalent to P do x ← p; q.

(K3): By (taut) and (nec), [p; y ← ret a] ret (y ⇒ y). By (ret P), we obtain [x ← ret a; p; y ← ret a] ret (x ⇒ y). By (ctrP) this is equivalent to [x ← ret a; y ← (do p; ret a)] ret (x ⇒ y). Then by (P) we obtain [x ← ret a; y ← [p] ret a] ret (x ⇒ y). By (K) this can be resolved into the implication:

[x ← ret a; y ← [p] ret a] ret x ⇒ [x ← ret a; y ← [p] ret a] ret y.
We will be done once we show that the left-hand side is equivalent to ret a and the right-hand side is equivalent to [p] ret a. Indeed, by (dis) and Proof. Assume that B is T -free. By induction over the term structure of t, we prove that t does not have a subterm of type T A. For the term formation rules (var) and (1), this is clear. For (pair) and the Ω-rules, we can apply the induction hypothesis. Due to the general assumption that the operations in the signature have T -free argument types, for rule (app), we can directly apply the induction hypothesis as well. Concerning (fst) and (snd), if t ≡ g 1 (. . . g n (v)), where g i ∈ {fst, snd} and n is maximal, v must have been obtained either by rule (pair) (but this contradicts the fact that t is in product β-normal form) or by rule (app), and then we can use the reasoning for (app). The remaining rules do not yield a term of T -free type.

(ret P), [x ← ret a; y ← [p] ret a] ret x ⇐⇒ [x ← ret a] ret x ⇐⇒ ret a,
We now discuss some structural properties of the calculus.

Theorem 4.5. The system of reduction rules fst t, u t snd t, u u do x ← ret t; p p[t/x] do x ← (do y ← p; q); r do y ← p; x ← q; r PPp Pp is confluent and strongly normalising.

Proof. Termination. Consider two reduction relations: λ and , the first of which represents one-step reduction by one of the first four reduction rules, and the second one is a one-step reduction by the P-rule. Both these relations are terminating. Termination of the first reduction relation is proved in [START_REF] Benton | Computational types from a logical perspective[END_REF]. Termination of the second reduction relation is trivial, because it decreases the number of boxes.

It is easy to check that the relations and λ have the following interchange property:

if t λ s than t λ . . . s, (1)
where the number of reductions on the right-hand side depends on the chosen rule, the term t, and the redex being rewritten. Now, we prove termination by contradiction. Suppose we have an infinite sequence of reductions t . . .

If there are only finitely many λ reductions in the sequence, then the sequence eventually becomes a non-terminating sequence of reductions, contradiction. Otherwise, we can gather reductions of type λ at the beginning, using property (1). We can thus construct a non-terminating sequence of λ reductions, a contradiction. Confluence. One easily checks that and λ commute, i.e.

if t s and t λ s then there exists r such that s λ r and s . . . r.

Thus, confluence of follows from confluence of and λ by the Hindley-Rosen Lemma [START_REF] Hindley | The Church-Rosser Property and a Result in Combinatory Logic[END_REF].

In the sequel, the terms rewriting and normal form will always refer to the above rule system.

Proposition 4.6. Let ϕ : P Ω be a monadic formula in product β-normal form having a subterm r : T A. Then there is a provably equivalent monadic formula ψ with ϕ * ψ (ψ is even a subformula of ϕ) such that ψ has one of the following forms:

1. x, where x : P Ω is a variable, 2. Px, where x : T Ω is a variable, 3. do x ← p; q, 4. P(do x ← p; q), 5. ret t, where t : Ω, 6. P ret t, where t : Ω.

Proof. We proceed by induction on ϕ. We have the following cases:

1. ϕ is a variable: then we are done. 2. ϕ ≡ f (t), f ∈ Σ. By our general assumption, the type of t is T -free. Hence, by Lemma 4.4, r does not occur in ϕ, a contradiction.

3. ϕ ≡ g 1 (. . . g n (t)), where g i ∈ {fst, snd} and n ≥ 1 is maximal. We have the following subcases:

• t ≡ f (t 1 ). Again, Lemma 4.4 leads to a contradiction.

• t ≡ u, v . This is a contradiction to the fact that ϕ is in product β-normal form.

• t is a variable. For typing reasons, t cannot be r, hence r does not occur in ϕ, a contradiction.

4. ϕ ≡ ret t. If ϕ ≡ r, then we are done. Otherwise r is a subterm of t. But since t : Ω, Lemma 4.4 leads to a contradiction.

5. ϕ ≡ do x ← p; q: then we are done. 6. ϕ ≡ Pq. We basically have the same case distinction for q again, with similar arguments. In the case that q ≡ Pq 0 , we have ϕ ≡ PPq 0 , which by (PMDL) is equivalent to (and can also be reduced to) Pq 0 , hence we can use the induction hypothesis for Pq 0 .

Using this result, we can apply a leftmost-outermost reduction strategy to obtain Proposition 4.7. An MDL formula ϕ is provably equivalent to its normal form.

Proof. Since the rewriting system is confluent and strongly normalising, we can use any strategy to compute the normal form. We always use the CC-rules (justified by axioms (CC)) to compute the CC-normal form between applications of the other rules, which are applied in a leftmost-outermost fashion.

We proceed by induction over ϕ. Assume that ϕ contains any further redex (i.e. not reducible with the CC-rules) p : T A. By Prop. 4.6, we can assume that ϕ is of form do x ← p; q or P do x ← p; q ≡ [x ← p] q -the other possible forms listed in Prop. 4.6 are already in normal form. We can use (seqP), (K) and (nec) to shift the focus among the p i , and reflect the reductions in the calculus with (retP) and (ctrP) -if ϕ is of form do x ← p; q, additionally (PMDL) is needed. Using this outermost rewriting, we eventually arrive at some (possibly boxed) sequence of doterms do ȳ ← q; r such that r is not a do-term. If r contains any redex p : T A, an analysis similar to cases in Prop. 4.6 shows that cases 1. to 4. are not possible. Case 5. already has been excluded, and in case 6. we just apply the induction hypothesis. Similarly, the q i cannot be of the form ret u or do z ← r 1 ; r 2 , since then outermost rewriting of ϕ would not have been completed yet. If q i is a variable or of form f (t), fst(t) or snd(t), using arguments similar to those in Prop. 4.6, we see that no further rewriting is possible. Finally, if q i is of form Pr, with (congP), we can normalise Pr using the induction hypothesis. This result in turn leads to further admissible rules: Proposition 4.8. The following rules are admissible:

(cong) ϕ ⇔ ψ χ[ϕ/x] ⇔ χ[ψ/x] (subst) ϕ ϕ[t/x] .
The following equivalences are derivable:

(comm) [x ← ϕ; y ← ψ] χ ⇐⇒ [y ← ψ; x ← ϕ] χ.
Finally, each lifted tautology ϕ : P Ω can be derived.

Proof. (cong): Occurrences of ϕ outside (but possibly under) boxes [x ← p] can be exchanged for ψ by means of propositional reasoning with (K) and necessitation. Inside boxes, normalise the program according to Prop. 4.7, split the box using (seqP), and then exchange ϕ for ψ by means of (congP).

(subst) can be proved by induction over proofs, noting that these are closed under substitution.

(comm) is proved in a way similar to the proof of Proposition 4.28 in [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF].

Concerning the lifted tautologies, from (taut), the definition of lifted Boolean operations, and (retP), we can derive each lifted propositional tautology a, as follows: the decoding of a can be brought into the form

[x ← ψ] ret t,
where t : Ω is a propositional tautology, using • (PMDL) and (cong) to get rid of nested boxes, • (ctrP) to get rid of nested do's, • (retP) to collect all propositional connectives in t, and • (copy) to remove duplicate occurrences of 'atoms'.

The normalised monadic formula can then be derived using (taut) and (nec).

Example 4.9 (Swap of two variables). We illustrate the usage of the calculus for MDL by proving a simple example about swapping the values of two variables. To that end we make use of the background axiomatisation of dynamic references from Example 3.1. Our goal is to prove that the program (do a ← *r; b ← *s; r := b; s := a) being run under the assumption r = s swaps the values under the references r and s. This is justified by the following derivation:

(x = *r ∧ y = *s ∧ r = s) =⇒ [a ← *r](x = *r ∧ y = *s ∧ r = s ∧ a = x) (step 1) =⇒ [a ← *r; b ← *s](x = *r ∧ y = *s ∧ r = s ∧ a = x ∧ b = y) (step 2) =⇒ [a ← *r; b ← *s; r := b](y = *s ∧ r = s ∧ a = x ∧ b = y ∧ b = *r) (step 3) =⇒ [a ← *r; b ← *s; r := b; s := a](a = x ∧ b = y ∧ b = *r ∧ a = *s) (step 4) =⇒ [a ← *r; b ← *s; r := b; s := a](y = *r ∧ x = *s) (step 5)
Here every step calls a series of axioms. Specifically, steps 1 and 2 essentially follow by (copy) and (comm), steps 3 and 4 call (K3), (read-write), (read-write-other), (taut), (nec) and step 5 essentially follows from the background axiomatisation of the equality predicate. Let us prove step 3 in detail. We have

x = *r ∧ y = *s ∧ r = s ∧ a = x ∧ b = y =⇒ y = *s ∧ r = s ∧ a = x ∧ b = y ∧ [r := b](r = *b) (read-write) =⇒ [r := b](y = *s ∨ s = r) ∧ r = s ∧ a = x ∧ b = y ∧ [r := b](r = *b) (read-write-other) =⇒ [r := b](y = *s ∨ s = r) ∧ [r := b](r = s ∧ a = x ∧ b = y) ∧ [r := b](r = *b) (K3) =⇒ [r := b]((y = *s ∨ s = r) ∧ r = s ∧ a = x ∧ b = y ∧ r = *b) (K), (taut), (nec) =⇒ [r := b](y = *s ∧ r = s ∧ a = x ∧ b = y ∧ r = *b).
(K), (taut), (nec)

After applying (nec) to the obtained implication, we have

[a ← *r; b ← *s](x = *r ∧ y = *s ∧ r = s ∧ a = x ∧ b = y ⇒ [r := b](y = *s ∧ r = s ∧ a = x ∧ b = y ∧ r = *b))
and then we are done by (K).

Observational Purity

Our notion of purity has some practical limitations: The program do r ← new x; ret * is not pure, because it modifies the state. In particular, it is not discardable, since it generally makes a difference whether a new memory cell is allocated or not. However, we generally cannot observe whether a memory cell is allocated (unless we program in C, where a function int2loc, written e.g. as "( * char)" is available). This leads to the following notions: Given a background MDL theory Φ (that axiomatises a given combination of effects), two programs p : T A and q : T A in context Γ = (x 1 : B 1 , . . . , x n : B n ) are observationally equivalent, p ≈ q, iff for all closed program sequences x ← r (where closedness means that every program r i mentions only the previously bound variables x 1 , . . . , x i-1 ) and all monadic formulae ϕ : P Ω in context Γ, y : A,

Φ [x ← r; y ← p] ϕ ⇐⇒ [x ← r; y ← q] ϕ.
(2)

A program is observationally pure if the equations for discardability, copyability and commutation hold up to observational equivalence. For example, in the case of discardability, this means that

Φ [x ← r; y ← (do z ← p; ret * )] ϕ ⇐⇒ [x ← r; y ← ret * ] ϕ, which amounts to Φ [x ← r] ϕ ⇐⇒ [x ← r; p] ϕ.
Deviating from [START_REF] Mossakowski | A generic complete dynamic logic for reasoning about purity and effects[END_REF], in the definition of observational equivalence, we impose the restriction that the equivalence (2) above does not contain free variables. This avoids the possibility of injecting arbitrary semantic values into the formulae, which would make too many things observable. This restriction makes it necessary to introduce an additional context x ← r of closed programs that makes all values obtainable by computations available for observations. Since the notion of observational equivalence depends on the observations that can be made, this also implies that it is dependent on the available operations and hence will vary from programming language to programming language.

This means that we cannot say in detail what observational purity is in our example monads, except from the general statement that a program is observationally pure if it is pure or differs from a pure program only in a way that cannot be observed. We will, however, elaborate some specific cases in more detail.

In particular, the notion of observational purity allows us to distinguish the behaviour of references in Java and in C. We therefore introduce two simple languages, Toy Java and Toy C. Toy Java has been specified in Example 3.1 above (although real-life Java does not have explicit reference types, it does pass every structured object using a reference). Recall that it provides, for any basic type A, a (basic) type Ref A of references to objects of type A, and the following operations:

* : Ref A → P A := : (Ref A) × A → T 1 new : A → T (Ref A)
While Toy Java treats references as an abstract data type that is fully encapsulated, references in Toy C are just integers. Thus, we have exactly the same specification as for Toy Java, except that the profile of the operations is now

* : Int → P A := : Int × a → T 1 new : A → T Int
Example 5.1. Due to the lack of encapsulation of references, writing on a newly allocated reference in Toy C fails to be observationally pure: If we put nwr v = do u ← new v; u := 1; *u then nwr v is not even discardable. To see this, let ϕ be the monadic formula

[z; x ← *n] (x = 1)
where n is some integer literal. Then ϕ[nwr v/z] ⇐⇒ ϕ[ret ()/z] is not provable from the axiomatisation of Toy C, since it fails to be semantically valid: it may or may not happen that the integer n coincides with the newly allocated reference. Note that this effect is excluded in Toy Java, because we cannot write down the corresponding formula: the only way to get hold of a reference in Toy Java is to create it via new , while in the above formula we have just used an integer literal. The following example formalises this point.

Example 5.2. In Toy Java, writing on a newly created reference and subsequently reading from it, i.e. programs such as nwr v = do u ← new v; u := 1; *u are observationally pure. In fact we shall prove that any closed term t : T 1 is observationally equal to ret * (and therefore observationally pure).

(

This implies e.g. observational purity of nwr v, as for closed r : T A and a monadic formula ϕ in context x, y, the axiomatisation of Toy Java allows deriving the following chain of equivalences:

[x ← r; y ← nwr v] ϕ ⇐⇒ [x ← r; u ← new v; u := 1; y ← *u] ϕ ⇐⇒ [x ← r; u ← new v; u := 1; y ← *u] (ret (y = v) ∧ ϕ) (read-write) ⇐⇒ [x ← r; u ← new v; u := 1; y ← *u] ϕ[v/y] (read-write) ⇐⇒ [x ← r; u ← new v; u := 1] ϕ[v/y] (dis) ⇐⇒ [x ← r] ϕ[v/y] (3) ⇐⇒ [x ← r; y ← ret v] ϕ
(with implicit steps for propositional and equational reasoning, the latter supported by the axiomatisation of =) which proves that nwr v is observationally equivalent to ret v, hence observationally pure.

To prove (3), let t : T 1, and let z : T 1 £ ϕ : P Ω; we have to show ϕ[t/z] ⇐⇒ ϕ[ret * /z], as follows. First, using (PMDL), add a box in front of ϕ, if there is none. According to Proposition 4.7 we can assume ϕ to be normal. Moreover, successively replace every subterm in the form P do x ← p; Pq by P do x ← p; q. It is easily seen that this transformation is sound (using (doP)), terminating, and does not spoil normality. In the end ϕ reaches the form P(do x ← p; ret b) or equivalently [x ← p] (ret b). By normality, all the variables in [x ← p] (ret b) are either of basic sorts or of reference sorts, and no projections or pairings occur. Note that b is a boolean combination of equalities (boolean variables are treated as equalities, i.e. b = for b : Ω) and boolean constants. For b = , [x ← p] ret ⇐⇒ ret . For b = ⊥, the equivalence [x ← p] ret ⊥ ⇐⇒ ret ⊥, which expresses termination of the program sequence, may easily be proved by induction, where the base case ('all atomic programs terminate') is directly expressed by the Toy Java axioms. Otherwise b is a boolean combination of equalities. Thus, we are done as soon as we prove the following.

For any variables x i and x j of coincident reference sorts, either [x ← p] ret (x i = x j ) or [x ← p] ret (x i = x j ) is provable, and for every variable x i of base sort there is a closed term q xi such that [x ← p] ret (x i = q xi ) is provable (note that this also gives complete information about equalities among non-closed terms at base type, by substituting q xi for x i and evaluating the resulting closed terms). Moreover, the result of such an evaluation is invariant under exchanging closed subterms of type T 1 in p. We refer to this property briefly as invariance and to the formula x i = x j in question as the target test.

We prove this claim by well-founded induction; a discussion of the actual induction ordering and the relevant cases to be considered will follow further below. If the program sequence p is non-empty (otherwise the statement becomes trivial), consider the last binding in it, say x n ← p n . We distinguish the following cases.

1. p n ≡ Pq. By the induction hypothesis and the fact that Ω is a boolean algebra, either [x 1 ← p 1 ; . . .

; x i-1 ← p i-1 ; x n ← q] ret (x n = ) or [x 1 ← p 1 ; . . . ; x n-1 ← p n-1 ; x n ← q] ret (x n = ⊥)
is provable, and in each case invariance holds. In the former case, [x ← p] ret (x n = ) is provable by (P) and invariance holds.

In the latter case, we have the same situation, except that the implication

[x n ← q] ret (¬x n ) =⇒ [x n ← Pq] ret (¬x n )
, rather than being universally valid, relies on the fact that q terminates as observed above, i.e. that ¬[q] ret ⊥ is derivable. In fact, using termination of q and the K-axiom, we derive from

[x n ← q] ret (¬x n ) that ¬[x n ← q] ret x n .
The latter is, by (unit), equivalent to ¬Pq, which in turn is by its definition equivalent to [x n ← Pq] ret (¬x n ). 2. p n = do y ← s; r. For every b, the monadic formula

[x ← p] ret b, i.e. [x 1 ← p 1 ; . . . ; x i-1 ← p i-1 ; x n ← (do y ← s; r)] ret b, is provably equivalent to [x 1 ← p 1 ; . . . ; x i-1 ← p i-1 ; y ← s; x n ← r] ret
[x n-1 ← new w; x n ← *v] ret (x n = t) ⇐⇒ [x n ← *v] ret (x n = t) (x n-1 = v, (read-new-other)) [x n-1 ← new w; x n ← *x n-1 ] ret (x n = w) ⇐⇒ ret (read-new) [u := w; x n ← *v] ret (x n = t) ⇐⇒ [x n ← *v] ret (x n = t) (v = u, (read-write-other)) [u := w; x n ← *u] ret (x n = w) ⇐⇒ ret (read-write) [x n-1 ← *w; x n ← *v] ret (x n = t) ⇐⇒ [x n ← *v] ret (x n = t) (t closed; (dis))
Otherwise, reduce to the induction hypothesis as in the previous cases.

A few comments about the above induction are needed. First, the induction is indeed well-founded, because every step decreases the number of bindings, boxes, returns, or atomic programs, respectively. Second, the normality of the formula as assumed in the beginning can be partially spoiled, because in case 1, the removal of a box may unblock application of a unit law or associativity. The arising additional cases show up above as cases 2 and 3, which would be unnecessary for a fully normal formula; we may restrict these additional cases to p n : T Ω, as removing boxes is the only source for such terms.

The example may by modified in various ways. For example, if switch to a non-deterministic Java monad and let new non-deterministically return an arbitrary free memory cell (instead of the next free one), nwr remains observationally pure in Toy Java, while in Toy C, it is not even copyable (since the non-determinism can be observed). If we drop the assignment operation from Toy Java, even new becomes pure, because we can no longer observe the allocation of new memory cells.

The example may also be used to illustrate that the notion of observational purity is, unsurprisingly, quite sensitive to modifications of the underlying logic. More to the point, already slight increases in expressiveness may destroy the above proof of observational purity. E.g. if the logic is extended by universal quantification, or even if we just admit free variables in the definition of observational equality, then the above program nwr v fails to be observationally pure in the extended logic. To see this, consider the formula ϕ ≡ z; r ← new x (s = r) with an additional free variable s of reference type besides the placeholder z : T 1. It says that it may happen that after executing z, s is a free reference which might be allocated by the next new statement. Then ϕ[nwr v/z] ⇐⇒ ϕ[ret ()/z] is not provable from the axiomatisation of Toy Java (as it can easily be falsified semantically, for the obvious reason that nwr v allocates a reference). This shows that monadic dynamic logic constitutes a well-balanced environment for observational purity.

Completeness

The completeness proof for MDL is based on a term model construction. Given a signature Σ and a set Φ of MDL formulae over Σ, we construct a category C Σ,Φ as follows: the objects of C Σ,Φ are the types of Σ, and morphisms t : A → B are terms in context

x : A £ t : B, taken modulo contextual equivalence: t ∼ u iff for all MDL formulae ϕ with one free variable x : A,

Φ ϕ[t/x] ⇐⇒ ϕ[u/x] (4)
(this is obviously a congruence). Identities are given by variables [x : A £ x : A] ∼ , and composition by substitution

[y : B £ u : C] ∼ • [x : A £ t : B] ∼ := [x : A £ u[t/y] : C] ∼ .
Using axiom (retP), one easily proves that this is well-defined and obeys the identity and associativity laws of a category. The basic types of Σ are interpreted as themselves, and so are the basic operations:

[[f : A → B]] := [x : A £ f (x) : B] ∼ .
The category C Σ,Φ comes with a canonical cartesian structure, which on objects is just given by taking product types as categorical products, and the unit type as the terminal object. Projections are The problem with contextual equivalence is that, although its definition is simple and intuitive, it can be quite hard to prove that given monadic programs are contextually equivalent. The key result is Theorem 6.1. For terms of type T A, contextual equivalence ∼ coincides with observational equivalence ≈.

π 1 := [x : A × B £ fst(x) : A] ∼ and π 2 := [x : A × B £ snd(x) : B] ∼ , pairing of morphisms is [t] ∼ , [u] ∼ := [ t, u ] ∼ ,
Proof. We first show a lemma on contextual equivalence: Lemma 6.2. For p, q : T A, p ∼ q iff (4) holds for the following cases.

1. ϕ ≡ Px 2. ϕ ≡ P do ȳ ← p; p 0 , and if x occurs freely in p i , then p i ≡ x (i = 0, . . . , n).

Proof. By Prop. 4.7, we can assume that ϕ is in normal form. We proceed by induction on ϕ. If x is not a subterm of ϕ, we are done. If x is a subterm of ϕ, by Prop. 4.6, it suffices to consider four subcases:

• ϕ ≡ x. By (PMDL), we can reach the next case.

• ϕ ≡ Px. Use assumption 1.

• ϕ ≡ do x ← p; p 0 . By (PMDL), we can reach the last case.

• P do x ← p; p 0 . For each p i (i = 0, . . . , n), we have the following subcases, in all of which the premises of assumption 2 are fulfilled:

1. p i is a variable. Then it is immediate that either p i ≡ x, or x does not occur freely in p i . 2. p i ≡ f (t), f ∈ Σ. By our general assumption, the type of t is T -free, and hence by Lemma 4.4, x does not occur freely in p i .

3. p i ≡ g 1 (. . . g n (t)), where g i ∈ {fst, snd} and n ≥ 1 is maximal. As in Prop. 4.6, we can show that x does not occur freely in p i .

4. p i ≡ ret t. For i > 0, this contradicts ϕ being in normal from. For i = 0, it follows that t : Ω, and hence by Lemma 4.4, x does not occur freely in t. 5. p i ≡ Pr. We use the induction hypothesis and (cong) to rewrite p i [t/x] to p i [u/x] within ϕ, and hence get rid of the free occurrences of x in p i .

6. p i ≡ do ȳ ← q; r. This contradicts ϕ being in normal from.

This completes the proof of the lemma. We now return to the Proof of Theorem 6.1. Obviously, contextual equivalence is included in observational equivalence. For the converse, let t ≈ u : T A. By (Pdef), the first assumption of Lemma 6.2 is a special case of the second assumption. The second assumption follows from iterated application of the equivalence (where all terms except from p and q only mention the previously bound variables) for all p, q, ϕ, Φ

[x ← p; x ← p; ȳ ← q] ϕ ⇐⇒ [x ← p; x ← q; ȳ ← q] ϕ (5)
by successively replacing each occurrence of p by an occurrence of q. Now (5) follows from observational equivalence by noting that y ← q can become part of the ϕ. This covers the occurrences of p in p i for i > 0.

For i = 0, we need to show Φ P do ȳ ← p; p ⇐⇒ P do ȳ ← p; q. But this follows from the instance of (5) Φ [ȳ ← p; x ← p] ret x ⇐⇒ [ȳ ← p; x ← q] ret x by rewriting both sides with (unit), (P) and (ctr). Lemma 6.5. In T Σ,Φ , terms are essentially (modulo tupling) interpreted by themselves, that is

[[x 1 : A 1 , . . . , x n : A n £ t : A]] = [x : A 1 × . . . × A n £ t[π n i (x)/x i ] : A] ∼ Proof.
Induction over the term structure. The only interesting case is that of do-terms. Let Γ ≡ x 1 : A 1 ×. . .×x n : A n . Then we have

[[Γ £ do x ← p; q : T B]] = [[Γ, x : A £ q : T B]] * • t [[Γ]],A • id [[Γ]] , [[Γ £ p : T A]] = (induction hypothesis) [z : A 1 × . . . × A n × A £ q[π n+1 i (z)/x i , π n+1 n+1 (z)/x]] * ∼ • [r : (A 1 × . . . × A n ) × T A £ do y ← snd(r); ret fst(r), y ] ∼ • [v : A 1 × . . . × A n £ v, p[π n i (v)/x i ] : (A 1 × . . . × A n ) × T A] ∼ = [s : T (A 1 × . . . × A n × A) £ do x ← s; q[π n+1 i (z)/x i , π n+1 n+1 (z)/x]] ∼ • [do y ← p[π n i (v)/x i ]; ret x, y ] ∼ = [v : A 1 × . . . × A n £ do z ← (do y ← p[π n i (v)/x i ]; ret x, y ); q[π n+1 i (z)/x i , π n+1 n+1 (z)/x] ] ∼ = [v : A 1 × . . . × A n £ (do x ← p; q)[π n i (v)/x i ]
] ∼ where the last steps involve several applications of Theorem 6.1 in connection with various proof rules. Corollary 6.6 (Full abstractness). In T

Σ,Φ , [[t]] = [[u]] iff t ∼ u. Proof. t[π n i (x)/x i ][ x 1 , .
. . , x n /x] ∼ t by axiom (CC). By Theorem 6.1, we also have Corollary 6.7. In T Σ,Φ , for p, q : T A,

[[p]] = [[q]] iff p ≈ q.
The crucial properties of the term model construction are summarised in Proposition 6.8 and Lemma 6.10 below. Proposition 6.8. T Σ,Φ is a fully abstract simple strong monad admitting dynamic logic.

The proof needs the following lemma.

[x ← p; y ← ϕ] ψ ⇐⇒ [x ← p] ((ϕ ⇐⇒ ) ∧ [y ← ϕ] ψ) (seqP, prop. reasoning) ⇐⇒ [x ← p] ((ϕ ⇐⇒ ) ∧ [y ← ret ] ψ) (congP, prop. reasoning) ⇐⇒ [x ← p; y ← ret ] ψ (prop. reasoning, seqP)
Proposition 6.8 By the results of [START_REF] Moggi | Notions of computation and monads[END_REF], it suffices to show the term variants of the monad laws in order to also ensure the coherence axioms for the strength. By Cor. 6.7, we need to show the equations using ≈.

• do x ← p; ret x = p:

By (ctrP), [x ← (do x ← p; ret x)] ψ is equivalent to [x ← p; x ← ret x] ψ. By (retP), this in turn is equivalent to [x ← p] ψ. • do x ← ret y; p = p[y/x]: By (ctrP), [u ← (do x ← ret y; p)] ψ is equivalent to [x ← ret y; u ← p] ψ. By (retP), this is equivalent to [u ← p[y/x]] ψ, noting that x is local to p.
• do y ← (do x ← p; q); r = do x ← p; y ← q; r: This follows easily with (ctrP).

• Simplicity: Let (do x ← p; ret ϕ) = do x ← p; ret . We have to show (do x ← p; ret x, ϕ ) = do x ← p; ret x, , i.e. we have to prove the corresponding observational equivalence. For ψ : P Ω, we have, as a special case of the assumption Φ [a ← (do x ← p; ret ϕ)] a ⇐⇒ [a ← (do x ← p; ret )] a and hence, by (ctrP) and (retP),

Φ [x ← p] ϕ ⇐⇒ [x ← p] ret .
The right hand side of the above equivalence is provable by (nec), so that Φ [x ← p] ϕ. By Lemma 6.9, this finishes the proof of simplicity.

For showing that T Σ,Φ admits dynamic logic, we need to show that

[ [x ← p; a ← Pp] ] x i ⇒ a iff [ [x ← p; a ← p] ] x i ⇒ a
This follows from the following two equivalences:

[ [ȳ ← q; a ← Pp] ] (y i ⇒ a) iff Φ [ȳ ← q] y i ⇒ Pp (6)
[ [ȳ ← q; a ← p] ] (y i ⇒ a) iff Φ [ȳ ← q] y i ⇒ Pp (7) Proof of (6), "⇒": By Cor. 6.7, [ [ȳ ← q; a ← Pp] ] (y i ⇒ a) means that for all ϕ, Φ [ȳ ← q; a ← Pp; x ← ret (y i ⇒ a)] ϕ ⇐⇒ [ȳ ← q; a ← Pp; x ← ret ] ϕ, which by retP is just

Φ [ȳ ← q; a ← Pp] ϕ[y i ⇒ a/x] ⇐⇒ [ȳ ← q; a ← Pp] ϕ[ /x] (8)
By (nec), [ȳ ← q; a ← Pp] , this is the right hand side of (8) for ϕ ≡ ret x. We hence obtain Φ [ȳ ← q; a ← Pp] ret (y i ⇒ a). By (P), the latter is equivalent to Φ [ȳ ← q; a ← p] ret (y i ⇒ a). Using (seqP), (congP) and (taut), we obtain Φ [ȳ ← q] (y i ⇒ [a ← p] ret a). With (Pdef), we obtain Φ [ȳ ← q] (y i ⇒ Pp).

Proof of (6), "⇐": Conversely, assuming Φ [ȳ ← q] (y i ⇒ Pp), by (congP), (taut) and (nec) we get

Φ [ȳ ← q] (y i ⇒ ([a ← Pp] ϕ[y i ⇒ a/x] ⇐⇒ [a ← Pp] ϕ[ /x]).
Also, by (congP), (taut) and (nec),

Φ [ȳ ← q] (¬y i ⇒ ([a ← Pp] ϕ[y i ⇒ a/x] ⇐⇒ [a ← Pp] ϕ[ /x]).
Altogether, with (taut) and (K), we arrive at (8).

Proof of (7), "⇒": [ [a ← p] ] a means (using (retP) again) that for all ϕ, [ȳ ← q; a ← p] ϕ[y i ⇒ a/x] ⇐⇒ [ȳ ← q; a ← p] ϕ[ /x]

We obtain Φ [ȳ ← q] (y i ⇒ Pp) in a similar way as for (6), "⇒", omitting the application of (P). Proof of (7), "⇐": Conversely, assume Φ [ȳ ← q] (y i ⇒ Pp), i.e. by (Pdef), Φ [ȳ ← q] (y i ⇒ [a ← p] ret a). The rest of the argument is similar as for (6), "⇐".

Conclusion and Future Work

Inspired by the logics of design by contract languages, we have introduced monad-based dynamic logic (MDL) as a means of handling with effects, purity and observational equivalence in an abstract way that avoids the development of a specific theory for each language. Our generic notion of observational purity captures the same intuition as Naumann's notion of observational purity [START_REF] Naumann | Observational purity and encapsulation[END_REF] when instantiated to his specific imperative language. However, besides state, store and non-termination, our logic can also handle effects like non-determinism, input/output, and many others. Moreover, our notions of observational and contextual equivalence (which coincide in the term model) come out of the logic in a more natural way, compared with the variety of notions in [START_REF] Naumann | Observational purity and encapsulation[END_REF]. The sound and complete calculus allows for reasoning about Hoare style and dynamic logic assertions as well as about observational purity in a uniform way.

MDL is similar to Pitts' evaluation logic [START_REF] Pitts | Evaluation logic[END_REF], but equipped with a different semantics which is induced directly by the underlying monad -rather than relying on an extra hyperdoctrine structure, which must in all likelihood be considered additional data (e.g. in the case of the state monad, the interpretation of monadic formulae as state predicates is explicitly imposed by the chosen hyperdoctrine). Existing completeness results for monad-based logics rely on a global semantics [START_REF] Moggi | A semantics for evaluation logic[END_REF][START_REF] Goncharov | Completeness of global evaluation logic[END_REF], which e.g. for the state monad means that a sequence of nested modalities leads to universal quantification over all states at each new nesting level -the (implicit) state is not passed across nesting levels. By contrast, our logic allows for reasoning in a truly local way about changes of state. So far, no completeness result has been proved for such logics.

A Hoare calculus has been built on top of MDL [START_REF] Schröder | Monad-independent Hoare logic in HASCASL[END_REF] and extended to a treatment of Java-style abrupt termination [START_REF] Schröder | Generic exception handling and the Java monad[END_REF][START_REF] Walter | Parametrized exceptions[END_REF]. Practical applications of MDL include reasoning about Haskell and the imperative fragment of Java. Numerous examples and a coding in the theorem prover Isabelle can be found in [START_REF] Walter | Monadic dynamic logic: Application and implementation[END_REF].

The completeness result now guarantees closedness of the deduction system (after the extension w.r.t. [START_REF] Schröder | Monad-independent dynamic logic in HASCASL[END_REF]) and paves the way for the future development of decision procedures. Of course, one cannot expect a decision procedure for arbitrary equational theories. In this respect, our calculus (unlike similar calculi [Pit91, Mog95, GSM06]) has the advantage that it makes use only of a rather limited and efficiently decidable equational theory. In particular, equations between programs are avoided; instead, properties of programs are expressed in terms of their observable behaviour.

More practical experience is needed for evaluating how practical actual proofs of purity and observational purity are. Typically, such proofs will not be semantical like those of the claims made in Sect. 5, but rather rely on the types of basic operations that deliver pure results, and on suitable axioms. Indeed, our calculus can be instantiated with a variety of different effects by axiomatising these effects; we have provided one sample axiomatisation for the dynamic reference monad.

The generalisation to non-simple monads is an important open question. Another important extension will be the treatment of control structures such as while loops (which currently happens at the meta-level) as well as of datatypes in the calculus proper.

Figure 2 .

 2 Figure 2. Semantics of monad-based dynamic logic

1.

  Stateful computations with non-termination (T A = (S →? (A × S))): Elements of P Ω are state-dependent truth values, i.e. functions S → Ω. A state s satisfies [x ← p] ϕ if the value x, if any, returned by p after terminating execution starting in state s satisfies ϕ. 2. Non-determinism (T A = P(A)): P Ω is isomorphic to the set Ω of truth values; [x ← p] ϕ holds if all x ∈ p satisfy ϕ. 3. Exceptions (T A = A + E): P Ω is essentially Ω; [x ← p] ϕ holds if p is either an exception or a value x satisfying ϕ. 4. Interactive input (T A = µγ. A + (U → γ)): P Ω is essentially Ω; [x ← p] ϕ holds if the value returned by p after reading a number of inputs satisfies ϕ. Interactive output (T A = µγ. A + (U × γ)): again, P Ω is essentially Ω, and [x ← p] ϕ holds if the value returned by p satisfies ϕ (the output is ignored). 5. Non-deterministic stateful computations (T A = P(S → (A × S))): Elements of P Ω are state-dependent truth values S → Ω. A state s satisfies [x ← p] ϕ if all values x possibly returned by p after terminating execution starting in state s satisfy ϕ. 6. Java monad (T A = S → (A × S + E × S + 1): again, P Ω is S → Ω, and [x ← p] ϕ means that all values x returned by p after a terminating execution satisfy ϕ.

Figure 3 .

 3 Figure 3. The generic proof calculus for monad-based dynamic logic for ϕ, ψ : P Ω. The following two claims are proved similarly as in [SM04a].

Proposition 4. 1 (

 1 Soundness of MDL). If Φ ψ, then Φ |= ψ.

  and the unique morphism into the terminal object is ! A := [x : A £ * : 1] ∼ . Axiom (CC) ensures that this does define a cartesian structure.

Lemma 6. 9 .

 9 If Φ [x ← p] ϕ, then do x ← p; ret (x, ϕ) ∼ do x ← p; ret (x, ) Proof. It suffices to prove Φ [x ← p; y ← ϕ] ψ ⇐⇒ [x ← p; y ← ret ] ψ for every monadic formula ψ in arbitrary context. Now the assumption implies [x ← p] (ϕ ⇐⇒ ret ) by propositional reasoning. Thus we have Φ

  Lemma 6.10 (Truth Lemma). T Σ,Φ |= ϕ iff Φ ϕ.Proof. T Σ,Φ |= G ϕ iff [[ϕ]] = [[ ]] iff (by Cor. 6.6) ϕ ∼ iff for all MDL formulae ψ, Φ ψ[ϕ/x] ⇐⇒ ψ[ /x] iff (by (cong)) Φ ϕ ⇐⇒ iff (by (taut), (mp)) Φ ϕ.The main result now follows straightforwardly: Theorem 6.11 (Completeness of MDL). If Φ |= ψ, then Φ ψ. Proof. Let Φ |= ψ. By the Truth Lemma, T Σ,Φ |= Φ, hence T Σ,Φ |= ψ (noting that by Prop. 6.8 T is a simple monad admitting dynamic logic). Again by the Truth Lemma, Φ ψ.

  and by (dis) and (ret P), [x ← ret a; y ← [p] ret a] ret y ⇐⇒ [y ← [p] ret a] ret y ⇐⇒ [p] ret a. Definition 4.3. A term is in product β-normal form if it does not contain subterms of the form fst t, u or snd t, u . Lemma 4.4. Let Γ £ t : B be in product β-normal form. If B is T -free, then t does not contain a subterm whose type is of the form T A.

  b and we are done by the induction hypothesis.3. p n = ret s. Here s must be of boolean type, as explained below. By induction, we can prove either [x 1 ← p 1 ; . . .; x i-1 ← p i-1 ] ret s or [x 1 ← p 1 ; . . . ; x i-1 ← p i-1] ret (¬s), and in each case invariance holds. This immediately implies that we can prove either [x ← p] ret (x n = ) or [x ← p] ret (x n = ⊥), respectively, and invariance holds in each case. 4. p n is an atomic program, i.e. either assignment or allocation or dereferencing. If the truth value of the final monadic formula does not depend on x n , then p n may be safely discarded, thus discharging this case by induction; this is applicable if p n is of type T 1 (i.e. p n is an assignment) and if the final monadic formula does not mention x n . Note that in the first case, invariance stipulates that p n itself can be invariantly exchanged for another term of the same type; this is evidently the case, as the previous argument applies to any term of type T 1. Next, suppose that p n = new v for some v, and that the target test is of the form x n = x i for some i. If p i is atomic, then it can only be an another new operator, and we have [. . . ; x i ← new w; . . . ; x n ← new v] ret (x n = x i ) by axiom (new-distinct) in the definition of Toy Java. If p i is not atomic, then it is either a binding or a box; both cases are reduced to the induction hypothesis similarly as in the previous steps. Finally, let p n = *v. We need to show that for some closed term t [x ← p] ret (x n = t) is provable. We proceed by case distinction over p n-1 . If p n-1 is atomic, we are done by the following equivalences and the induction hypothesis.

There are two dynamic logics for Java, one for the KIV prover[START_REF] Stenzel | A formally verified calculus for full java card[END_REF], and on in the KeY project[START_REF] Beckert | A dynamic logic for the formal verification of Java Card programs[END_REF]. However, they neither address purity, nor are they generic.

The original calculus does feature generic loop constructs; however, absolute completeness results such as the one proved here are impossible for dynamic logics over Turing complete languages: this would entail recursive enumerability of the set of non-terminating programs.

Till Mossakowski, Lutz Schröder, Sergey Goncharov(var)x :A ∈ Γ Γ £ x : A (app) f : A → B ∈ Σ Γ £ t : A Γ £ f (t) : B (1) Γ £ * : 1 (fst) Γ £ t : A × B Γ £ fst(t) : A (snd) Γ £ t : A × B Γ £ snd(t) : A (pair) Γ £ t : A Γ £ u : B Γ £ t, u : A × B ( ) Γ £ : Ω (⊥) Γ £ ⊥ : Ω (¬) Γ £ a : Ω Γ £ ¬a : Ω similarly for ∧, ∨, ⇒, ⇐⇒(do)Γ £ p : T A Γ, x : A £ q : T B Γ £ do x ← p; q : T B (doP) Γ £ p : P A Γ, x : A £ q : P B Γ £ do x ← p; q : P B (ret) Γ £ t : A Γ £ ret t : P A (P)

× is product with projections π 1 , π 2 , 1 the terminal object with ! A : A → 1 the unique arrow.

One obvious possibility is to let P A consist of all pure computations; this always gives a strong submonad. We will use this possibility in the examples below.

Acknowledgements This work has been supported by the German Federal Ministry of Education and Research (Project 01 IW 07002 FormalSafe) and by the DFG (project HASCASL KR 1191/7-2). The authors wish to thank the anonymous referees for useful comments, and Erwin R. Catesbeiana for pointing out various pitfalls.

We are now ready to complete the term model construction by constructing a monad T Σ,Φ on C Σ,Φ . It is given by the following data: T Σ,Φ A := T A, η A := [x : A £ ret x : T A] ∼ , and given x : A £ q : T B, [x : A £ q : T B] * ∼ := [p : T A £ do x ← p; q : T B] ∼ Well-definedness follows easily by Theorem 6.1. Finally, the strength is given by

In C Σ,Φ , Hom(A, Ω) is coherently turned into a Boolean algebra by defining e.g.

) is coherently a Boolean algebra, that is, Ω is an internal Boolean algebra object.

Proof. We show a sample Boolean algebra law, namely commutativity of ∧. We note that by (retP

Coherence of the Boolean algebra structure follows since composition is substitution (Lem. 3.3).

We also need to show that the generalised elements of (i.e. morphisms into) P A are pure, i.e. discardable and copyable. Concerning discardability, for ϕ : P A, we need to show (do x ← ϕ; ret * ) ∼ ret * , i.e.

By (retP), [a ← ret * ] ψ ⇐⇒ ψ. By (retP) and (dis), ψ ⇐⇒ [x ← ϕ; ret * ] ψ. By (ctrP), this is in turn equivalent to [a ← (do x ← ϕ; ret * )] ψ. The proof of copyability is similar and uses axiom (copy). Lemma 6.4. In C Σ,Φ , (id

Proof. Since composition in the term model is substitution, we need to show that for all x : A × Ω £ t : B, x :

By definition of contextual equivalence, this means that for any ϕ (w.l.o.g. assuming that x is not free in ϕ), we have, when defining ψ :≡ ϕ[t/z] ⇐⇒ ϕ[u/z], that ψ[ y, /x] and ψ[ y, ⊥ /x] imply ψ. As a first important property of the term model T Σ,Φ , we prove: