inductive CommunicationComplexity.Deterministic.FiniteMessage.Protocol (X : Type u_1) (Y : Type u_2) (α : Type u_3) : Type (max (max (max 1 u_1) u_2) u_3)

A generalized deterministic two-party communication protocol where at each step, a player sends an element of an arbitrary finite type β (rather than just a Bool). Equivalent to DetProtocol up to complexity (see toProtocol) where sending a β-valued message costs ⌈log₂ |β|⌉ bits.

• output {X : Type u_1} {Y : Type u_2} {α : Type u_3} (val : α) : Protocol X Y α
• alice {X : Type u_1} {Y : Type u_2} {α : Type u_3} {β : Type} [Fintype β] [Nonempty β] (f : X → β) (P : β → Protocol X Y α) : Protocol X Y α
• bob {X : Type u_1} {Y : Type u_2} {α : Type u_3} {β : Type} [Fintype β] [Nonempty β] (f : Y → β) (P : β → Protocol X Y α) : Protocol X Y α

def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.run {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (x : X) (y : Y) : α

Executes the generalized protocol on inputs x and y.

Equations

• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.output val).run x y = val
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.alice f P).run x y = (P (f x)).run x y
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bob f P).run x y = (P (f y)).run x y

def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.complexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} : Protocol X Y α → ℕ

The communication complexity of a generalized protocol. Sending a β-valued message costs ⌈log₂ |β|⌉ bits, reflecting the number of bits needed to encode an element of β.

Equations

• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.output val).complexity = 0
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.alice f P).complexity = Nat.clog 2 (Fintype.card β) + Finset.univ.sup fun (i : β) => (P i).complexity
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bob f P).complexity = Nat.clog 2 (Fintype.card β) + Finset.univ.sup fun (i : β) => (P i).complexity

noncomputable def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toProtocol {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : Deterministic.Protocol X Y α

Convert a finite-message protocol to a binary protocol with the same run behavior and complexity, encoding each β-valued message as ⌈log₂ |β|⌉ bits.

Equations

• p.toProtocol = ⋯.choose

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toProtocol_run {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : p.toProtocol.run = p.run

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toProtocol_complexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : p.toProtocol.complexity = p.complexity

def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.ofProtocol {X : Type u_1} {Y : Type u_2} {α : Type u_3} : Deterministic.Protocol X Y α → Protocol X Y α

Embed a binary protocol into a generalized protocol (with β = Bool at each step).

Equations

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

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.ofProtocol_run {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Deterministic.Protocol X Y α) (x : X) (y : Y) : (ofProtocol p).run x y = p.run x y

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.ofProtocol_complexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Deterministic.Protocol X Y α) : (ofProtocol p).complexity = p.complexity

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.ofProtocol_equiv {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Deterministic.Protocol X Y α) : ∃ (P : Protocol X Y α), P.run = p.run ∧ P.complexity = p.complexity

Every binary protocol can be viewed as a generalized protocol with the same run behavior and complexity (using β = Bool at each step).

def CommunicationComplexity.Deterministic.FiniteMessage.Protocol.comap {X : Type u_1} {Y : Type u_2} {α : Type u_3} {X' : Type u_4} {Y' : Type u_5} (p : Protocol X Y α) (fX : X' → X) (fY : Y' → Y) : Protocol X' Y' α

Pull back a finite-message protocol along functions fX : X' → X and fY : Y' → Y, composing each message function with the maps.

Equations

• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.output val).comap fX fY = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.output val
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.alice f P).comap fX fY = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.alice (f ∘ fX) fun (b : β) => (P b).comap fX fY
• (CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bob f P).comap fX fY = CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bob (f ∘ fY) fun (b : β) => (P b).comap fX fY

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.comap_run {X : Type u_1} {Y : Type u_2} {α : Type u_3} {X' : Type u_4} {Y' : Type u_5} (p : Protocol X Y α) (fX : X' → X) (fY : Y' → Y) (x' : X') (y' : Y') : (p.comap fX fY).run x' y' = p.run (fX x') (fY y')

@[simp]

theorem CommunicationComplexity.Deterministic.FiniteMessage.Protocol.comap_complexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} {X' : Type u_4} {Y' : Type u_5} (p : Protocol X Y α) (fX : X' → X) (fY : Y' → Y) : (p.comap fX fY).complexity = p.complexity