Spatial Logics allow one to reason about the behaviour and structure of concurrent programs. SLMC is a spatiallogic model checker for pi-calculus processes. As a little exercise I used it for reasoning about Church numerals and processes that operate on them.
In his original work on the pi calculus, Robin Milner defined an encoding of Church numerals, where the number
n is encoded as n outputs on a successor channel, followed by an output on a zero channel, e.g.
Milner also defines some handy processes for doing basic arithmetic:
Note that numbers are ephemeral – they are consumed when being processed. To do anything useful we therefore need a process to duplicate number processes:
Armed with the above we can define a process that calculates the Fibonacci function:
This probably looks incomprehensible at first. It has been optimised to avoid unnecessary copying and roughly corresponds to the following pseudocode
So far we have only defined some simple pi-calculus processes. Now let’s start reasoning about them. First would like to know whether a process represents a number. After a lot of trial-and-error, and consultation with my colleague Francis, I eventually arrived at the following SLMC predicate:
Translated into English this says
A process represents a number if it communicates on two names, symbolically denoted as
- it may do an output on
x, or perform an internal transition,
- after performing an output on
zit may only perform internal transitions and must eventually evolve to nothing,
- after performing an output on
xit must evolve to a process that represents a number,
- it cannot perform an infinite sequence of internal transitions or outputs on
- it may not perform any other actions.
Item 4 and 5 deserve some discussion. Item 4 basically excludes infinity as a number. Item 5 states that we want our processes to be just numbers and nothing else. For example, we would not want a process to behave like a number but also delete all files on our hard
drive. This point sparked some philosophical discussion with my colleague Paul. Specifically, axiomatisation in mathematics usually does not exclude additional behaviours. For example, file-deleting numbers satisfy all the Peano
axioms. Should there be an additional axiom along the lines of “Numbers must not satisfy any
axioms other than the ones stated here”?
Anyway, let’s put our
number predicate to some use:
Feeding these to SLMC all result in success, so 0,1,2,3 really are numbers – hooray! Now for some counter examples of processes that are almost numbers, but not quite:
All the checks fail, as expected.
Finally, let’s check whether the Fibonacci process produces numbers for
certain inputs – or, more precisely, whether the Fibonnaci process,
when composed with certain number processes, evolves into a process
that represents a number:
These all succeed. However, the last check – whether
fib(3) is a number – takes several hours to complete. I know the complexity of the computations performed by SLMC can be quite bad, but I am still at a loss to explain why it would perform so much more badly on
when the check for
fib(2) completes within a few milliseconds.
The reader may wonder why we selected particular examples to test the Fibonacci process, rather than checking whether it evolves to a number for any given input number. To express such a test we need the spatial logic’s guarantee operator,
|>, and then could write:
Is Fibonacci a process that when composed with a process that is a
number, is a number?
Unfortunately, SLMC does not support the guarantee operator. There is a good reason for that. The expressiveness of the logic must be finely tuned in order for model checking of interesting properties to be decidable for interesting processes. Introducing the guarantee operator makes model checking undecidable for most interesting processes.