Epilogue

I thought I might report a bit about what I’ve been up to with coinduction. Headline: we can set up propositional equality so that every coprogram equals its unfolding, even though that had jolly well better not hold definitionally if we want decidable anything.

What I’ve got is an Agda universe with inductive and coinductive Petersson-Synek trees (also known as Hancock-Setzer interaction structures). Actually, it’s a pair of universes—PROP and SET. Equality is a proposition computed recursively over the structure of sets and elements.

The underlying sets

Let’s have Zero : Set; _ : One : Set; tt, ff : Two : Set. Let’s have (x : S) -> T. Let’s have record-style Sigma-types Sg S T, with projections fst and snd, handy split functional sp0 (eliminating over Set, sp0 f p = f (fst p) (snd p)) and defined constructor _,_. Let’s have

record Cont (S : Set) : Set1 where
  field
    Comm : S -> Set
    Resp : (s : S) -> Comm s -> Set
    next : (s : S) -> (c : Comm s) -> Resp s c -> S

open module Cont’ {S : Set} = Cont {S}

Fun : {S : Set} -> Cont S -> (S -> Set) -> S -> Set
Fun F X s = Sg (Comm F s) \ c -> (r : Resp F s c) -> X (next F s c r)

That’s yer state-indexed interaction structure kit. Now there’s

data IMu {S : Set}(F : Cont S)(s : S) : Set where
  con : (c : Comm F s)-> ((r : Resp F s c)-> IMu F (next F s c r)) -> IMu F s

induction : forall {S}(F : Cont S)(P : Sg S (IMu F) -> Set) ->
    ((s : S)(c : Comm F s)(f : (r : Resp F s c) -> IMu F (next F s c r))->
    ((r : Resp F s c) -> P (next F s c r , f r)) -> P (s , con c f)) ->
    {s : S}(x : IMu F s) -> P (s , x)
induction {S} F P p {s} (con c f) = p s c f \ r -> induction F P p (f r)

Exercise: define the plain fold instead of dependent induction; find out what else you need to reconstruct induction on IMu F from the plain fold on IMu BoxF, where BoxF : Cont (Sg S (IMu F)), a suitably constructed container for inductive hypotheses. But I digress.

Let’s have general codata, with a coconstructor…

codata INu {S : Set}(F : Cont S)(s : S) : Set where
  con : (c : Comm F s)-> ((r : Resp F s c)-> INu F (next F s c r)) -> INu F s

…and yer final coalgebra…

out : forall {S}{F : Cont S}{s} -> INu F s -> Fun F (INu F) s
out (con c f) = c , f

…cut into pieces for ease of reference. A coprogram, or interaction structure (client-view) has an initial command which it issues…

command : forall {S}{F : Cont S}{s} -> INu F s -> Comm F s
command d = fst (out d)

…and a strategy to continue after a response is delivered.

continue : forall {S}{F : Cont S}{s}(d : INu F s)
    (r : Resp F s (command d)) -> INu F (next F s (command d) r)
continue d = snd (out d)

Here’s how to write coprograms. First of all, we’ll need the appropriate notion of morphism between indexed sets—the index-respecting functions.

_->>_ : {S : Set} -> (S -> Set) -> (S -> Set) -> Set
A ->> B = (s : _) -> A s -> B s

Then we can say that if F defines a command-response structure, any F-coalgebra gives a way to construct F-coprograms.

unfold : forall {S}{F : Cont S}(A : S -> Set) ->
    (A ->> Fun F A) -> A ->> INu F
unfold A g s a = con (fst x) \ r -> unfold A g _ (snd x r) where x = g s a

What’s an F-coalgebra? It’s a choice of carrier A : S -> Set, being a kitbag of whatever we need to make progress in a given state, and a function of type A ->> Fun F A, showing how the kit can be used to handle one interaction, leaving the right kit to continue in whatever state results. Such is the basis of sustainable progress: if we have an F-coalgebra, and we have a startup kit, we can manage whatever interaction we’re prompted for.

Note that the above ‘equation’ does not hold definitionally, nor can it in a theory with decidable definitional equality—it can unfold forever. Rather, it computes only when triggered by out. Even so, one should be able to prove this equation. It ain’t gonna happen with the intensional identity type (whose canonical values reflect only the definitional equality).

