Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I got lost at Next diagram:

   next P : ●ー○ー○

   P      : ○ー●ー○
Is the P in the 2nd row meant to represent “P after evaluating next(P)”?


Each circle represents a state. A filled circle represents the formula to be true in that state.

Here P is true in state 2, then false subsequently. So in state 1, the formula "next P" is true. "next P" is false in state 2, because P is false in state 3.


Does the “next P” of row 1 refer to:

a) the 2nd dot in the 1st row?

b) the entire 2nd row?


(a)


Shouldn’t it then be:

    next P : ●ー●ー○

?


No. It should be:

              1  2  3

   P          ●  ●  ○

   (next P)   ●  ○  ○
All formulae share the same timeline in terms of state numbering.

In non-temporal logic, all operators operate on the values at a single time. So, when we say "P and Q", or "not P", these implicitly all apply to some state i.

Temporal logic adds "next", which links a state i to the state i+1. (next P) in state i refers to the value of P in state (i+1). (always P) refers to states (i ... inf).

In this example, the value of (next P) in state 2 must be false, because it refers to P's value in state 3.


I can comprehend your interpretation of ‘next’; it is algebraic: For all states ‘i’: ‘next P’ is true for state ‘i’, if P is true for state ‘i+1’.

The article seems to have a side-effect based interpretation rather than an algebraic one. It seems that ‘next P’ updates the state state of ‘P’. Hence the different diagram.


Yes it is the "next state" of P after applying the function




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: