[Iris-Club] pre-wp's definition: s, s1, and s2
Jeehoon Kang
jeehoon.kang at sf.snu.ac.kr
Sat Aug 20 16:22:48 CEST 2016
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>:
> 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>:
>
>> 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 - Mailing List for the Iris Logic
>> Management: https://lists.mpi-sws.org/listinfo/iris-club
>> Unsubscribe: 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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160820/e7c7c258/attachment.html>
More information about the Iris-Club
mailing list