Joachim Parrow
                                                         Pi-calculus note JP15
                                                         20 Oct 1999

 On the relationship between two proof systems for the pi-calculus
 -----------------------------------------------------------------

Background
----------

The following note fills a small gap in the known results about
axiomatisations in the pi-calculus, and the technique may have some
general interest. It also substantiates a claim about axiomatisation
of weak congruences made in my recent "An Introduction to the
pi-calculus".

There are two kinds of axiomatisations of pi:

1. The systems developed notably by Huimin Lin and Matthew Hennessy, where
judgements are of the kind

  C |> P = Q

meaning "under the condition C it holds that P=Q". In the following I
shall use the proof system including Mismatch in "Complete inference
systems for weak bisimulation in the pi-calculus" by Lin, and refer to
it as "Lin's system"; whenever a judgement of kind C |> P = Q is
presented it means derivability in Lin's system. I shall refer to the
proof rules by the names in that paper.

Lin's system has been shown to be complete for late and early strong
and weak congruence. Adding the three standard tau-laws means moving
from strong to weak, and adding the law E-INPUT means moving from late
to early. E-INPUT is:

 Assume C => ai=bj, i in I and j in J, and x notin n(C), and 
 C |> SUMi t.Pi = SUMj t.Qj. Then C |> SUMi ai(x).Pi = SUMj bj(x).Qj


2. The systems originally presented for the pi-calculus by Milner,
Parrow, Walker and later developed by eg Parrow and Sangiorgi, where
judgements are of the kind

 P = Q

with the standard interpretation.  In the following I shall use the
proof system in my "An introduction to the pi-calculus", and refer to
it laconically as "my system" although it is a mere variant of the
system developed with Davide Sangiorgi. A statement like "P=Q" (with
no preceding "C |>") is taken to mean derivability in my system.  I
shall refer to the proof rules by the names in my "introduction."

My system has been shown complete for strong late and early
congruence, where moving from late to early is accomplished by adding
either one of the laws EARLY or EARLY2.  EARLY is

 a(x).P + a(x).Q = a(x).P + a(x).Q + a(x)(if x=y then P else Q)

and the law EARLY2 is inspired by E-INPUT, but simpler:

 If  SUMi t.Pi = SUMj t.Qj  then  SUMi a(x).Pi = SUMj a(x).Qj

However, the weak congruences have not yet been treated in detail in
my system. The claim in my "introduction" is that adding the the
tau-laws gives a complete axiomatisation of the weak congruences.

Summary
-------

The main result in this note is that for any proof in Lin's system of

 C |> P = Q

there is an isomorphic proof in my system of

 if C then P  =  if C then Q 

Here, with "isomorphic proof" I mean that each step in the proof in
Lin's system can be mapped to a small sequence of steps of a proof in
my system.  The demonstration of this main result is by induction on
the length of the proof in Lin's system, with one inductive step for
each of the proof rules (there are 13 in all).

This has some nice consequences. Completeness of my system follows
immediately by the completeness of Lin's system, taking C to be
true. Moreover Lin's system is parametrised on a set of axioms, and
the "isomorphism" is of course preserved by adding the same axioms
to my system. In particular if the tau-laws are added, my system then
becomes complete for weak congruence. But the technique is quite general
and could have wider applications.

The same result applies for early congruence if EARLY2 is adjoined to
my system. So in particular, with EARLY2 and the tau-laws we get
completeness for weak early congruence. It shold be noted that I have
failed to establish the same kind of isomorphy using EARLY rather than
EARLY2.  Although I do believe that adjoining EARLY also gives a
complete axiomatisation for weak early congruence, I currently see no
quick way to demonstrate this through a reduction to Lin's system.

Acknowledgements
----------------

Credit goes to Huimin Lin for suggesting this way to prove
completeness of my system.  I also thank Davide Sangiorgi whose polite
inquiry about where to find the proof of the claim in my
"introduction" prompted me to write this.

Details
-------

