Refinement Calculus

(and Martin-Löf type theory)

Peter Hancock

peter@premise.demon.co.uk
http://www.dcs.ed.ac.uk/~pgh

March 2002

Summary

Some (unexpected) connections between the refinement calculus (Back, Morris, Morgan, von-Wright, ...) and Petersson-Synek trees in Martin-Löf type theory.

Suggests a normal form for specifications of certain kinds of interactive program (angelic “user-side” programs and demonic “system-side” programs), expressible with dependent types. A proof that a specification is satisfiable is in principle executable as a program of the appropriate kind.

Many questions raised. I’d like your opinion.

Collaborators

Anton Setzer (Swansea)

– input-output monads and coalgebras Pierre Hyvernat (Lyons/Chalmers)

– implementation

My own interest

– specifications using dependent types.

How to deal with interaction

(action/reaction) in type theory?

What kind of proof is it that

• runs an internet server to book plane-flights and hotel rooms?

• prevents the brakes on a bus from locking in a skid?

• flies a cruise missile?

What proposition does it prove, and how is this connected with a specification of the desired behaviour?

Context: strength of a programming logic

batch  Input ⟶^{f} Output

Input/output is available in its entirity when execution starts/terminates.

Strength: the set of batch programs that can be proved to terminate. (Termination strength, provably total recursive functions)

transaction Input is consumed and output is produced piece by piece. Eventual termination.

Strength: the set of transaction programs that can be proved to terminate (i.e. with output available in its entirity) given a sufficiently long sequence of inputs. (Continuity, well-foundedness, ….)

A model of imperative interfaces

Two levels of choice:

angel, client  demon, server
stimulus,  response
command, response
action,  reaction
move,  counter-move
call,  return
C,  R
S : set ,  ( States )
C(x) : set (x ∈ S),  ( Angel )
R(x, y) : set (x ∈ S, y ∈ C(x)),  ( Demon )
n(x, y, z) : S (x ∈ S, y ∈ C(x), z ∈ R(x, y))  ( next )

For each s ∈ S a family of families of outcomes:

{ { n(s, c, r) | r ∈ R(s, c) } | c ∈ C(s) }

Interaction structure

Φ : S → 𝔽(𝔽(S′))

s ∈ S  a state (position)
c ∈ C(s) an input (action) in state s ∈ S
r ∈ R(s,c) an output (reaction)

in response to c ∈ C(s)

s[c / r] : S′ the new state after interaction c/r.
= n(s,c,r) notation

Interaction system

(S : set , Φ : S → 𝔽(𝔽(S)), s_{0} ∈ S)

Notions of powerset

subset S  notation
ℙ(S) = set^{S}  P = { s ∈ S | P(s) }
𝔽(S) = (∃ T : set )S^{T}  ⟨T, s⟩ = { s(t) | t ∈ T }

Predicates to families: ‘Σ-types’ and (first) projection.

P ↦ { π_{0}(z) | z ∈ (∃ s ∈ S)P (s) }

Families to predicates: singleton predicates^{∗} { s } = { s′ ∈ S | s′ =_{S} s }.

{ s(t) | t ∈ T } ↦ { s′ ∈ S | s′ =_{S} s(t) }

(∗: Singleton predicates are evil.)

The programmer’s firmament

A → B^{Function}

A → ℙ(B)^{Relation}

Transition Structure

A → 𝔽(B)

Predicate Transformer

A → ℙ(ℙ(B)) ≅ ℙ(B) → ℙ(A) (flip)

Interaction Structure

A → 𝔽(𝔽(B))

Interaction structures as predicate transformers

Given Φ : S → 𝔽(𝔽(S′)), define Φ^{∘} : ℙ(S′) → ℙ(S).

Φ^{∘}(X) = \{ s ∈ S | \begin{matrix}(∃ c ∈ C_{Φ} (s)) \\ (∀ r ∈ R_{Φ} (s, c)) \\ X(n_{Φ} (s, c, r)) \} \end{matrix}

“DNF” (Disjunctive Normal Form). Aside : conjunctive normal form doesn’t work.

The refinement calculus

• predicate transformers (business end): Φ, Ψ ::= • abort, magic, Φ ⊔ Ψ, Φ ⊓ Ψ, ⊔_{i}Φ_{i}, ⊓_{i}Φ_{i}, ⟨ϕ⟩, [ϕ] • skip, (Φ ; Ψ)

Φ ⊑ Ψ = ∀X. Φ(X) ⊆ Ψ(X)

• relations: R ::= … ϕ ::= … • predicates: P, Q ::= …

• state transformers: f, g ::= …

• ergonomics.

Semantic hijack e.g. sequential composition

C_{Φ;Ψ} (s)

\begin{matrix}= (∃ c ∈ C_{Φ} (s))(∀ r ∈ R_{Φ} (s, c))C_{Ψ} (n_{Φ} (s, c, r)) \\ = Φ^{∘}(C_{Ψ} , s) \end{matrix}

R_{Φ;Ψ} (s, ⟨c, f⟩)

= (∃ r ∈ R_{Φ} (s, c))R_{Ψ} (n_{Φ} (s, c, r), f(r)) n_{Φ;Ψ} (s, ⟨c, f⟩, ⟨r, r′⟩)

= n_{Ψ} (n_{Φ} (s, c, r), f(r), r′)

Have to check (Φ; Ψ)^{∘} = Φ^{∘} · Ψ^{∘}. Proof: axiom of choice, amalgamation of same-sex quantifiers.

Two forms of recursion

Φ^{∗} = μΨ. skip ⊔ (Φ ; Ψ)
Φ^{∞} = νΨ. skip ⊓ (Φ ; Ψ)

Φ^{∗}: inductively defined (Petersson and Synek). We have to terminate eventually, but we can choose when. Formally a closure operator.

Φ^{∞}: coinductively defined. They can choose to terminate at any point, or not at all. Formally an interior operator.

Y = Φ^{∞}(X) is the weakest invariant of Φ (i.e. post fixed point, satisfying Y ⊆ Φ(Y)) that implies X.

Y = Φ^{∗}(X) is also an invariant (Lambek). It is the strongest invariant of Φ that is implied by X holding eventually.

Φ^{∼} = Φ with the angel and the demon swapped.

What theorem is proved by a c/r-program?

(First approximation.)

a client (terminating) A ⊆ Φ∗(B) Requires A initially, guarantees B finally (provided there is a ‘finally’).

a server (perpetual) A ↓^{‘overlaps’} ; )(Ψ∞(B) Guarantees A initially, and B perpetually.

where Ψ = Φ^{∼}. Problem: relate state in B to state in A.

More grit

Given

\begin{matrix}A : ℙ(S) \\ B : ∀s ∈ S. A(s) → ℙ(S) \end{matrix}

initial condition, termination/invariant condition

\begin{matrix}(∀ s ∈ S, p ∈ A(s)) Φ^{∗}(B(s, p), s) \\ (∃ s ∈ S, p ∈ A(s)) Ψ^{∞}(B(s, p), s) \end{matrix}

Inconclusion

I freely admit I don’t (continuously) find these suggestions very convincing.

Some directions:

• Case studies.

• Thorough study of refinement calculus. (Different sub-species of predicate transformer: conjunctive, continuous, … commuting with intersections/unions of various kinds)

• Relate to work linear-time temporal logic. (eg. Lamport’s TLA.)

• Relate to work in formal topology.

(Sambin, Mulvey etc.)

Work on type theory: coinduction (in ‘intensional’ type theory).