Parallel composition of population protocols (CRN-3)

The protocol of the proof of [AADFP06, Lemma 3]: states Q₁ × Q₂, input s ↦ (I₁ s, I₂ s), both components make their own transition in every encounter, and the output of (p₁, p₂) is ξ(O₁ p₁, O₂ p₂). Every path of the composition projects to paths of both components (reaches_fst, reaches_snd), and a path of one component lifts to a path of the composition, along which the other component follows a path of its own (lift_fst, lift_snd). Hence (prod_stablyComputes): run the first component to an output-stable configuration, then the second; the first stays output-stable.

def Crn.Protocol.prod {X : Type u_1} {Q₁ : Type u_2} {Q₂ : Type u_3} (P₁ : Protocol X Q₁) (P₂ : Protocol X Q₂) (ξ : Bool → Bool → Bool) : Protocol X (Q₁ × Q₂)

Parallel composition of two protocols with output ξ(O₁, O₂) [AADFP06, proof of Lemma 3].

Equations

• One or more equations did not get rendered due to their size.

theorem Crn.Protocol.prod_interact_fst {X : Type u_1} {Q₁ : Type u_2} {Q₂ : Type u_3} {n : ℕ} {P₁ : Protocol X Q₁} {P₂ : Protocol X Q₂} {ξ : Bool → Bool → Bool} (c : Fin n → Q₁ × Q₂) (e : AgentPair n) : (fun (w : Fin n) => ((P₁.prod P₂ ξ).interact c e w).1) = P₁.interact (fun (w : Fin n) => (c w).1) e

The first component of an encounter of the composition is an encounter of P₁.

theorem Crn.Protocol.prod_interact_snd {X : Type u_1} {Q₁ : Type u_2} {Q₂ : Type u_3} {n : ℕ} {P₁ : Protocol X Q₁} {P₂ : Protocol X Q₂} {ξ : Bool → Bool → Bool} (c : Fin n → Q₁ × Q₂) (e : AgentPair n) : (fun (w : Fin n) => ((P₁.prod P₂ ξ).interact c e w).2) = P₂.interact (fun (w : Fin n) => (c w).2) e

The second component of an encounter of the composition is an encounter of P₂.

theorem Crn.Protocol.reaches_fst {X : Type u_1} {Q₁ : Type u_2} {Q₂ : Type u_3} {n : ℕ} {P₁ : Protocol X Q₁} {P₂ : Protocol X Q₂} {ξ : Bool → Bool → Bool} {c d : Fin n → Q₁ × Q₂} (h : (P₁.prod P₂ ξ).Reaches c d) : P₁.Reaches (fun (w : Fin n) => (c w).1) fun (w : Fin n) => (d w).1

Paths of the composition project to paths of the first component.

theorem Crn.Protocol.reaches_snd {X : Type u_1} {Q₁ : Type u_2} {Q₂ : Type u_3} {n : ℕ} {P₁ : Protocol X Q₁} {P₂ : Protocol X Q₂} {ξ : Bool → Bool → Bool} {c d : Fin n → Q₁ × Q₂} (h : (P₁.prod P₂ ξ).Reaches c d) : P₂.Reaches (fun (w : Fin n) => (c w).2) fun (w : Fin n) => (d w).2

Paths of the composition project to paths of the second component.

theorem Crn.Protocol.lift_fst {X : Type u_1} {Q₁ : Type u_2} {Q₂ : Type u_3} {n : ℕ} {P₁ : Protocol X Q₁} {P₂ : Protocol X Q₂} {ξ : Bool → Bool → Bool} {c₁ d₁ : Fin n → Q₁} (h : P₁.Reaches c₁ d₁) (c : Fin n → Q₁ × Q₂) (hc : (fun (w : Fin n) => (c w).1) = c₁) : ∃ (d : Fin n → Q₁ × Q₂), (P₁.prod P₂ ξ).Reaches c d ∧ (fun (w : Fin n) => (d w).1) = d₁ ∧ P₂.Reaches (fun (w : Fin n) => (c w).2) fun (w : Fin n) => (d w).2

A path of the first component lifts to the composition (same encounters); the second component follows a path of P₂.

theorem Crn.Protocol.lift_snd {X : Type u_1} {Q₁ : Type u_2} {Q₂ : Type u_3} {n : ℕ} {P₁ : Protocol X Q₁} {P₂ : Protocol X Q₂} {ξ : Bool → Bool → Bool} {c₂ d₂ : Fin n → Q₂} (h : P₂.Reaches c₂ d₂) (c : Fin n → Q₁ × Q₂) (hc : (fun (w : Fin n) => (c w).2) = c₂) : ∃ (d : Fin n → Q₁ × Q₂), (P₁.prod P₂ ξ).Reaches c d ∧ (fun (w : Fin n) => (d w).2) = d₂ ∧ P₁.Reaches (fun (w : Fin n) => (c w).1) fun (w : Fin n) => (d w).1

A path of the second component lifts to the composition (same encounters); the first component follows a path of P₁.

theorem Crn.Protocol.prod_stablyComputes {X : Type u_1} {Q₁ : Type u_2} {Q₂ : Type u_3} {P₁ : Protocol X Q₁} {P₂ : Protocol X Q₂} {ξ : Bool → Bool → Bool} [Fintype X] [DecidableEq X] {φ ψ : (X → ℕ) → Bool} (h₁ : P₁.StablyComputes φ) (h₂ : P₂.StablyComputes ψ) : (P₁.prod P₂ ξ).StablyComputes fun (x : X → ℕ) => ξ (φ x) (ψ x)

[AADFP06, Lemma 3] The parallel composition of protocols stably computing φ and ψ stably computes ξ(φ, ψ).