[Iris-Club] pre-wp's definition: s, s1, and s2

[Robbert Krebbers]

I just proved this in Coq:

   https://gitlab.mpi-sws.org/FP/iris-coq/commit/738d8bcc

The tutorial said it was easy, and it indeed turned out to be easy :).

On 08/21/2016 09:03 AM, Lars Birkedal wrote:
> Dear Jeehon,
>
> The fixed point is unique, see 5.10 in the tutorial notes:
>
>  http://cs.au.dk/~abizjak/documents/publications/categorical-logic-tutorial-notes.pdf
> <http://cs.au.dk/%7Eabizjak/documents/publications/categorical-logic-tutorial-notes.pdf>
>
> Best,
> Lars.
>
>> On 20 Aug 2016, at 16:22, Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr
>> <mailto:jeehoon.kang at sf.snu.ac.kr>> wrote:
>>
>> 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.
>>
>> - Is it indeed "the" fixed-point"?
>> - If not, in what sense a chosen fixed-point is canonical?
>>
>> Thank you,
>> Jeehoon
>>
>> 2016-08-20 23:02 GMT+09:00 Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr
>> <mailto:jeehoon.kang at sf.snu.ac.kr>>:
>>
>>     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?
>>
>>     Thank you,
>>     Jeehoon
>>
>>     2016-08-19 21:14 GMT+09:00 Ralf Jung <jung at mpi-sws.org
>>     <mailto:jung at mpi-sws.org>>:
>>
>>         Hi,
>>
>>         > But I am still confused of the definition of `pre-wp`..  In the 2nd
>>         > line, `s` should have the type ∆(Val), mandated by `ϕ(s)`; and yet at
>>         > the same time `s` should have the type Res, from `s · rf`.  May I ask if
>>         > what am I missing here?
>>
>>         Right, that should have been ϕ(v)(s). Then things hopefully
>>         make sense...
>>
>>         Kind regards,
>>         Ralf
>>
>>         --
>>         iris-club at lists.mpi-sws.org
>>         <mailto:iris-club at lists.mpi-sws.org> - Mailing List for the
>>         Iris Logic
>>         Management: https://lists.mpi-sws.org/listinfo/iris-club
>>         <https://lists.mpi-sws.org/listinfo/iris-club>
>>         Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>>         <mailto:iris-club-unsubscribe at lists.mpi-sws.org>
>>
>>
>>
>>
>>     --
>>     Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
>>     Software Foundations Laboratory <http://sf.snu.ac.kr/>
>>     Seoul National University <http://www.snu.ac.kr/>
>>
>>
>>
>>
>> --
>> Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
>> Software Foundations Laboratory <http://sf.snu.ac.kr/>
>> Seoul National University <http://www.snu.ac.kr/>
>> --
>> iris-club at lists.mpi-sws.org <mailto:iris-club at lists.mpi-sws.org> -
>> Mailing List for the Iris Logic
>> Management: https://lists.mpi-sws.org/listinfo/iris-club
>> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>> <mailto:iris-club-unsubscribe at lists.mpi-sws.org>
>
>
>