Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle - Correct System Design: Recent Insights and Advances - page 16

But even this is only a small subset of the number of transition rules that would
be needed to achieve communication in all circumstances. A much easier way to
deal with all cases is to just postulate that

j is a commutative operator, that it

is associative, and that it has unit 0.

P j 0 = P

P j Q = Q j P

P j Q j R Pj QjR

) 1

( )= (

These are called structural laws in a process calculus. They represent the mobility
of process, because the implementation may use the equations for substitution
in either direction, and so move a process around until it reaches a neighbour
capable of an interaction with it. In a bottom-up presentation, these laws are
just postulated as axioms that dene a particular calculus; they can be used in
the proof of other theorems, but they themselves are not susceptible of proof,
because there is no semantic basis from which such a proof could be constructed.
The laws governing reduction apply only to complete programs; and they
need to be extended to allow reduction steps to take place locally within a
larger context. For example a local reduction can occur anywhere within a larger
parallel network, as stated by the rule

If P ! P 0 then ( P j Q ! P 0 j Q

) ( )

A similar law applies to hiding.

P ! P 0 then ( new e) P 0 . If P ! ( new e)

But there is no similar rule for e:P: A reduction of P is not permitted until

after has happened. It is only this omission of a rule that permits terminating

programs to be distinguished from non-termination.
One of the main objectives of a theory of programming is to model the
behaviour of computing systems that exist in the world today. The world-wide
network of interconnected computers is obviously the largest and most important
such system. Any of the connected computers can emit a communication into
the network at any time. There is reasonable assurance that the message will
be delivered at some later time at some destination that is willing to accept it
(if any). But the exact order of delivery does not necessarily reflect the order
of sending: messages in the net can overtake each other. This aspect of reality
is very simply encoded in the calculus by adding a single new reduction step.
This just detaches a message from its sender, and allows the message to proceed
independently in its own timescale through the network to its destination.

e

e:P ! ( e: 0) j P

1 These equations are more usually written with equivalence ( ) in place of equal-
ity, which is reserved for syntactic identity of two texts. They are called structural
congruences , because they justify substitution in the same way as equality.