[Agda] Re: Classical Mathematics for a Constructive World

[Ramana Kumar]

On Sun, Dec 2, 2012 at 10:10 AM, Jan Burse <janburse at fastmail.fm> wrote:

> wren ng thornton schrieb:
>
>  You run into similar issues in separation logic. When using Hoare
>> separation logic we get this nice frame rule:
>>
>>      {P}   C {Q}
>>      -------------
>>      {P*R} C {Q*R}
>>
> >
> > (subject to some mild side conditions about R). People often focus on >
> the fact that the addition of R is preserved from precondition to
> > postcondition
>
> Correctness wise I guess the above inference
> rule is in most cases invalid. Take the following
> example:
>
>    { x = 0 v x = 1 }
>    x = x + 1
>    { x = 1 v x = 2 }
>
> Now add the condition x = 0:
>
>    { x = 0 }
>    x = x + 1
>    { false }
>
> What it needs is x = a & x = b -> false
> for a <> b. Should be possible in minimal
> logic without any choice principle. Its
> would be for example part of CET (Clark
> Equational Theory). So I guess it is not
> related. But I might be wrong.
>
> Or what would be the mild condition on R
> to make the inference rule meaningful?
>

The condition is that R does not mention any variables assigned in C.


>
> Bye
>
>
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121202/05ccceda/attachment.html