The * is not just conjunction, it is separating conjunction.<br>Maybe you know that already, but just to make sure, the semantics of P * R is<br>(P * R)(x,h) = exists h1. exists h2. h = h1 + h2 & P(x,h1) & R(x,h2)<br>
where + is disjoint union.<br>The choice issue is that the h2 for R on the Q * R side doesn't have to be the same.<br><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Dec 2, 2012 at 10:41 AM, Jan Burse <span dir="ltr"><<a href="mailto:janburse@fastmail.fm" target="_blank">janburse@fastmail.fm</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Jan Burse schrieb:<div class="im"><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Or what would be the mild condition on R<br>
to make the inference rule meaningful?<br>
</blockquote>
<br></div>
Ramana Kumar just wrote me:<div class="im"><br>
> The condition is that R does not mention any<br>
> variables assigned in C.<br>
<br></div>
Then I also wonder how this is related to choice<br>
principles. I see that it is related to variable<br>
occurence rules. So if I desugar the following:<br>
<br>
{ P } C { Q }<br>
<br>
I get:<br>
<br>
P(x,z) -> forall y (C(x,y) -> Q(y,z))<br>
<br>
Question is now whether this implies:<br>
<br>
P(x,z)&R(z) -> forall y(C(x,y) -> Q(y,z)&R(z))<br>
<br>
I guess the answer is affirmative already in<br>
minimal logic. But I might be also wrong here.<div class="HOEnZb"><div class="h5"><br>
<br>
Bye<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>