[Agda] Re: Adding (inductive) transitivity to weak bisimilarity not sound?

[Edsko de Vries]

On Tue, Sep 1, 2009 at 5:05 PM, Nils Anders Danielsson <nad at cs.nott.ac.uk>wrote:

> On 2009-09-01 15:45, Edsko de Vries wrote:
>
>> On Tue, Sep 1, 2009 at 2:59 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk
>> >wrote:
>>
>>> It is sound but useless.
>>>
>>
>> Then I clearly don't understand the rules for mixed inductive/coinductive
>> definitions. Is
>>
>>   inductive_constructor (..) (coinductive_constructor (coinductive
>> recursive call))
>>
>> a valid call or not?
>>
>
> It is (currently, in Agda). I think you and Thorsten interpret the word
> "sound" differently here.
>

Right. So, we have a relation R (weak bisimularity), which is provably
transitive. Then, we can give a definition of a similar relation R' which is
like R except that it has an extra, inductive, transitivity rule. This is
"useful" in the sense that a proof which was previously

  transitivity_lemma (...) (coinductive_constructor (...)
coinductive_recursive_call))

and was rejected because the coinductive_recursive_call was not guarded  can
now be replaced by

  transitivity_constructor (...) (coinductive_constructor (...)
coinductive_recursive_call))

which *is* guarded. It is not "sound" in the sense that R' is larger than R.

I find this counter-intuitive because I would have thought that adding an
inductive transitivity rule to a provably transitive relation would not
change anything. Again, it strongly reminds me of the problem of weak
bisimulation up to weak bisimilarity (see "*Techniques of weak bisimulation
up-to", *R.Milner and D. Sangiorgi).

Edsko
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090901/5c46aca5/attachment.html