\underline{Functions} ; A → B

\underline{Relations} ; A → Pow(B)

Transition Systems A → Fam(B)

Predicate Transformers A → Pow(Pow(B)) ≅ Pow(B) → Pow(A)

Interaction Systems A → Fam(Fam(B))

Pow(X ) = X → Set  ( contravariant )
Fam(X ) = (ΣI : Set)X^{I}  ( covariant )

Coalgebras

Transition Systems (A, λa.(B(a), λb.a[b]))

\begin{aligned}A & : & Set \\ B & : & A → Set \\ [ ] & : & (Πa : A)B(a) → A \end{aligned}

Interaction Systems (A, λa.(B(a), λb.(C(a, b), λc.a[b/c])))

A  : Set
B  : A → Set
C  : (Πa : A)B(a) → Set
[ / ] : (Πa : A, b : B(a))C(a, b) → A

Setup for Petersson-Synek ‘Tree sets’.

Interactive system (game) interpretation

a : A  a state (position)
b : B(a)  an input (action) in state a : A
c : C(a, b) an output (reaction) in response to b : B(a)
a[b/c] : A the new state after interaction b/c.

[figure: b : B(a); a ↦ a[b/c]; c : C(a, b)]

Rule set interpretation

a : A  a formula
b : B(a)  an inference step with conclusion a
c : C(a, b) a sub-proof (premise) required by b
a[b/c] : A the formula to be proved by sub-proof c

…  c … a[b/c]  b a

Predicate transformers

Interaction Systems (A, λa.(B(a), λb.(C(a, b), λc.a[b/c])))

P^{∘∘}(a) = (Σb : B(a))(Πc : C(a, b))P (a[b/c])
P^{••}(a) = (Πb : B(a))(Σc : C(a, b))P (a[b/c])
Bar  = μP.P^{∘∘} ⊆ P
Pos  = νP.P ⊆ P^{••}

Petersson-Synek ‘Tree sets’: T (a) = Bar(a)

Bar

Constructor: \frac{x : Bar^{∘∘}(a)}{bar(x) : Bar(a)}

Recursor:

BarRec : (Π G : (Πa : A, x : Bar(a))Set g : (Π \begin{matrix}a : A, b : B(a), \\ f : (Πc : C(a, b))Bar(a[b/c]), \\ h : (Πc : C(a, b))G(a[b/c], f(c))) \end{matrix} ) G(a, bar(b, f)) a : A, x : Bar(a) ) G(a, x)

Equation: ([G, g]) ≡ BarRec(G, g) ([G, g])(a, bar(b, f)) = g(a, b, f, λc.([G, g])(a, f(c)))

Sequential composition

Given ρ_{1}, ρ_{2} : A → Fam(Fam(A)), where

\begin{aligned}ρ_{1} & = & λa.(B_{1}(a), λb.(C_{1}(a, b), λc.a[b/c]_{1})) \\ ρ_{2} & = & λa.(B_{2}(a), λb.(C_{2}(a, b), λc.a[b/c]_{2})) \end{aligned}

define ρ_{1} ;^{∘} ρ_{2} = ρ such that ρ^{∘∘} = ρ_{1}^{∘∘} · ρ_{2}^{∘∘}.

ρ \{ \begin{matrix}B(a) & = & \underbrace{(Σb : B_{1}(a))(Πc : C_{1}(a, b))B_{2}(a[b/c]_{1})}_{ρ_{1}^{∘∘}(B_{2},a)} \\ C(a, (b, f)) & = & (Σc : C_{1}(a, b))C_{2}(a[b/c]_{1}, f(c)) \\ a[(b, f)/(c_{1}, c_{2})] & = & a[b/c_{1}]_{1}[f(c_{1})/c_{2}]_{2} \end{matrix}

The programmer’s predicament

The devil  [figure: α; server; ω; client]  The deep blue sea

Transactions

B^{⋆}  = μP.True ∪ P^{∘∘}
C^{⋆}(a, inl 0)  = 1
C^{⋆}(a, inr (b, f))  = (Σc : C(a, b))C^{⋆}(a[b/c], f(c))
a[inl 0/0]^{⋆}  = a
a[inr (b, f)/(c, cs)]^{⋆} = a[b/c][f(c)/cs]^{⋆}
t : B^{⋆}(a) – well founded trees with ‘leaves’
p : C^{⋆}(a, t) – paths through t to a leaf
a[t/p]^{⋆}  – state at end of path p

Refinement

[figure: α; server; ω; client]

[α, ω] → \begin{matrix}(Πb : B(α))(Σt : B^{⋆}(ω)) \\ (Πp : C^{⋆}(ω, t)(Σc : C(α, b) \\ [α[b/c], ω[t/p]^{⋆}] \end{matrix}

We need a greatest fixed point of this relation transformer.

Composition of refinement

[figure: α; server; μ; client; μ; server; ω; client]

… A challenge!