[Agda] Partiality/delay monad

[Guillaume Allais]

Thanks! That's a lot of content!

I haven't implemented anything regarding weak bisimilarity yet because
it's notoriously hard. One thing I'm wondering as a complete newcomer
is whether it'd make sense to have a stricter notion of proofs of weak
bisimilarity and then recover some of the current constructor's types
as lemmas.

E.g. (reusing your notations, forgetting about the very general setting
for the moment) would it make sense to have:

  data [_]_≈_ (i : Size) :
           Delay A ∞ → Delay A ∞ → Set a where
      now    : ∀ {k x} → [ i ] now x ≈ now x
      later  : ∀ {k x y} →
               [ i ] force x ≈′ force y →
               [ i ] later x ≈ later y
      later-now : ∀ {k x y} →
               [ i ] force x ≈ now y →
               [ i ] later x ≈ now y
      now-later : ∀ {x y} →
               [ i ] now x ≈ force y →
               [ i ] now x ≈ later y

? Have you experimented with such a definition in the past?

Cheers,
--
gallais

On 20/03/18 11:37, Nils Anders Danielsson wrote:
> On 2018-03-08 14:20, Guillaume Allais wrote:
>> I have pushed a first few modules to the codata branch to start the
>> discussion one of which is Codata.Delay:
>> https://github.com/agda/agda-stdlib/blob/codata/src/Codata/Delay.agda
>
> Feel free to port parts of my library (git clone
> http://www.cse.chalmers.se/~nad/repos/delay-monad/).
>
> Note that an important feature of/problem with the delay monad is that
> transitivity is not fully size-preserving for weak bisimilarity and
> expansion. I have proved that a number of variants of transitivity
> cannot be implemented:
>
>  
> http://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.Bisimilarity.Negative.html
>
> However, some variants can be implemented:
>
>  
> http://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.Bisimilarity.html
>
> The standard library's equational reasoning framework was not designed
> to handle "heterogeneous" forms of transitivity. I have experimented
> with a more general framework:
>
>  
> http://www.cse.chalmers.se/~nad/listings/up-to/Equational-reasoning.html
>
> However, I am not entirely happy with it. Too much overloading can make
> code harder to read and harder for Agda to type-check. In the
> delay-monad library I defined a set of combinators that is used only for
> strong and weak bisimilarity and expansion.
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180320/091588e7/attachment.sig>