In the following I write [C]P for the generalised Match "if C then P"
where C is a conjunction of Matches and Mismatches.  We consider first
the system for late congruence. We shall demonstrate that for each
proof of C |> T = U in Lin's system there is a proof of [C]T = [C]U in
my system. The argument is by induction on the length of the inference
of C |> T = U. Consider the last step in the inference, there is one
case for each of the inference rules applied.

1. EQUIV. Follows from equational reasoning in my system and induction.

2. AXIOM. Follows from the fact that the axioms in Lin's system is a
subset of the axioms in my system (Lin's S1, S3, S4, R1 and R4 are part of
my structural congruence).

3. CHOICE. Assume C |> Pi = Qi for i=1,2 by shorter inferences.
By induction (1) [C]Pi = [C]Qi for i=1,2. 
We must prove [C](P1+P2) = [C](Q1+Q2).

[C](P1+P2) =
  by GM3
[C]P1 + [C]P2 =
  by (1)
[C]Q1 + [C]Q2 =
  by GM3
[C](Q1+Q2)

4. L-INPUT. Assume C |> P = Q by a shorter inference and that C => a=b and
x notin n(C). Then C <=> C & a=b. By induction (1) [C]P = [C]Q. We must prove
[C]a(x).P = [C]b(x).Q.

[C]a(x).P =
  by GM4 and x notin n(C)
[C]a(x).[C]P =
  by (1)
[C]a(x).[C]Q =
  by GM4
[C]a(x).Q =
  by  C <=> C & a=b and GM1
[C][a=b]a(x).Q =
  by GM5
[C][a=b]b(x).Q =
    by  C <=> C & a=b and GM1
[C]b(x).Q


5. OUTPUT. The reasoning is as in case 4 above.

6. TAU. Assume C |> P = Q by a shorter inference. By induction (1)
[C]P = [C]Q. We must prove [C]t.P = [C]t.Q.

[C]t.P =
  by GM4
[C]t.[C]P =
  by (1)
[C]t.[C]Q =
  by GM4
[C]t.Q

