Introduction  The Operational Models  The Monads used in these Models

Compound Monads in Specification Languages

Jeremy Dawson

Logic and Computation Program, NICTA ^{1}

Automated Reasoning Group, Australian National University, Canberra, ACT 0200, Australia

                 http://users.rsise.anu.edu.au/^{∼}jeremy/

September 4, 2007

1National ICT Australia is funded by the Australian Government’s Dept of Communications, Information Technology and the Arts and the Australian Research Council through Backing Australia’s Ability and the ICT Centre of Excellence program.

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model The Chorus Angelorum Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads The Chorus Angelorum Monad Definition of Choice

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model The Chorus Angelorum Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads The Chorus Angelorum Monad Definition of Choice

Introduction  The Operational Models  The Monads used in these Models

Introduction

Several sorts of refinement suggested by Dunne.

General Correctness Total Correctness Chorus Angelorum

Each is based, implicitly or explicitly, on a notion of what a computation is, an underlying “model of computation” Each underlying “model of computation” is based on a monad Each of these monads is, or is somewhat like, a compound monad

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model The Chorus Angelorum Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads The Chorus Angelorum Monad Definition of Choice

The General Correctness Operational Model

Want to distinguish computations which (on a given initial state) fail to terminate terminate in final state s non-deterministically, either of the above

Neither wlp / partial correctness nor wp / total correctness does this. General correctness refinement (Dunne):

A ⊑ B ≡ wp(A, Q) ⇒ wp(B, Q) ∧ wlp(A, Q) ⇒ wlp(B, Q)

The General Correctness Operational Model

Type of Computations

A computation (on given state) produces a set of outcomes. An outcome is either

NonTerm, indicating non-termination, or Term s, indicating termination in the state s.

In Isabelle: datatype σ TorN = NonTerm | Term σ

For a non-deterministic computation (from given initial state), result is a set of outcomes.

type outcome = TorN state

type of computations is state → set TorN state

Introduction  The Operational Models  The Monads used in these Models

The Total Correctness Operational Model

Related to semantics of the B-method, only interested in total correctness (weakest preconditions). A computation which may fail to terminate fails every post-condition. Such computation is refinement-equivalent to a computation which does fail to terminate. Type of results is either

NonTerm, indicating possible non-termination, or Term S, indicating termination in a state s ∈ S.

type of result tcres (“total correctness result”) = TorN set state type of computations is state → TorN set state weakest precondition function (hence refinement):

[C] Q s = ∃S. (∀x ∈ S. Q x) ∧ C s = Term S

The Chorus Angelorum Operational Model

Ordinarily, non-determinism is demonic choice (all possible results must satisfy post-condition ≡ the result chosen by a demon satisfies post-condition)

Want to model angelic and demonic non-determinism

Computation returns a set of sets A of states:

angel chooses set A ∈ A demon chooses state a ∈ A

weakest precondition function (hence refinement):

[C] Q s = ∃U ∈ C s. (∀u ∈ U. Q u)

If A ∈ A, A′ ⊇ A, to include A′ in A, or not, makes no difference: consider only A up-closed: if A′ ⊇ A and A ∈ A then A′ ∈ A.

Confirming the Models

In each case, to confirm model is appropriate, we show two computations refinement-equivalent iff they are the same function (of type used in model) we define operations operationally, and prove these definitions correspond to Dunne’s definitions (which use weakest preconditions)

(Caveat: we ignore “frames”). Note: all proofs in the theorem prover Isabelle/HOL

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model The Chorus Angelorum Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads The Chorus Angelorum Monad Definition of Choice

Introduction  The Operational Models  The Monads used in these Models

Monads

Long known in category theory. Define unit and extension functions, satisfying rules

unit : α → Mα
ext : (α → Mβ) → (Mα → Mβ)
ext f ∘ unit = f
ext unit = id
ext (ext g ∘ f ) = ext g ∘ ext f

or functions unit, map and join (7 axioms for these) Can represent the structure of a computation (Moggi)

Monads — the Kleisli category

ext B models the action of B on result of previous computation Define B ⊙ A = ext B ∘ A : sequencing computations B and A.

f ⊙ unit = f  (1)
unit ⊙ f = f  (2)
h ⊙ (g ⊙ f ) = (h ⊙ g) ⊙ f  (3)

Properties (1) to (3) show that we have a category:

objects are types

arrow from α to β is function α → Mβ,

the identity arrow for object α is the function unit : α → Mα composition is given by ⊙.

Called the Kleisli category of M, K(M).

Monads — the Kleisli category

