[Agda] Codata oddity

[Anton Setzer]

Nils Anders Danielsson wrote:
> On Sat, Jun 7, 2008 at 2:06 AM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>   
>> In my opinion it is important to keep here a clear connection with
>> category theory [...]
>>     
>
> What you describe seems to be restricted to non-dependent pattern
> matching; you have
>
>   case : Conat -> ConatCases
>
> rather than
>
>   case : (n : Conat) -> ConatCases n.
>
> Do you have any ideas about how to beef this up to a more dependent
> setting ("coinductive families")? Or are we restricted to "restricted
> coinductive families", which I think your current approach allows?
>
> Restricting pattern matching on codata to be non-dependent would solve
> the particular problem that I posted before, by the way. Maybe it
> would even reestablish type preservation. However, I would prefer a
> solution which enables the use of full coinductive families, if this
> is possible.
>
>   
I think the work of Peter Hancock and myself gives an information about what
dependent coalgebras are.
We considered state dependent programs which are weakly final coalgebras
of functors of the form

F : (S -> Set) -> (S -> Set)
where
F(X,s) = Sigma c: C(s). (r : R(s,c) ) -> X(n(s,c,r))
where
S : Set (the set of states
C : S -> Set  (the set of commands of an interactive program depending
on the
      state the program is in)
R : (s: S, C(s)) -> Set  (the set of responses to this command)
n : (s : S, c: C(s), R(s,c)) -> S
           (the next state one reaches after an interaction with c:
C(s), r: R(s,c) has taken place.

If we translate this into my coalg notation we get definitions of the form

coalg  F* : S -> Set where
    F* : (s : S, x : F* s) ->  Sigma c: C s. (r : R s c) -> F* (n s c r)

more generally we can have

coalg F* : S -> Set where
   F* : (s : S, x : F* s) -> A(s,x)

where A is a set depending on s and x and which is strictly positive in F*

This gives rise to coinductive families in the sense of Peter hancock's
email,
or restricted coinductive families in the sense of the work by myself
and Peter Dybjer.

  Typically A as above needs to be defined by case distinction on s,
which amounts typically
to a mutual definition.
For instance we can define bisimulation on coNat as

mutual
   coalg _bisim_ : coNat -> coNat -> Set where
       _* : n bisim m -> C n m
   C : coNat -> coNat -> Set
   C  (~ Z) (~ Z) =   True
   C  (~ (S n)) (~ (S m)) = n bisim m
   C (~ _)  (~ _)              = False

where True is the one element set and False is the empty set.

Here I am using a new notation for pattern matching on codata,
which I will explain in a next email.

However, the following is maybe in fact better:


mutual
    _bisim_ : coNat -> coNat -> Set
    (~ Z)  bisim  (~ Z) = bisimZ
    (~ (S n)) bisim (~ (S m)) = n bisimS m
    (~ _ ) bisim (~ _)  = bisimEmpty

    coalg bisimZ : Set where
         _* : bisimZ -> True

    coalg _bisimS_ : coNat -> coNat -> Set where
         _* : n bisimS m -> n bisim m
 
    coalg bisimEmpty : Set where
         _*  : bisimEmpty -> False

I don't know how to play the game if we want to get a
codata version of bisim

I don't know how to translate something like

codata _bisim_ : coNat -> coNat -> Set where
    pZ : (~ Z) bisim (~ Z)
    pS : (n m : coNat) -> n bisim m ->  ~ (S n)  bisim ~ (S m)

because I don't know what the type of pZ  and pS is.


But the following


mutual
   _bisim_ : coNat -> coNat -> Set where
   (~ Z) bisim (~ Z) = bisimZ
   (~ (S n)) bisim (~ (S m)) = n bisimS m
   (~ _) bisim (~ _) = bisimFalse
 
   codata bisimZ : Set where
       pZ : bisimZ

   codata _bisimS_ : coNat -> coNat -> Set where
        pS : n  bisim m -> n bisimS m

   codata bisimFalse where


seems to me an acceptable definition which translates into the
following:

mutual
   _bisim_ : coNat -> coNat -> Set where
   (~ Z) bisim (~ Z) = bisimZ
   (~ (S n)) bisim (~ (S m)) = n bisimS m
   (~ _) bisim (~ _) = bisimFalse

   coalg bisimZ : Set where
         _* : bisimZ -> bisimZ'
 
   data bisimZ' : Set where
         pZ' : bisimZ'

    coalg _bisimS_ : coNat -> coNat -> set where
         _* : n bisimS m -> n bisimS' m

    data _bisimS'_ : coNat -> coNat -> Set where
          pS' : n bisim m -> n bisimS' m

    coalg bisimFalse : Set where
        _* :  bisimFalse -> bisimFalse'

    data bisimFalse' : Set where
         
pZ : bisimZ where
pZ *  = pZ'

pS : n bisimS m -> n bisimS' m where
(pS q) * = pS' q


I don't know whether it makes sense to talk about
general indexed coalgebras or codata type.


Anton




   






-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
 
                    
  

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080608/9fba8060/attachment.html