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.
Linear Temporal Logic takes the basic ideas of Propositional and Predicate logic and introduces concepts about time.
Predicate logic is widely used for automatically checking and proving theorems, verifying software correctness and security, and is the foundation of the programming language ProLog.
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
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
There are more sophisticated operators too, such as
A Until B or A U B, which means
A is true until
B is true,
Eventually B. This can be written recursively as A U B ≡ B∨(A∧◇B∧◯(A U B)). There is also a weaker version
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
B are types then A∧B can be written the pair
(A,B), A∨B can be written as
Either A B, and
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
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
Forever (Int, Int) for mouse position,
Eventually Bytestring for receiving network data,
Char `Until` Nothing for standard input.
Evan Czaplicki's Paper goes over the many 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.