7. MATCH. Assume C & x=y |> P = Q and C & x#y |> Q = 0. Then by induction
(1) [C & x=y]P = [C & x=y]Q  and (2) [C & x#y]Q = [C & x#y]0. We must show
[C & x=y]P = [C]Q.

[C & x=y]P =
  by (1)
[C & x=y]Q =
  by structural congruence
[C & x=y]Q + 0 =
  by 0 = [M]0 for any M (derived law mentioned in my chapter)
[C & x=y]Q + [C & x#y]0 =
  by (2)
[C & x=y]Q + [C & x#y]Q =
  by GM3
[C]([x=y]Q + [x#y]Q) =
  by GM2
[C]Q

8. MISMATCH. The reasoning is as in case 7 above.

9. RES. Write "x fresh" for the conjunction of inequalities x#y for
all y free in P or in Q, except x itself, and assume x notin n(C).
Assume C & x fresh |> P = Q. Then by induction
(1) [C & x fresh]P = [C & x fresh]Q. We must show [C](nu x)P = [C](nu x)Q.

[C](nu x) P =
  by repeated application of GM6*
[C](nu x)[x fresh] P =
  by structural congruence since x notin n(C)
(nu x)[C & x fresh] P =
  by (1)
(nu x)[C & x fresh] Q =
  by structural congruence
[C](nu x)[x fresh] Q =
    by repeated application of GM6* in the other direction
[C](nu x) Q

10. PARTITION. Assume C & x=y |> P = Q and C & x#y |> P = Q. Then by
induction (1) [C & x=y]P = [C & x=y]Q and (2) [C & x#y]P = [C & x#y]Q.
We must show [C]P = [C]Q.

[C]P =
  by GM2
[C]([x=y]P + [x#y]P) =
  by GM3
[C & x=y]P + [C & x#y]P =
  by (1) and (2)
[C & x=y]Q + [C & x#y]Q =
   by GM3
[C]([x=y]Q + [x#y]Q) =
  by GM2
[C]Q

11. CONSEQ. Assume C' => C and C |> P = Q, then by induction (1) [C]P = [C]Q.
We must prove [C']P = [C']Q.

[C']P =
  by C' => C we get C' <=> C' & C, and thus by GM1
[C' & C]P =
[C'][C]P =
  by (1)
[C'][C]Q =
[C' & C]Q =
  as in the first step
[C']Q =

12. ABSURD. [x#x]P = [x#x]Q follows immediately from MM1.

13. ALPHA. Follows from structural congruence.

QED


Now consider the corresponding system for early congruence. There is
one additional case:

14. E-INPUT. Assume C => ai=bj, i in I and j in J, and x notin n(C), and 
C |> SUMi t.Pi = SUMj t.Qj. Then by induction (1) [C]SUMi t.Pi = [C]SUMj t.Qj.
We must prove [C]SUMi ai(x).Pi = [C]SUMj bj(x).Qj. We may safely
assume that neither I nor J is empty (in the case that both are empty
the conclusion boils down to 0 = 0, which follows anyway from
equational reasoning, and the case that only one is empty is
impossible since the precondition of E-INPUT would then be false, for
any of the congruences considered).

We first prove that  (2) SUMi t.[C]Pi = SUMj t.[C]Qj.

SUMi t.[C]Pi =
 by GM2 repeatedly, letting -C stand for the complement of C
[C]SUMi t.[C]Pi + [-C]SUMi t.[C]Pi =
 by GM4, GM3
[C]SUMi t.Pi + [-C]SUMi t.[C]Pi =
 by GM4, GM3
[C]SUMi t.Pi + SUMi [-C]t.[-C][C]Pi =
 by GM1, MM1
[C]SUMi t.Pi + SUMi [-C]t.0 =
 by I nonempty and the law S
[C]SUMi t.Pi + [-C]t.0 =
 by (1)
[C]SUMj t.Qj + [-C]t.0 =
 by J nonempty and S
[C]SUMi t.Qi + [-C]SUMj t.0 =
 by GM4, GM3, GM1, MM1
[C]SUMi t.Qi + [-C]SUMj t.[C]Qj =
 by GM4, GM3
[C]SUMi t.[C]Qi + [-C]SUMj t.[C]Qj =
 by GM2 repeatedly
SUMi t.[C]Qi

By (2) and EARLY2 we get (3) SUMi a(x).[C]Pi = SUMj a(x).[C]Qj. Finally,
choosing a to be a1, 

[C]SUMi ai(x).Pi =
 by GM3
SUMi [C]ai(x).Pi =
 by GM1 and C => a=ai, which means C <=> C & a=ai
SUMi [C][a=ai]ai(x).Pi =
 by GM5
SUMi [C][a=ai]a(x).Pi =
 by GM1
SUMi [C]a(x).Pi =
 by GM4 and x notin n(C)
SUMi [C]a(x).[C]Pi =
 by GM3
[C]SUMi a(x).[C]Pi =
 by (3)
[C]SUMj a(x).[C]Qj =
 by GM3
SUMj [C]a(x).[C]Qj =
 by GM4 and x notin n(C)
SUMj [C]a(x).Qj =
 by C=>a=bj, GM1 and GM5
SUMj [C]bj(x).Qj =
 by GM3
[C]SUMj bj(x).Qj.

QED

There appears no straightforward way to emulate EARLY2 using EARLY.
The converse is however easy as EARLY follows from EARLY2 and

t.P + t.Q = t.P + t.Q + t.([x=y]P + [x#y]Q)

which in turn follows by

t.P + t.Q + t.([x=y]P + [x#y]Q) =
 by GM2
[x=y](t.P + t.Q + t.([x=y]P + [x#y]Q) + [x#y](t.P + t.Q + t.([x=y]P + [x#y]Q) =
 by GM3, GM4, GM1 and MM1
[x=y](t.P + t.Q + t.(     P + 0)      + [x#y](t.P + t.Q + t.(0      + Q) =
 by structural congruence and S
[x=y](t.P + t.Q)                      + [x#y](t.P + t.Q) =
 by GM2
t.P + t.Q