LShift Ltd.

Nothing But a Number

April 5th, 2006 matthias

Spatial Logics allow one to reason about the behaviour and structure of concurrent programs. SLMC is a spatial logic model checker for pi-calculus processes. As a little excercise I used it for reasoning about Church numerals and processes that operate on them.

Numbers as Processes

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.

defproc N0(x,z) = z!();
defproc N1(x,z) = x!().z!();
defproc N2(x,z) = x!().x!().z!();
defproc N3(x,z) = x!().x!().x!().z!();

Milner also defines some handy processes for doing basic arithmetic:

defproc Succ(x,z,y,w) = y!().Copy(x,z,y,w)
and Copy(x,z,y,w) =
  select {
    x?().Succ(x,z,y,w);
    z?().w!()
  };

defproc Add(x1,z1,x2,z2,y,w) =
  select {
    x1?().y!().Add(x1,z1,x2,z2,y,w);
    z1?().Copy(x2,z2,y,w)
  };

Note that numbers are ephemeral - they are consumed when being processed. To do anything useful we therefore need a process to duplicate number processes:

defproc Double(x,z,y1,w1,y2,w2) =
  select {
    x?().new y1_,w1_,y2_,w2_ in (
           Succ(y1_,w1_,y1,w1) |
           Succ(y2_,w2_,y2,w2) |
           Double(x,z,y1_,w1_,y2_,w2_));
    z?().(w1!() | w2!())
  };

Armed with the above we can define a process that calculates the Fibonacci function:

defproc Fib(x,z,y,w) =
  select {
    z?().w!();
    x?().select {
      z?().y!().w!();
      x?().new x0,z0,x1,z1,x2,z2,y1,w1,y2,w2 in (
        Double(x,z,x0,z0,x1,z1) |
        Succ(x0,z0,x2,z2) |
        Fib(x1,z1,y1,w1) |
        Fib(x2,z2,y2,w2) |
        Add(y1,w1,y2,w2,y,w))
    }
  };

This probably looks incomprehensible at first. It has been optimised to avoid unnecessary copying and roughly corresponds to the following pseudocode

fib(x) {
  if (x-- == 0) return 0;
  else if (x-- == 0) return 1;
  else return fib(x) + fib(x+1);
}

What is a Number?

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:

defprop number(x,z) =
  minfix X.((<z!>true or <x!>true or <tau>true) and
            [z!]allTau and [x!]X and [tau]X and
            forall n.(n==z or n==x or [n]false));

defprop allTau =
  minfix X.((void or <tau>true) and
            [tau]X and forall n.[n]false);

Translated into English this says

A process represents a number if it communicates on two names, symbolically denoted as x and z, s.t.

1. it may do an output on z or x, or perform an internal transition,
2. after performing an output on z it may only perform internal transitions and must eventually evolve to nothing,
3. after performing an output on x it must evolve to a process that represents a number,
4. it cannot perform an infinite sequence of internal transitions or outputs on x,
5. 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:

check N0(x,z) |= number(x,z);
check N1(x,z) |= number(x,z);
check N2(x,z) |= number(x,z);
check N3(x,z) |= number(x,z);

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:

defproc Infinity(x,z) = x!().Infinity(x,z);
defproc ErraticNumber1(x,z) =
  select {
    x!().(e!() | ErraticNumber1(x,z));
    z!()
  };
defproc ErraticNumber2(x,z) = x!().(e!() | z!());
defproc ErraticNumber3(x,z) =
  select {
    x!().(e!() | z!());
    z!()
  };
defproc ErraticNumber4(x,z) =
  select {
    x!().(e!() | e?() | z!());
    z!()
  };
defproc ErraticNumber5(x,z) =
  select {
    x!().z!();
    z!().(e!() | e?())
  };

check Infinity(x,z) |= number(x,z);
check ErraticNumber1(x,z) |= number(x,z);
check ErraticNumber2(x,z) |= number(x,z);
check ErraticNumber3(x,z) |= number(x,z);
check ErraticNumber4(x,z) |= number(x,z);
check ErraticNumber5(x,z) |= number(x,z);

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:

defproc Fib0 = new x,z in (N0(x,z) | Fib(x,z,y,w));
defproc Fib1 = new x,z in (N1(x,z) | Fib(x,z,y,w));
defproc Fib2 = new x,z in (N2(x,z) | Fib(x,z,y,w));
defproc Fib3 = new x,z in (N3(x,z) | Fib(x,z,y,w));

check Fib0 |= number(y,w);
check Fib1 |= number(y,w);
check Fib2 |= number(y,w);
check Fib3 |= number(y,w);

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 fib(3) when the check for fib(2) completes within a few milliseconds.

There is no Guarantee

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:

check Fib(x,z,y,w) |= number(x,z) |> number(y,w)

which says

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.

Entry Filed under: Technology