24 Jul 2007 17:12
Odelay
Sebastian Hanowski <seha <at> informatik.uni-kiel.de>
2007-07-24 15:12:08 GMT
2007-07-24 15:12:08 GMT
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)
RSS Feed