3.3. CCS in bigraphs🔗

Theorem3.3.1

uses 1used by 1✓L∃∀N

The encoding \llbracket - \rrbracket of finite CCS respects structural congruence, and the converse is REFUTED:

P \equiv Q \;\Longrightarrow\; \llbracket P \rrbracket = \llbracket Q \rrbracket, \qquad \llbracket \bar a.(0 \mid 0) \rrbracket = \llbracket \bar a.0 \rrbracket \;\text{ but }\; \bar a.(0 \mid 0) \not\equiv \bar a.0 .

Rests on UNBRIDGED: Locus.CCS.SC; not audited: CCS.X0, CCS.names, Locus.CCS.Name.

Lean code for Theorem3.3.1●2 theorems

theoremdefined in Bigraph/CCS.lean

complete

theorem sc_sound {X : NameSet Nat} {p q : Locus.CCS.Proc} (h : Locus.CCS.SC p q)
  (hp : CCS.NamesIn X p) (hq : CCS.NamesIn X q) : ⟦p⟧ = ⟦q⟧

theorem sc_sound {X : NameSet Nat}
  {p q : Locus.CCS.Proc}
  (h : Locus.CCS.SC p q)
  (hp : CCS.NamesIn X p)
  (hq : CCS.NamesIn X q) : ⟦p⟧ = ⟦q⟧

**Structural congruence is sound for the encoding**: structurally
congruent processes are the same abstract agent.

theoremdefined in Bigraph/CCS.lean

complete

theorem sc_not_complete :
  ⟦Locus.CCS.Proc.pre (Locus.CCS.Act.snd 0)
          (Locus.CCS.Proc.nil.par Locus.CCS.Proc.nil)⟧ =
      ⟦Locus.CCS.Proc.pre (Locus.CCS.Act.snd 0) Locus.CCS.Proc.nil⟧ ∧
    ¬Locus.CCS.SC
        (Locus.CCS.Proc.pre (Locus.CCS.Act.snd 0)
          (Locus.CCS.Proc.nil.par Locus.CCS.Proc.nil))
        (Locus.CCS.Proc.pre (Locus.CCS.Act.snd 0) Locus.CCS.Proc.nil)

theorem sc_not_complete :
  ⟦Locus.CCS.Proc.pre
          (Locus.CCS.Act.snd 0)
          (Locus.CCS.Proc.nil.par
            Locus.CCS.Proc.nil)⟧ =
      ⟦Locus.CCS.Proc.pre
          (Locus.CCS.Act.snd 0)
          Locus.CCS.Proc.nil⟧ ∧
    ¬Locus.CCS.SC
        (Locus.CCS.Proc.pre
          (Locus.CCS.Act.snd 0)
          (Locus.CCS.Proc.nil.par
            Locus.CCS.Proc.nil))
        (Locus.CCS.Proc.pre
          (Locus.CCS.Act.snd 0)
          Locus.CCS.Proc.nil)

**REFUTED: equal agents need not be structurally congruent.**

Theorem3.3.2

Statement uses 2

Statement dependency previews

Preview

Definition 3.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Reaction of the encoding is exactly reduction of finite CCS:

\llbracket P \rrbracket \longrightarrow b \;\iff\; \exists Q.\; P \to Q \;\wedge\; b = \llbracket Q \rrbracket .

Lean code for Theorem3.3.2●1 theorem

theoremdefined in Bigraph/CCSComplete.lean

complete

theorem react_iff {X : NameSet Nat} {p : Locus.CCS.Proc} (hp : CCS.NamesIn X p)
  (b : Bg.Abstract CCS.sig Nat) :
  ⟦p⟧ ⟶[CCS.ccsRules] b ↔ ∃ q hq, Locus.CCS.Red p q ∧ b = ⟦q⟧

theorem react_iff {X : NameSet Nat}
  {p : Locus.CCS.Proc}
  (hp : CCS.NamesIn X p)
  (b : Bg.Abstract CCS.sig Nat) :
  ⟦p⟧ ⟶[CCS.ccsRules] b ↔
    ∃ q hq, Locus.CCS.Red p q ∧ b = ⟦q⟧

**The encoding agrees with CCS**: an encoded process reacts exactly as
it reduces, up to structural congruence of the result.

Theorem3.3.3

uses 1used by 0✓L∃∀N

The same correspondence holds for closed CCS processes with restriction and replication, in two encodings. With restriction as a closed edge it needs the fragment in which no restriction lies inside a replicated body (CCSFull.react_iff); with restriction as a binder node, a pure bigraph under Jensen's scope rule, it holds for every closed process (CCSFull.react_iffB). For open processes it is OPEN.

Rests on NEW: CCSFull.Closed, CCSFull.Ctl, CCSFull.agentB, CCSFull.ccsRules, CCSFull.ccsRulesB, CCSFull.sig, Locus.CCSFull.NamesIn, Locus.CCSFull.Proc and 2 more.

Lean code for Theorem3.3.3●2 theorems

theoremdefined in Bigraph/CCSFullIff.lean

complete

theorem react_iff (X : NameSet Nat) (ρ : Nat → Nat) {p : Locus.CCSFull.Proc}
  (hwf : p.WF) (hcl : CCSFull.Closed p)
  (hp : Locus.CCSFull.NamesIn X.names ρ p)
  (b : Bg.Abstract CCSFull.sig Nat) :
  ⟦p⟧ ⟶[CCSFull.ccsRules] b ↔ ∃ q hr, b = ⟦q⟧

theorem react_iff (X : NameSet Nat)
  (ρ : Nat → Nat) {p : Locus.CCSFull.Proc}
  (hwf : p.WF) (hcl : CCSFull.Closed p)
  (hp : Locus.CCSFull.NamesIn X.names ρ p)
  (b : Bg.Abstract CCSFull.sig Nat) :
  ⟦p⟧ ⟶[CCSFull.ccsRules] b ↔
    ∃ q hr, b = ⟦q⟧

**The encoding agrees with CCS**: on a closed process of the fragment,
the reactions of its agent are exactly the agents of its reducts.

theoremdefined in Bigraph/CCSBindIff.lean

complete

theorem react_iffB (X : NameSet Nat) (ρ : Nat → Nat) {p : Locus.CCSFull.Proc}
  (hcl : CCSFull.Closed p) (hp : Locus.CCSFull.NamesIn X.names ρ p)
  (b : Bg.Abstract CCSFull.sig Nat) :
  CCSFull.agentB X ρ p hp ⟶[CCSFull.ccsRulesB] b ↔
    ∃ q hr, b = CCSFull.agentB X ρ q ⋯

theorem react_iffB (X : NameSet Nat)
  (ρ : Nat → Nat) {p : Locus.CCSFull.Proc}
  (hcl : CCSFull.Closed p)
  (hp : Locus.CCSFull.NamesIn X.names ρ p)
  (b : Bg.Abstract CCSFull.sig Nat) :
  CCSFull.agentB X ρ p
        hp ⟶[CCSFull.ccsRulesB]
      b ↔
    ∃ q hr, b = CCSFull.agentB X ρ q ⋯

**The second encoding agrees with CCS**: on every closed process, the
reactions of its agent are exactly the agents of its reducts.