5.3. Reduction and reaction🔗

Theorem5.3.1

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 5.3.2

Loading preview

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

✓L∃∀N

Every reduction is a reaction of the encodings: for every X and \rho with \mathrm{fn}_\rho(P) \subseteq X,

P \to Q \;\Longrightarrow\; \llbracket P \rrbracket_{X,\rho} \longrightarrow_{\mathcal{R}_\pi} \llbracket Q \rrbracket_{X,\rho} .

Lean code for Theorem5.3.1●1 theorem

theoremdefined in Pi/Sound.lean

complete

theorem red_soundπ {p q : Proc} (h : p ⟶ q) (X : NameSet Nat) (ρ : Nat → Nat)
  (hp : NamesIn X.names ρ p) : ⟦p⟧ ⟶[piRules] ⟦q⟧

theorem red_soundπ {p q : Proc} (h : p ⟶ q)
  (X : NameSet Nat) (ρ : Nat → Nat)
  (hp : NamesIn X.names ρ p) :
  ⟦p⟧ ⟶[piRules] ⟦q⟧

**Soundness of the π encoding: every reduction of every process is a
reaction of the encodings** under the two name-passing rules, for every
name set and environment.

Theorem5.3.2

uses 1used by 0✓L∃∀N

For closed processes, reaction of the encoding is exactly reduction: for P closed, \mathrm{fn}_\rho(P) \subseteq X, and every abstract bigraph b,

\llbracket P \rrbracket_{X,\rho} \longrightarrow_{\mathcal{R}_\pi} b \;\iff\; \exists Q.\; P \to Q \;\wedge\; b = \llbracket Q \rrbracket_{X,\rho} .

For open processes the direction from left to right is OPEN.

Rests on NEW: Closed.

Lean code for Theorem5.3.2●1 theorem

theoremdefined in Pi/Iff.lean

complete

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

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

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

Theorem5.3.3

uses 1used by 0✓L∃∀N

Mobility: a private name is sent, then used. In the calculus the two steps below are reductions, and with X = \{x, y\} and \rho constant their encodings react:

\llbracket \nu z\,(\bar{x}z.\bar{z}y.0) \mid x(u).u(v).0 \rrbracket_{X,\rho} \;\longrightarrow_{\mathcal{R}_\pi}\; \llbracket \nu z\,(\bar{z}y.0 \mid z(v).0) \rrbracket_{X,\rho} \;\longrightarrow_{\mathcal{R}_\pi}\; \llbracket \nu z\,(0 \mid 0) \rrbracket_{X,\rho} .

Rests on NEW: X01, pMob, qMob, rMob; not audited: ρ01.

Lean code for Theorem5.3.3●3 theorems

theoremdefined in Pi/Examples.lean

complete

theorem mob_react : ⟦pMob⟧ ⟶[piRules] ⟦qMob⟧ ∧ ⟦qMob⟧ ⟶[piRules] ⟦rMob⟧

theorem mob_react :
  ⟦pMob⟧ ⟶[piRules] ⟦qMob⟧ ∧
    ⟦qMob⟧ ⟶[piRules] ⟦rMob⟧

**Mobility in the agents**: the first reaction links the receiver to the
private edge, and the second reacts on it.

theoremdefined in Pi/Examples.lean

complete

theorem red_mob₁ : pMob ⟶ qMob

theorem red_mob₁ : pMob ⟶ qMob

**Scope extrusion by name passing**: `z` is sent along `x`, and its
scope grows to hold the receiver.

theoremdefined in Pi/Examples.lean

complete

theorem red_mob₂ : qMob ⟶ rMob

theorem red_mob₂ : qMob ⟶ rMob

**…and the received name is used**: the two ends now meet on `z`.