[Iris-Club] Frame-preserving update and double-negation
jtassaro at andrew.cmu.edu
Wed Aug 24 01:04:38 CEST 2016
Inspired by the recent discussion about classical separation logic, I
was wondering about the following. In Iris 3.0, there is a new modality
called "rvs", written "|=r=>", where |=r=> P n x holds if we can do a
frame-preserving update which changes x into a resource that satisfies P.
It is not hard to show that (P -* False) -* False implies |=r=> P. In
addition, if (a) P is timeless, (b) the underlying CMRA is discrete, and
(c) your meta-logic is classical, you can show that |=r=> P entails (P
-* False) -* False.
So, now I have two questions:
(a) Does anyone know of a way to characterize |=r=> P as (P -* Q) -* Q
for some (simple) Q in the more general case where P is not timeless and
the CMRA is not discrete? Ideally, Q should be definable using the other
(b) Would anything break if we replaced all uses of |=r=> P with (P -*
False) -* False in the Iris 3.0 model?
This is purely idle curiosity.
P.S. What is "rvs" supposed to stand for?
More information about the Iris-Club