Sebastian Hanowski | 24 Jul 17:12 2007
Picon

Odelay


         Been playing with  the partial monad a little  longer. Tried to
        use it  for making the  equations of  section 3.4 of  these nice
        lecture notes

                http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf

        hold /definitionally/.

>       {-# OPTIONS -fglasgow-exts #-}

        Given the suitable codata to capture divergence

> {-co-}data D a = Now a | Later (D a) ; never = Later never    

        we  can   not  only  'race'   two  or  (infinitely   many)  more
        computations against each other

>       Now a   \/ _       = Now a
>       _       \/ Now a   = Now a
>       Later d \/ Later e = Later (d \/ e)

        but also 'sync' two or finitely more of them.

>       Now a     /\ Now _     = Now a
>       a <at> (Now _) /\ Later d   = Later (a /\ d)
>       Later d   /\ a <at> (Now _) = Later (d /\ a)
>       Later d   /\ Later e   = Later (d /\ e)

        By  quotienting with  respect to  termination we  can have  this
(Continue reading)


Gmane