At Matrix AI our research into language constructs for formally describing distributed systems has led us to a concept called Linear Temporal Logic. It is a logic system that allows us to express logical statements about time. This article will provide a brief introduction to this logic system.
In Linear Temporal Logic (LTL), we can express statements about things that are true. Our expression will have both English word variants and also operator variants. The simplest statement is simply
A. This means that
A is true right now. We can also write that
A will be true from now on and to the future, and that can be expressed as
Forever A or □A. If
A will be true eventually, we can write
Eventually A or ◇A. Notice that
Not Forever Not A is the same as
Eventually A or ¬□¬A≡◇A. This is because if
A won't always be false then
A will eventually be true. If we model time as discrete moments, we can say that
A will be true in the next moment, and write it as
Next A or ◯A.
There are more sophisticated operators too, such as
A Until B or A U B, which means
A is true until
B is true, and
Eventually B. This can be written recursively as A U B ≡ B∨(A∧◇B∧◯(A U B)). There is also a weaker version of
Until, denoted A W B, where
B need not occur. We can write A W B ≡ □A ∨ (A U B).
There is a strong parallel between Propositional Logic and Functional Programming. Let's use Haskell as an example. If the formulas
B are types then A∧B can be written the pair
(A,B), A∨B can be written as
Either A B, and if
B, we use the function type
A -> B. Now function application looks like Modus Ponens, the distributivity laws look like alternative representations of the same types, and formal proofs look like Haskell programs.
As for the modal operators of linear temporal logic, we have to look at Functional Reactive Programming.
Forever A is an unending stream of values of type
Eventually A is a container that will eventually yield a value of type
A Until B is a stream of type
A terminated with a value of type
B. Using these types, IO operations can have types like
Forever (Int, Int) for mouse position,
Eventually Bytestring for receiving network data, and
Char `Until` Nothing for standard input.
Evan Czaplicki's Paper goes over the many different attempts to implement Functional Reactive Programming. However, for distributed systems, a complete functional reactive language is unnecessary. Instead, we can learn from Arrowised FRP, and model processes as Signal Functions. This model may help us describe the distributed services that Matrix is orchestrating.