ext B models the action of B on result of previous computation Define B ⊙ A = ext B ∘ A : sequencing computations B and A.

f ⊙ unit = f  (1)
unit ⊙ f = f  (2)
h ⊙ (g ⊙ f ) = (h ⊙ g) ⊙ f  (3)

Properties (1) to (3) show that we have a category:

objects are types

arrow from α to β is function α → Mβ,

the identity arrow for object α is the function unit : α → Mα composition is given by ⊙.

Called the Kleisli category of M, K(M).

Monads — Examples

The non-termination monad: a computation either terminates in a new state, or fails to terminate.

unit nt s = Term s

map nt f NonTerm = NonTerm map nt f (Term s) = Term (f s)

ext nt f NonTerm = NonTerm ext nt f (Term s) = f s

The set monad: models non-deterministic (but necessarily terminating) computations.

Monads — Examples

The non-termination monad: a computation either terminates in a new state, or fails to terminate.

unit nt s = Term s

map nt f NonTerm = NonTerm map nt f (Term s) = Term (f s)

ext nt f NonTerm = NonTerm ext nt f (Term s) = f s

The set monad: models non-deterministic (but necessarily terminating) computations.

Introduction  The Operational Models  The Monads used in these Models

Compound Monads

Let M and N, each with unit and extension functions, be monads. Then is MNα a monad? Need unit_{MN} : α → MNα and ext_{MN} ext_{MN} “extends” a function f from domain α to MNα. pext, “partial extension”, does part of this

ext_{MN} : (α → MNβ) → (MNα → MNβ)
pext : (α → MNβ) → (Nα → MNβ)

Definitions using pext for a compound monad

ext_{MN} g = ext_{M} (pext g)
unit_{MN} = unit_{M} ∘ unit_{N}

Introduction  The Operational Models  The Monads used in these Models

Compound Monads

Let M and N, each with unit and extension functions, be monads. Then is MNα a monad? Need unit_{MN} : α → MNα and ext_{MN} ext_{MN} “extends” a function f from domain α to MNα. pext, “partial extension”, does part of this

ext_{MN} : (α → MNβ) → (MNα → MNβ)
pext : (α → MNβ) → (Nα → MNβ)

Definitions using pext for a compound monad

ext_{MN} g = ext_{M} (pext g)
unit_{MN} = unit_{M} ∘ unit_{N}

Introduction  The Operational Models  The Monads used in these Models

Compound Monads — rules for pext

pext also must satisfy three rules

pext f ∘ unit_{N} = f
pext unit_{MN} = unit_{M}
pext (ext_{MN} g ∘ f ) = ext_{MN} g ∘ pext f

unit_{MN} and pext are the unit and extension functions of a monad in the category K(M), whose Kleisli category is also K(MN).

Compound Monads — Distributive Law

Jones & Duponcheel: two conditions, J(1) and J(2), which compound monads may satisfy.

Assuming unit_{MN} = unit_{M} ∘ unit_{N} and map_{MN} = map_{M} ∘ map_{N}, compound monads arise from a function pext iff J(1) holds

Compound monads satisfying J(1) and J(2) are those arising from a distributive law swap : NMα → MNα A distributive law satisfies S(1) to S(4) of Jones & Duponcheel

swap = pext (map_{M} unit_{N})

Introduction  The Operational Models  The Monads used in these Models

The General Correctness Compound Monad

Want set TorN α is a monad; in fact, for any monad M, M TorN α is a monad

pext : (α → M TorN β) → (TorN α → M TorN β)

pext f (Term a) = f a

             pext f NonTerm = unit_{M} NonTerm

Proof of pext axioms easy. Arises from a distributive law: swap = pext (map_{M} unit_{N}), so

swap gc : TorN set α → set TorN α

            swap gc NonTerm = {NonTerm}

swap gc (Term S) = {Term s | s ∈ S}

Introduction  The Operational Models  The Monads used in these Models

The Total Correctness Compound Monad

Recall tcres = TorN set state.

pext tc : (state → tcres) → set state → tcres

defined using prod tc : set tcres → tcres

                prod tc S = NonTerm  if NonTerm ∈ S

prod tc {Term s | s ∈ S} = Term (⋃ S)

The Total Correctness Compound Monad

A Distributive Law and Monad Morphism

Total Correctness monad also arises from a distributive law:

swap tc : set TorN σ → TorN set σ

                swap tc S = NonTerm  if NonTerm ∈ S

swap tc {Term s | s ∈ S} = Term S

Relating the General and Total Correctness monads

swap tc : set TorN σ → TorN set σ is also a monad morphism from the general correctness monad to the total correctness monad.

