Re-worked CCS with alpha-conversion over recursion operator

[binghe]

Hi,

This huge PR modifies the existing CCS example with alpha-conversion over recursion operator, using the nominal generic terms from the examples/lambda/basics.

Recall in Milner's Calculus of Communicating Systems (CCS) [1], there are totally 8 operators (nil, var, prefix, sum, par, restr, relab and rec), which is usually defined by the following Datatype:

Datatype: CCS = nil
              | var string
              | prefix ('a Action) CCS
              | sum CCS CCS
              | par CCS CCS
              | restr ('a Label set) CCS
              | relab CCS ('a Relabeling)
              | rec string CCS
End

The structural operational semantics (SOS) of CCS defines how a CCS process transits to another one under certain action. For example, the term prefix u E can transit to E under action u, denoted by |- TRANS (prefix u E) u E.

One may think that any process represented by finite term can only make finite number of transitions as the term size reduces. But this is not true: the recursion operator rec, together with var, can be used to define CCS processes with infinite transition. For example, the CCS process given by rec X (prefix u (var X)) have infinite transition under the actionu. In the previous CCS term, the leading rec X ... can be consider as a "constant" definition: X := prefix u (var X), and once the SOS reaches var X, it will replace var X by the body of rec X ..., thus become another prefix u (var X) and so on. Clearly, substituting the name "X" to any other name, does not change the transition behavior at all.

By using the nomsetTheory and generic_termsTheory from the λ-calculus example, now I've successfully redefined CCS terms with alpha-conversion built into the recursion operator, thus now we have rec X (var X) = rec Y (var Y) holds literally.

Previously the type CCS has two arguments: :(α, β) CCS, where α is the type of recursion variable names, while β is the type of actions. Now the first type argument becomes just :string, and thus it remains :α CCS where 'α᾽ is the previous type argument β (of actions).

The first big benefit (of α-conversion) is the avoiding of discussions on bound variables of CCS terms, previously defined by BV and is needed in the proofs of some advanced theorems. This reduced the overall proof size. The new CCS induction theorem, with the ability to exclude a set of names, which I still call it "nc_INDUCTION2", is the following:

nc_INDUCTION2
⊢ ∀P X.
    (∀s. P (var s)) ∧ P nil ∧ (∀u E. P E ⇒ P (u..E)) ∧
    (∀E1 E2. P E1 ∧ P E2 ⇒ P (E1 + E2)) ∧
    (∀E1 E2. P E1 ∧ P E2 ⇒ P (E1 || E2)) ∧ (∀L E. P E ⇒ P (restr L E)) ∧
    (∀E rf. P E ⇒ P (relab E rf)) ∧ (∀y E. P E ∧ y ∉ X ⇒ P (rec y E)) ∧
    FINITE X ⇒
    ∀t. P t

Term substitutions and simultaneous substitutions are also defined like the way of λ-calculus but look more tedious due to more operators of CCS:

[SUB_THM]
⊢ ([N/x] (var x) = N ∧ (x ≠ y ⇒ [N/y] (var x) = var x) ∧
   (∀u E. [E/u] nil = nil) ∧ (∀x u E t. [E/u] (x..t) = x..[E/u] t) ∧
   (∀u E t t'. [E/u] (t' + t) = [E/u] t' + [E/u] t) ∧
   (∀u E t t'. [E/u] (t' || t) = [E/u] t' || [E/u] t) ∧
   (∀x u E t. [E/u] (restr x t) = restr x ([E/u] t)) ∧
   (∀x u E t. [E/u] (relab t x) = relab ([E/u] t) x) ∧
   ∀v u E t. v ≠ u ∧ v # E ⇒ [E/u] (rec v t) = rec v ([E/u] t)) ∧
  ∀N x x' y t.
    x' ≠ x ∧ x' # N ∧ y ≠ x ∧ y # N ⇒
    tpm [(x',y)] ([N/x] t) = [N/x] (tpm [(x',y)] t)

[ssub_thm]
⊢ (∀s fm. fm ' (var s) = if s ∈ FDOM fm then fm ' s else var s) ∧
  (∀fm. fm ' nil = nil) ∧ (∀x fm t. fm ' (x..t) = x..fm ' t) ∧
  (∀fm t t'. fm ' (t' + t) = fm ' t' + fm ' t) ∧
  (∀fm t t'. fm ' (t' || t) = fm ' t' || fm ' t) ∧
  (∀x fm t. fm ' (restr x t) = restr x (fm ' t)) ∧
  (∀x fm t. fm ' (relab t x) = relab (fm ' t) x) ∧
  ∀v fm t.
    v ∉ FDOM fm ∧ (∀y. y ∈ FDOM fm ⇒ v # fm ' y) ⇒
    fm ' (rec v t) = rec v (fm ' t)

But more substitution theorems have both the same name and same statements as in λ-calculus, e.g.

[lemma14b]
⊢ ∀M. v # M ⇒ [N/v] M = M
[lemma14b_ext1]
⊢ ∀v M. v # M ⇔ ∀N. [N/v] M = M
[lemma14b_ext2]
⊢ ∀v M. v # M ⇔ ∀N1 N2. [N1/v] M = [N2/v] M

On the other hand, some new theorems about substitutions, like the above [lemma14b_ext1], is also added back to the λ-calculus example (in termTheory) for potential future uses.

All existing (major) CCS theorems (except for those small utilities) still hold with minor fix-ups. I think the present work has opened new opportunities for further developments of the theory of CCS, and one such work from me is still in process.

--Chun

[1] Milner, Robin. Communication and concurrency. Prentice hall, 1989.

[binghe]

Previous, to define new terms from generic_termsTheory, the following helper theorems were repeatedly defined:

val LENGTH_NIL' =
    CONV_RULE (BINDER_CONV (LAND_CONV (REWR_CONV EQ_SYM_EQ)))
              listTheory.LENGTH_NIL
val LENGTH1 = prove(
  ``(1 = LENGTH l) ⇔ ∃e. l = [e]``,
  Cases_on `l` >> srw_tac [][listTheory.LENGTH_NIL]);
val LENGTH2 = prove(
  ``(2 = LENGTH l) ⇔ ∃a b. l = [a;b]``,
  Cases_on `l` >> srw_tac [][LENGTH1]);
val FORALL_ONE = prove(
  ``(!u:one. P u) = P ()``,
  SRW_TAC [][EQ_IMP_THM, oneTheory.one_induction]);
val FORALL_ONE_FN = prove(
  ``(!uf : one -> 'a. P uf) = !a. P (\u. a)``,
  SRW_TAC [][EQ_IMP_THM] THEN
  POP_ASSUM (Q.SPEC_THEN `uf ()` MP_TAC) THEN
  Q_TAC SUFF_TAC `(\y. uf()) = uf` THEN1 SRW_TAC [][] THEN
  SRW_TAC [][FUN_EQ_THM, oneTheory.one]);

val EXISTS_ONE_FN = prove(
  ``(?f : 'a -> one -> 'b. P f) = (?f : 'a -> 'b. P (\x u. f x))``,
  SRW_TAC [][EQ_IMP_THM] THENL [
    Q.EXISTS_TAC `\a. f a ()` THEN SRW_TAC [][] THEN
    Q_TAC SUFF_TAC `(\x u. f x ()) = f` THEN1 SRW_TAC [][] THEN
    SRW_TAC [][FUN_EQ_THM, oneTheory.one],
    Q.EXISTS_TAC `\a u. f a` THEN SRW_TAC [][]
  ]);

The theorem LENGTH_NIL' is already in listTheory as LENGTH_NIL_SYM. The theorem FORALL_ONE is already in oneTheory. I think the rest of them are general enough to be added into listTheory and oneTheory so that the duplicated proofs can now be all removed (in termTheory, ctermTheory and labelled_termTheory).

[binghe]

Once CCS got alpha-conversion, it's possible to define the I combinator and prove their alpha-equivalence:

[I_def]
⊢ I = rec "x" (var "x")
[I_cases]
⊢ I = rec Y P ⇒ P = var Y
[I_thm]
⊢ ∀X. I = rec X (var X)

It's interesting that the existing SOS rules for TRANS cannot prove that I has or has not transitions. To fix this issue, I have to modify the SOS rule [REC] from:

[REC] (old)
⊢ ∀E u X E1. CCS_Subst E (rec X E) X --u-> E1 ⇒ rec X E --u-> E1

to (adding E ≠ var X):

[REC] (new)
⊢ ∀E u X E1. CCS_Subst E (rec X E) X --u-> E1 ∧ E ≠ var X ⇒ rec X E --u-> E1

This should be considered as a small bug in the textbook definition of SOS rules for CCS. With this change, all existing theorems can still be proved, but then I'm able to prove that I has no transitions:

[I_NO_TRANS]
⊢ ∀u E. ¬(I --u-> E)
[REC_VAR_NO_TRANS]
⊢ ∀X u E. ¬(rec X (var X) --u-> E)

When doing induction on E of STRONG_EQUIV (rec X E) ..., the case for E = var X previously cannot be proved, now the proof can continue.

[binghe]

Today Ian Shillito provided me a method to solve the proof difficulty in "I_NO_TRANS" (|- ∀u E. ¬(I --u-> E)). His idea is to first define labelled transition with an extra number as the "proof depth", and then the SOS rule [RECn] is

[RECn]
⊢ ∀n E u X E1.
    TRANSn n (CCS_Subst E (rec X E) X) u E1 ⇒ TRANSn (SUC n) (rec X E) u E1

By induction it's simple to prove that TRANS and TRANSn are exchangeable:

[TRANS_iff_TRANSn]
⊢ ∀E u E'. E --u-> E' ⇔ ∃n. TRANSn n E u E'

Meanwhile by induction on the "proof depth" I can prove that "I" combinator has no labelled transitions: (because there's no infinite descending proofs of rec X (var X) with all positive "proof depth")

[I_NO_TRANSn]
⊢ ∀u E n. ¬TRANSn n I u E

Combining the above two theorems we get I_NO_TRANS without modifying SOS rules at all. That's amazing...

[mn200]

Awesome!