technology from back to front

Nothing But a Number

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.

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.

by
matthias
on
05/04/06
  1. Matthew Sackman
    on 08/04/06 at 12:48 pm

    The examples given here seem, at first glance, to be expressible in HML. Given that the guarantee operator |> isn’t supported in the model checker, are there other parts of Spatial Logics that give more power than HML that are supported by SLMC?

    Do spatial logics reduce to SHML or WHML and are respectful? Or is there a more complex relationship between the logics? Certainly the modal operators look right out of SHML – are there [[cond]] and <> equivalents of WHML too?

    Amusing to see defproc again after all these years – last seen in BBC BASIC!

  2. Gah, silly HTML – I meant [[cond]] and <<cond>> in the above…

  3. The examples given here seem, at first glance, to be
    expressible in HML.

    The example doesn’t require the use of any of the spatial operators of the logic, so I supect they may well be expressible in HML.

    are there other parts of Spatial Logics that give more
    power than HML that are supported by SLMC?

    Yep. All the spatial operators. See the SLMC papers/manual for details.

  4. Greg Meredith pointed me towards Mads Dam‘s work on Proof Systems for pi-calculus Logics, which contains a number predicate in a more standard HML that looks very similar to mine. The differences are interesting:

    • Mads’ number processes are “located” at a single channel, whereas I use Milner’s original and simpler un-located encoding. The added complexity is reflected in Mad’s formula Nat0 on page 15. The rest is dealt with in Nat1, which corresponds very closely to my formula.

    • My formula fails to ensure that a number process must not simultaneously enable x and z transitions. Consider a process that duplicates such a number, e.g. using Double. The resulting number processes are not guaranteed to represent the same number, which is clearly undesirable. That is easy to fix by adding a condition not (<z!>true and <x!>true) to the number predicate.

    • Mads’ formula fails to ensure that after the z transition a number process should not be able to do anything other than tau transitions, and must eventually terminate. That is easy to fix.

    • Mads’ formula disallows processes that can do a (finite) number of tau transitions during which n and z are disabled. I think that is wrong, but it is a matter of opinion and easy to change either way.

 
 


eight − 2 =

Search

Categories

Feeds

2000-14 LShift Ltd, 1st Floor, Hoxton Point, 6 Rufus Street, London, N1 6PE, UK+44 (0)20 7729 7060   Contact us