A universe of propositions and sets

Or two universes, mutually defined. Or something. I have two sorts…

data Sort : Set where
  PROP SET : Sort

…and I give you…

mutual
  data Ty : Sort -> Set where
    `0′ `1′ : Ty PROP
    `2′ : Ty SET
    `Pi’ : {K : Sort}(S : Ty SET) (T : [ S ] -> Ty K) -> Ty K
    `Sg’ : {K : Sort}(S : Ty K) (T : [ S ] -> Ty K) -> Ty K
    `IMu’ : (S : Ty SET)(C : [ S ] -> Ty SET)
          (R : (s : [ S ])(c : [ C s ]) -> Ty SET)
          (n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->
          (s : [ S ]) -> Ty SET
    `INu’ : {K : Sort}(S : Ty SET)(C : [ S ] -> Ty K)
          (R : (s : [ S ])(c : [ C s ]) -> Ty SET)
          (n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->
          (s : [ S ]) -> Ty K
    `Prf’ : Ty PROP -> Ty SET

  [_] : {K : Sort} -> Ty K -> Set
  [ `0' ] = Zero
  [ `1' ] = One
  [ `2' ] = Two
  [ `Pi' S T ] = (s : [ S ]) -> [ T s ]
  [ `Sg' S T ] = Sg [ S ] \ s -> [ T s ]
  [ `IMu' S C R n s ] = IMu {[ S ]}
    (record {Comm = \ s -> [ C s ]; Resp = \ s c -> [ R s c ]; next = n}) s
  [ `INu' S C R n s ] = INu {[ S ]}
    (record {Comm = \ s -> [ C s ]; Resp = \ s c -> [ R s c ]; next = n}) s
  [ `Prf' P ] = [ P ]

Philosophy and Software Engineering live in PROP. Electronic Engineering and Computer Science live in SET. Big clue: things in contravariant positions (cruel devils) are always SETs, but covariant positions (polite angels) preserve sort. I could add inductive relations, but I want all prop-based computation to be lazy. We have 0, 1, Pi, Sigma, and lazy coinductive predicates.

I think of these coinductive predicates as being a bit like Mickey Mouse costumes at Disneyland. Their inhabitants are obliged to radiate relentless cheerfulness, no matter how horrid the world’s responses.

Equality for sets and values

Here’s another steaming mutual definition for your doorstep. It’s SET equality _<->_ and heterogeneous value equality, ASCIIly depicted ! S > s == T > t ! so you can see all the pieces. Intuitively SET equality means ‘accepts the same values as’, which is a rather tighter notion than isomorphism. The value equality has my usual conditional interpretation: values exchangeable if sets equal, otherwise no information.

mutual

Kick off with some handy abbreviations. Here’s ‘given equal values in these sets…’…

  funQ : (S T : Ty SET) -> ([ S ] -> [ T ] -> Ty PROP) -> Ty PROP
  funQ S T R = `Pi’ S \ s -> `Pi’ T \ t -> ! S > s == T > t ! => R s t

…and here’s ‘these sets are equal, and given equal values in them…’.

  DFunQ : (S T : Ty SET) -> ([ S ] -> [ T ] -> Ty PROP) -> Ty PROP
  DFunQ S T R = (S <-> T) & funQ S T R

Now, set equality is relentlessly structural with the notable exception of proof sets (which are equal by mutual implication). Keep your eyes peeled for swappings in contravariant positions.

  _<->_ : Ty SET -> Ty SET -> Ty PROP
  `2′ <-> `2′ = `1′
  `Pi’ Sl Tl <-> `Pi’ Sr Tr = DFunQ Sr Sl \ sr sl -> Tl sl <-> Tr sr
  `Sg’ Sl Tl <-> `Sg’ Sr Tr = DFunQ Sl Sr \ sl sr -> Tl sl <-> Tr sr
  `IMu’ Sl Cl Rl nl sl <-> `IMu’ Sr Cr Rr nr sr =
      ! Sl > sl == Sr > sr ! &
      DFunQ Sl Sr \ sl sr ->
      DFunQ (Cl sl) (Cr sr) \ cl cr ->
      DFunQ (Rr sr cr) (Rl sl cl) \ rr rl ->
      ! Sl > nl sl cl rl == Sr > nr sr cr rr !
  `INu’ Sl Cl Rl nl sl <-> `INu’ Sr Cr Rr nr sr =
      ! Sl > sl == Sr > sr ! &
      DFunQ Sl Sr \ sl sr ->
      DFunQ (Cl sl) (Cr sr) \ cl cr ->
      DFunQ (Rr sr cr) (Rl sl cl) \ rr rl ->
      ! Sl > nl sl cl rl == Sr > nr sr cr rr !
  `Prf’ Pl <-> `Prf’ Pr = (Pl => Pr) & (Pr => Pl)
  _ <-> _ = `0′

Value equality is as tested for 2, extensional for functions, componentwise for pairs, computed recursively for inductive data, defined as bisimulation for codata, and trivial for proofs. It’s also trivial when the types are obviously different.

  !_>_==_>_! : (S : Ty SET) -> [ S ] -> (T : Ty SET) -> [ T ] -> Ty PROP
  ! `2′ > tt == `2′ > tt ! = `1′
  ! `2′ > tt == `2′ > ff ! = `0′
  ! `2′ > ff == `2′ > tt ! = `0′
  ! `2′ > ff == `2′ > ff ! = `1′
  ! `Pi’ Sl Tl > fl == `Pi’ Sr Tr > fr ! =
      funQ Sl Sr \ sl sr -> ! Tl sl > fl sl == Tr sr > fr sr !
  ! `Sg’ Sl Tl > pl == `Sg’ Sr Tr > pr ! =
      ! Sl > fst pl == Sr > fst pr ! &
      ! Tl (fst pl) > snd pl == Tr (fst pr) > snd pr !
  ! `IMu’ Sl Cl Rl nl sl > dl == `IMu’ Sr Cr Rr nr sr > dr ! = muQ sl dl sr dr where
      muQ : (sl : [ Sl ]) -> [ `IMu' Sl Cl Rl nl sl ] ->
          (sr : [ Sr ]) -> [ `IMu' Sr Cr Rr nr sr ] -> Ty PROP
      muQ sl (con cl fl) sr (con cr fr) =
          ! Cl sl > cl == Cr sr > cr ! &
          `Pi’ (Rl sl cl) \ rl -> `Pi’ (Rr sr cr) \ rr ->
          ! Rl sl cl > rl == Rr sr cr > rr ! =>
          muQ (nl sl cl rl) (fl rl) (nr sr cr rr) (fr rr)

Let’s do this one slowly. Equality between coprograms…

  ! `INu’ Sl Cl Rl nl sl > dl == `INu’ Sr Cr Rr nr sr > dr ! =

…is a simulation relation, indexed by both state-of-world-and-configuration-of-coprogram pairs.

      `INu’ (`Sg’ Sl (`INu’ Sl Cl Rl nl) & `Sg’ Sr (`INu’ Sr Cr Rr nr))

We’re cheerful if the coprograms issue equal commands.

          (sp0 (sp0 \ sl dl -> sp0 \ sr dr ->
              ! Cl sl > command dl == Cr sr > command dr !))

A response is a pair of equal responses for each coprogram. If some little b**tard kicks Mickey in the shin, his sister has to kick Minnie in the corresponding shin.

          (sp0 (sp0 \ sl dl -> sp0 \ sr dr q ->
           `Sg’ (Rl sl (command dl)) \ rl -> `Sg’ (Rr sr (command dr)) \ rr ->
           `Prf’ ! Rl sl (command dl) > rl == Rr sr (command dr) > rr !))

The simulation evolves by evolving both processes.

          (sp0 (sp0 \ sl dl -> sp0 \ sr dr cq -> sp0 \ rl -> sp0 \ rr rq ->
              (nl sl (command dl) rl , continue dl rl) ,
                (nr sr (command dr) rr , continue dr rr) ))

And the simulation starts in the initial configuration for both.

          ((sl , dl) , (sr , dr))

Phew!

  ! `Prf’ y > s == `Prf’ y’ > t ! = `1′
  ! _ > _ == _ > _ ! = `1′

As ever, I postulate the reflexivity of these things, safe in the knowledge that I’m only making extensionally valid assumptions, and that computation on proofs is lazy.

postulate Resp : (S : Ty SET)(P : [ S ] -> Ty SET) ->
        [ `Prf' (funQ S S \ x y -> P x <-> P y) ]
postulate refl : (S : Ty SET)(s : [ S ]) -> [ `Prf' ! S > s == S > s ! ]

Coercion?

What I ought to do now is show how to transport values between equal sets. Given that equality of sets is structural, with covariant twists reflecting the flow of information, we’ve got everything we need. It’s an interesting exercise!

Unfolding

But what I really want to check is that we can see how things unfold. I need a quick helper just to give the code for the set delivered by the out function.

Guts : (S : Ty SET)
    (C : [ S ] -> Ty SET)
    (R : (s : [ S ])(c : [ C s ]) -> Ty SET)
    (n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->
    (s : [ S ]) -> Ty SET
Guts S C R n s = `Sg’ (C s) \ c -> `Pi’ (R s c) \ r -> `INu’ S C R n (n s c r)

And now let’s prove…

conOutLaw : (S : Ty SET)(C : [ S ] -> Ty SET)
    (R : (s : [ S ])(c : [ C s ]) -> Ty SET)
    (n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->
    (s : [ S ])(x : [ `INu' S C R n s ]) ->
    [ `Prf'
    ! `INu' S C R n s > x ==
       `INu' S C R n s > con (command x) (continue x) ! ]

…that everything equals its unfolding. Deep breath.

conOutLaw S C R n s x = unfold

Gosh! What’s the carrier? We need that both sides are in the same state and identified by out.

  (\ sxsx ->
    let sx0 = fst sxsx ; s0 = fst sx0 ; x0 = snd sx0 ;
        sx1 = snd sxsx ; s1 = fst sx1 ; x1 = snd sx1
    in [ `Prf' (! S > s0 == S > s1 ! &
        ! Guts S C R n s0 > out x0 == Guts S C R n s1 > out x1 !) ])

Now, how do we show that this happy situation persists forthwith? First, we get state-configuration pairs, in equal states, and identified by out, so they have equal commands and continues. I get to do a lot of unpacking.

  (\ sxsx scfq ->
    let sx0 = fst sxsx ; s0 = fst sx0 ; x0 = snd sx0
        sx1 = snd sxsx ; s1 = fst sx1 ; x1 = snd sx1
        sq = fst scfq ; cfq = snd scfq
        c0 = command x0 ; c1 = command x1 ; cq = fst cfq
        f0 = continue x0 ; f1 = continue x1 ; fq = snd cfq
    in

The commands are indeed the same!

        cq ,

And given equal responses…

        sp0 \ r0 -> sp0 \ r1 rq ->

…we get equal next-states-of-the-world…

            let n0 = n s0 c0 r0 ; n1 = n s1 c1 r1
                nq = refl (`Pi’ S \ s -> `Pi’ (C s) \ c -> `Pi’ (R s c) \ _ -> S) n
                    s0 s1 sq c0 c1 cq r0 r1 rq

            in nq ,

…and equal continuing processes, as shown by out

                refl (`Pi’ S \ s -> `Pi’ (`INu’ S C R n s) \ _ -> Guts S C R n s)
                    (\ s x -> out x)
                    n0 n1 nq (f0 r0) (f1 r1) (fq r0 r1 rq))

We know our starting situation, and it’s easy to show that our initial conditions are satisfied.

  _ (refl S s , refl (Guts S C R n s) (out x))

Thank goodness for that.

Exercise: use this result to establish a dependent case analysis principle for codata, eliminating over Ty SET.

So what?

So the observational equality setup means that we can work with bisimulation as our substitutive equality for codata. Although our computational presentation of coinduction is weak (plain old unfold, plain old out), reasoning up to bisimulation is enough to recover (and give a suitable evidence language to) the dependent reasoning principles we need. We can plug the gap left by Agda without suffering the subject reduction issue inherent in Coq’s overly intensional presentation. Or, in other words, it works.

Requiem

Would we even be thinking these thoughts without Robin Milner? Rest in peace.

This entry was posted on Monday, March 22nd, 2010 at 6:51 pm and is filed under Observational Type Theory. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.