<div dir="ltr">Another point is that, "wp is defined as the fixed-point of a contractive function," but I am not sure there is "the" fixed-point.  Previously in the documentation it is only said that a contractive function has "a" fixed-point.<div><br></div><div>- Is it indeed "the" fixed-point"?</div><div>- If not, in what sense a chosen fixed-point is canonical?<br><div><br></div><div>Thank you,</div><div>Jeehoon</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">2016-08-20 23:02 GMT+09:00 Jeehoon Kang <span dir="ltr"><<a href="mailto:jeehoon.kang@sf.snu.ac.kr" target="_blank">jeehoon.kang@sf.snu.ac.kr</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I think I almost understand `pre-wp` ;-)  But I still cannot understand the use of step-index: may I ask what is the intuition behind requiring `m+1 \in ...` for the value case?  I think I understand why you required `m in ...` in the reduction case, since there is actually a step.  But for the value case, I am not sure why it is necessary to demand `m+1 \in ...`.  Why `m \in ...` is not enough?<div><br></div><div>Thank you,</div><div>Jeehoon</div></div><div class="gmail_extra"><div><div class="h5"><br><div class="gmail_quote">2016-08-19 21:14 GMT+09:00 Ralf Jung <span dir="ltr"><<a href="mailto:jung@mpi-sws.org" target="_blank">jung@mpi-sws.org</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<span><br>
> But I am still confused of the definition of `pre-wp`..  In the 2nd<br>
> line, `s` should have the type ∆(Val), mandated by `ϕ(s)`; and yet at<br>
> the same time `s` should have the type Res, from `s · rf`.  May I ask if<br>
> what am I missing here?<br>
<br>
</span>Right, that should have been ϕ(v)(s). Then things hopefully make sense...<br>
<div><div><br>
Kind regards,<br>
Ralf<br>
<br>
--<br>
<a href="mailto:iris-club@lists.mpi-sws.org" target="_blank">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/list<wbr>info/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank">iris-club-unsubscribe@lists.mp<wbr>i-sws.org</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div></div></div><span class="">-- <br><div data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</span></div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div>