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

Robbert Krebbers mail at robbertkrebbers.nl
Mon Aug 22 09:10:47 CEST 2016

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

```