Calculus of Communicating Systems (CCS)

CCS [Mil80], as presented in [San]. In the semantics (see CCS.lts), we adopt the option of constant definitions (K = P).

Main definitions

• CCS.Process: processes.
• CCS.Context: contexts.

Main results

• CCS.Context.complete: any process is equal to some context filled an atomic process (nil or a constant).

References

• [R. Milner, A Calculus of Communicating Systems] [Mil80]
• [D. Sangiorgi, Introduction to Bisimulation and Coinduction] [San]

inductive CCS.Act (Name : Type u) : Type u

Actions.

• name {Name : Type u} (a : Name) : Act Name
• coname {Name : Type u} (a : Name) : Act Name
• τ {Name : Type u} : Act Name

instance CCS.instDecidableEqAct {Name✝ : Type u_1} [DecidableEq Name✝] : DecidableEq (Act Name✝)

Equations

• CCS.instDecidableEqAct = CCS.decEqAct✝

inductive CCS.Process (Name : Type u) (Constant : Type v) : Type (max u v)

Processes.

• nil {Name : Type u} {Constant : Type v} : Process Name Constant
• pre {Name : Type u} {Constant : Type v} (μ : Act Name) (p : Process Name Constant) : Process Name Constant
• par {Name : Type u} {Constant : Type v} (p q : Process Name Constant) : Process Name Constant
• choice {Name : Type u} {Constant : Type v} (p q : Process Name Constant) : Process Name Constant
• res {Name : Type u} {Constant : Type v} (a : Name) (p : Process Name Constant) : Process Name Constant
• const {Name : Type u} {Constant : Type v} (c : Constant) : Process Name Constant

instance CCS.instDecidableEqProcess {Name✝ : Type u_1} {Constant✝ : Type u_2} [DecidableEq Name✝] [DecidableEq Constant✝] : DecidableEq (Process Name✝ Constant✝)

Equations

• CCS.instDecidableEqProcess = CCS.decEqProcess✝

def CCS.Act.co (Name : Type u) (μ : Act Name) : Act Name

Co action.

Equations

• CCS.Act.co Name (CCS.Act.name a) = CCS.Act.coname a
• CCS.Act.co Name (CCS.Act.coname a) = CCS.Act.name a
• CCS.Act.co Name CCS.Act.τ = CCS.Act.τ

theorem CCS.Act.co.involution (Name : Type u) (μ : Act Name) : co Name (co Name μ) = μ

Act.co is an involution.

inductive CCS.Context (Name : Type u) (Constant : Type v) : Type (max u v)

Contexts.

• hole {Name : Type u} {Constant : Type v} : Context Name Constant
• pre {Name : Type u} {Constant : Type v} (μ : Act Name) (c : Context Name Constant) : Context Name Constant
• parL {Name : Type u} {Constant : Type v} (c : Context Name Constant) (q : Process Name Constant) : Context Name Constant
• parR {Name : Type u} {Constant : Type v} (p : Process Name Constant) (c : Context Name Constant) : Context Name Constant
• choiceL {Name : Type u} {Constant : Type v} (c : Context Name Constant) (q : Process Name Constant) : Context Name Constant
• choiceR {Name : Type u} {Constant : Type v} (p : Process Name Constant) (c : Context Name Constant) : Context Name Constant
• res {Name : Type u} {Constant : Type v} (a : Name) (c : Context Name Constant) : Context Name Constant

instance CCS.instDecidableEqContext {Name✝ : Type u_1} {Constant✝ : Type u_2} [DecidableEq Name✝] [DecidableEq Constant✝] : DecidableEq (Context Name✝ Constant✝)

Equations

• CCS.instDecidableEqContext = CCS.decEqContext✝

def CCS.Context.fill {Name : Type u} {Constant : Type v} (c : Context Name Constant) (p : Process Name Constant) : Process Name Constant

Replaces the hole in a Context with a Process.

Equations

• CCS.Context.hole.fill p = p
• (CCS.Context.pre μ c_2).fill p = CCS.Process.pre μ (c_2.fill p)
• (c_2.parL r).fill p = (c_2.fill p).par r
• (CCS.Context.parR r c_2).fill p = r.par (c_2.fill p)
• (c_2.choiceL r).fill p = (c_2.fill p).choice r
• (CCS.Context.choiceR r c_2).fill p = r.choice (c_2.fill p)
• (CCS.Context.res a c_2).fill p = CCS.Process.res a (c_2.fill p)

theorem CCS.Context.complete (Name : Type u) (Constant : Type v) (p : Process Name Constant) : ∃ (c : Context Name Constant), p = c.fill Process.nil ∨ ∃ (k : Constant), p = c.fill (Process.const k)

Any Process can be obtained by filling a Context with an atom. This proves that Context is a complete formalisation of syntactic contexts for CCS.