<div class="gmail_extra"><div class="gmail_quote">On Sun, Dec 2, 2012 at 10:10 AM, Jan Burse <span dir="ltr">&lt;<a href="mailto:janburse@fastmail.fm" target="_blank">janburse@fastmail.fm</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

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


<br>
Bye<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>