[Iris-Club] Intention of later(False) in timeless predicate

[Robbert Krebbers]

Hi Jeehoon,

think of timeless as being invariant under the step-indexes. 
Semantically that means (ignoring resources):

   Timeless P := ∀ n, P 0 → P n

So, now let's think how we could describe that in the logic. An obvious 
guess would be:

   Timeless P := ▷ P ⊢ P

However, this is wrong. Take a look at the following:

        0      1      2      3
   ▷ P  True   P(0)   P(1)   P(2)
   P    P(0)   P(1)   P(2)   P(3)

As you see here, step-index 0 is problematic. According to the semantic 
definition, False would be timeless, but ▷ False ⊢ False does not hold 
at step-index 0.

So, what we somehow would like to do is to "exclude" the 0th step-index, 
and that's where the disjunction with ▷ False comes in:

                0      1      2      3
   ▷ P          True   P(0)   P(1)   P(2)

   P            P(0)   P(1)   P(2)   P(3)
   ▷ False      True   False  False  False
   P ∨ ▷ False  True   P(1)   P(2)   P(3)

Hope this helps.

Robbert

On 08/22/2016 07:00 AM, Jeehoon Kang wrote:
> Dear Iris Club,
>
> In the Iris 2.0 documentation, the timeless predicate is defined as
> follows (page 11):
> Γ |- timeless(P) <=> Γ | later(P) |- P ∨ later(False)
>
> I guess the intention of the later(False) disjunct is allowing more
> predicates to be timeless.  But I am not sure which rule of "Laws for
> the later modality" (page 14) requires the later(False) disjunct.  May I
> ask is it really used?
>
> Thank you,
> Jeehoon
>
> --
> 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>
>
>