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

Lars Birkedal birkedal at cs.au.dk
Sun Aug 21 09:03:50 CEST 2016

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

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
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>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160821/7d20a045/attachment.html>