unit tc a = swap tc (unit gc a)
ext tc (swap tc ∘ f ) (swap tc x) = swap tc (ext gc f x)

Since it is surjective, could use monad axioms for general correctness monad to prove axioms for total correctness monad.

The Chorus Angelorum Monad

up-closure, swapping angel and demon

Result A : set set state (up-closed): angel chooses A ∈ A, demon chooses a ∈ A.

Alternative model: demon chooses first, then angel.

swap uc turns angel-chooses-first result into demon-chooses-first.

up cl: the up-closure of a set of sets.

swap uc A = {B | ∀A ∈ A. B ∩ A ≠ {}}
up cl A = {A′ | ∃A ∈ A. A ⊆ A′}

up cl (up cl A) = up cl A  swap uc (swap uc A) = up cl A
swap uc (up cl A) = swap uc A  up cl (swap uc A) = swap uc A

So work on equivalence classes of sets of sets of states A ≡ A′ iff up cl A = up cl A′ each equivalence class has exactly one up-closed member.

The Chorus Angelorum Monad

up-closure, swapping angel and demon

Result A : set set state (up-closed): angel chooses A ∈ A, demon chooses a ∈ A.

Alternative model: demon chooses first, then angel.

swap uc turns angel-chooses-first result into demon-chooses-first.

up cl: the up-closure of a set of sets.

swap uc A = {B | ∀A ∈ A. B ∩ A ≠ {}}
up cl A = {A′ | ∃A ∈ A. A ⊆ A′}

up cl (up cl A) = up cl A  swap uc (swap uc A) = up cl A
swap uc (up cl A) = swap uc A  up cl (swap uc A) = swap uc A

So work on equivalence classes of sets of sets of states A ≡ A′ iff up cl A = up cl A′ each equivalence class has exactly one up-closed member.

The Chorus Angelorum Monad

proofs of monad rules

try to prove S(1) to S(4) (to show distributive law): cannot, but we can prove them modulo up-closure, eg

swap uc A = up cl (map s unit s A) S(2)′
swap uc (map s unit s A) = up cl A  S(3)′

proofs of the monad axioms for set set α (again, some equalities only modulo up-closure) difficult, but imitated usual proofs from S(1) to S(4) defined type ucss α : up-closed sets of sets (ie, a representative of each equivalence class) defined the monad functions for the ucss α type translated results about set set α to ucss α: it is a monad!

Introduction  The Operational Models  The Monads used in these Models

The Chorus Angelorum Monad

Link to Continuation Monad

First, recall functions used by Jones & Duponcheel

join : M N M N α → M N α prod : N M N α → M N α
dorp : M N M α → M N α  swap : N M α → M N α

Think of M (N) as a set from which angel (demon) chooses. “evaluation function” eval uc : set set α → (α → bool) → bool, eval uc A P tells whether the post-condition P is satisfied when angel and demon have made their choices from A. eval uc B P ≡ ∃B ∈ B. ∀b ∈ B. P b. (α → bool) → bool is type of continuation monad K α Ball and Bex: set α → (α → bool) → bool, ie : set α → K α express quantification over a given set: Ball S P ≡ ∀s ∈ S. P s

The Chorus Angelorum Monad

Link to Continuation Monad – ctd

eval uc = Ball ⊙_{K} Bex
eval uc ∘ swap uc = Bex ⊙_{K} Ball

Using obvious isomorphism K α → set set α, called K to SS:

join uc = K to SS ∘ (Ball ⊙_{K} Bex ⊙_{K} Ball ⊙_{K} Bex)
dorp uc = K to SS ∘ (Bex ⊙_{K} Ball ⊙_{K} Bex)
prod uc = K to SS ∘ (Ball ⊙_{K} Bex ⊙_{K} Ball)
swap uc = K to SS ∘ (Bex ⊙_{K} Ball)
ext uc f = K to SS ∘ (Ball ⊙_{K} (Bex ∘ f ) ⊙_{K} Ball ⊙_{K} Bex)
pext uc f = K to SS ∘ (Ball ⊙_{K} (Bex ∘ f ) ⊙_{K} Ball)

Introduction  The Operational Models  The Monads used in these Models

Angelic and Demonic Choice

We defined these as follows (simplified by omitting conversion between the set set α and ucss α types assuming up-closed families of sets)

dem B s = ⋂ {B s | B ∈ B}
ang B s = ⋃ {B s | B ∈ B}

giving these results (which would normally be the definitions)

[dem B] Q s = ∀B ∈ B. [B] Q s
[ang B] Q s = ∃B ∈ B. [B] Q s