The breakthrough Ohad Asor achieved with the guarded successor second order time compatible logic is under recognized. So in this blogpost I want to breakdown the key formula which explains exactly how it works, while also addressing at a high level what it is.
The GSSOTC is essentially the temporal logic for formal specifications. It is this temporal logic which allows for the specification of programs through the Tau Language. The TC means time compatible which has a very specific meaning in logic, but I'll give the basic understanding, which is to say that we want a logic which guarantees a causal relationship between program states through time, where each program state mapped in time only depends on the previous state.
Universal Quantification: For all pairs n and k.
Successor Relation s(n,k): If k is the successor of n.
Implication →: Then the condition φ involving values x(n), x(k), y(n), and y(k) must hold.
So what exactly is n and k? For people who aren't logicians what we are looking at is the state transition. We can think of this as like the map through time for the sequence of program states. In most cases the sequence of possible program states is finite rather than infinite, but in the case of GSSOTC as long as you maintain causality, as long as the future state depends on the previous state, as long as it's time compatible, you can accommodate for infinite state transitions. This as far as I know is quite a unique property.
Quantification: ∀nk
This quantifies over all pairs of time points n and k.
Successor relation: s(n,k)
This defines k as the immediate successor of n.
Implication: →
This sets up the relationship between the successor relation and the state transition.
State transition: φ(x(n),x(k),y(n),y(k))
This describes how the state (represented by x and y) changes from time n to time k. In addition, this can be an infinite amount of transitions as there is no upper bound put on the state transitions.
I asked the development team in the last Q&A how they intend to manage the inevitable problem of state explosion. Their answer was enlightening. David said the plan is to use BDDs, memory maps, normalization and simplification. In other words it's a means of reducing the possibilities and narrowing the solution space, by using more effective data structures. We can think of the use of BDDs as a sort of compression tactic to preserve memory. Normalization increases the efficiency so memory is not wasted.
GSSOTC is the key logic for program specification. NSO (Nullary Second Order) logic is what allows Tau sentences to speak about itself. The two variable fragment with counting is what allows for knowledge representation and reasoning. CNL (Controlled natural languages) can be seen as a sort of syntatic sugar, it makes the logic formulas more human readable. When we have all of this combined we have Tau Language in a complete form, and I intend to develop on it.
