5.2. Structural congruence🔗

Theorem5.2.1

uses 1used by 1✓L∃∀N

The encoding respects structural congruence: for every X and \rho with \mathrm{fn}_\rho(P) \subseteq X,

P \equiv Q \;\Longrightarrow\; \llbracket P \rrbracket_{X,\rho} = \llbracket Q \rrbracket_{X,\rho} .

Rests on UNBRIDGED: SC.

Lean code for Theorem5.2.1●1 theorem

theoremdefined in Pi/Enc.lean

complete

theorem sc_soundπ {X : NameSet Nat} {ρ : Nat → Nat} {p q : Proc} (h : p ≡ q)
  (hp : NamesIn X.names ρ p) : ⟦p⟧ = ⟦q⟧

theorem sc_soundπ {X : NameSet Nat}
  {ρ : Nat → Nat} {p q : Proc} (h : p ≡ q)
  (hp : NamesIn X.names ρ p) : ⟦p⟧ = ⟦q⟧

**Structural congruence is sound**: congruent processes are one agent.

Theorem5.2.2

uses 1used by 1✓L∃∀N

On closed processes the converse holds: for P, Q closed and every X, \rho with \mathrm{fn}_\rho(P) \subseteq X and \mathrm{fn}_\rho(Q) \subseteq X,

\llbracket P \rrbracket_{X,\rho} = \llbracket Q \rrbracket_{X,\rho} \;\iff\; P \equiv Q .

Rests on UNBRIDGED: SC; NEW: Closed.

Lean code for Theorem5.2.2●1 theorem

theoremdefined in Pi/Complete.lean

complete

theorem sc_iffπ {X : NameSet Nat} {ρ : Nat → Nat} {p q : Proc} (hp : Closed p)
  (hq : Closed q) (hpX : NamesIn X.names ρ p)
  (hqX : NamesIn X.names ρ q) : ⟦p⟧ = ⟦q⟧ ↔ p ≡ q

theorem sc_iffπ {X : NameSet Nat} {ρ : Nat → Nat}
  {p q : Proc} (hp : Closed p)
  (hq : Closed q)
  (hpX : NamesIn X.names ρ p)
  (hqX : NamesIn X.names ρ q) :
  ⟦p⟧ = ⟦q⟧ ↔ p ≡ q

**For closed processes, one agent iff congruent.**

Theorem5.2.3

uses 1used by 0✓L∃∀N

Structural congruence is exactly isomorphism of shapes, for open and closed processes alike: for all P, Q,

P \equiv Q \;\iff\; \mathrm{shape}(P) \cong \mathrm{shape}(Q) ,

an isomorphism being a pair of bijections, of nodes and of edges, that preserves controls and parents and links each port as before (free names and dangling indices kept).

Rests on UNBRIDGED: SC.

Lean code for Theorem5.2.3●1 theorem

theoremdefined in Pi/Complete.lean

complete

theorem sc_iff_isoπ {p q : Proc} :
  p ≡ q ↔ Nonempty (Shapes.Iso (shapeπ p) (shapeπ q))

theorem sc_iff_isoπ {p q : Proc} :
  p ≡ q ↔
    Nonempty
      (Shapes.Iso (shapeπ p) (shapeπ q))

**`SC` is shape isomorphism.**

Theorem5.2.4

uses 1used by 0✓L∃∀N

REFUTED without the exchange law. Let \equiv_0 be structural congruence without the exchange of restrictions. There are closed P, Q with

\bigl(\forall X\, \rho.\;\; \llbracket P \rrbracket_{X,\rho} = \llbracket Q \rrbracket_{X,\rho}\bigr) \;\wedge\; P \not\equiv_0 Q ,

namely P = \nu a\, \nu b\, \bar{b}a.0 and Q = \nu a\, \nu b\, \bar{a}b.0; for this pair P \equiv Q.

Rests on UNBRIDGED: SC; NEW: Closed, SC₀, Shapes.Chan; not audited: pExch, qExch.

Lean code for Theorem5.2.4●5 declarations

theoremdefined in Pi/Converse.lean

complete

theorem converse_refuted :
  ∃ p q,
    Closed p ∧
      Closed q ∧
        (∀ (X : NameSet Nat) (ρ : Nat → Nat) (hp : NamesIn X.names ρ p)
            (hq : NamesIn X.names ρ q), ⟦p⟧ = ⟦q⟧) ∧
          ¬SC₀ p q

theorem converse_refuted :
  ∃ p q,
    Closed p ∧
      Closed q ∧
        (∀ (X : NameSet Nat)
            (ρ : Nat → Nat)
            (hp : NamesIn X.names ρ p)
            (hq : NamesIn X.names ρ q),
            ⟦p⟧ = ⟦q⟧) ∧
          ¬SC₀ p q

**REFUTED: without the exchange law, equal agents need not be congruent
processes**, even closed ones.

inductive(11 constructors, Prop, 2 parameters)defined in Pi/Converse.lean

complete

inductive SC₀ : Proc → Proc → Prop

inductive SC₀ : Proc → Proc → Prop

**`SC` as it first stood**: every law but the exchange of two
restrictions.  Kept to state the refutation that motivated the law.

Constructors

refl (p : Proc) : SC₀ p p

symm {p q : Proc} : SC₀ p q → SC₀ q p

trans {p q r : Proc} : SC₀ p q → SC₀ q r → SC₀ p r

parNil (p : Proc) : SC₀ (p.par Proc.nil) p

parComm (p q : Proc) : SC₀ (p.par q) (q.par p)

parAssoc (p q r : Proc) :
  SC₀ ((p.par q).par r) (p.par (q.par r))

parCong {p p' q q' : Proc} :
  SC₀ p p' → SC₀ q q' → SC₀ (p.par q) (p'.par q')

resCong {p p' : Proc} : SC₀ p p' → SC₀ p.res p'.res

sumCong {m m' : Pi.Sum} :
  SCS₀ m m' → SC₀ (Proc.sum m) (Proc.sum m')

repCong (x : Shapes.Chan) {p p' : Proc} :
  SC₀ p p' → SC₀ (Proc.rep x p) (Proc.rep x p')

resPar (p q : Proc) {p' : Proc} (h : p' = Proc.shift 0 p) :
  SC₀ (p.par q.res) (p'.par q).res

theoremdefined in Pi/Converse.lean

complete

theorem sc_exch : pExch ≡ qExch

theorem sc_exch : pExch ≡ qExch

**With it, they are congruent.**

defdefined in Pi/Converse.lean

complete

def pExch : Proc

def pExch : Proc

`νx νy ȳx` (`νν 0̄1`): the channel is the inner binder, the datum the outer.

defdefined in Pi/Converse.lean

complete

def qExch : Proc

def qExch : Proc

`νx νy x̄y` (`νν 1̄0`): the channel is the outer binder, the datum the inner.