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

A deterministic two-party communication protocol where Alice holds input x : X, Bob holds input y : Y, and the protocol computes a value of type α. At each step, either Alice or Bob sends a single bit based on their input, and the protocol branches accordingly.

• 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} (f : X → Bool) (P : Bool → Protocol X Y α) : Protocol X Y α
• bob {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : Y → Bool) (P : Bool → Protocol X Y α) : Protocol X Y α

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

Executes the protocol on inputs x and y, returning the output value.

Equations

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

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

The communication complexity of a protocol, i.e. the worst-case number of bits exchanged.

Equations

• (CommunicationComplexity.Deterministic.Protocol.output val).complexity = 0
• (CommunicationComplexity.Deterministic.Protocol.alice f P).complexity = 1 + max (P false).complexity (P true).complexity
• (CommunicationComplexity.Deterministic.Protocol.bob f P).complexity = 1 + max (P false).complexity (P true).complexity

def CommunicationComplexity.Deterministic.Protocol.Equiv {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p q : Protocol X Y α) : Prop

Two protocols are equivalent if they produce the same output on all inputs.

Equations

• p.Equiv q = (p.run = q.run)

def CommunicationComplexity.Deterministic.Protocol.Computes {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (f : X → Y → α) : Prop

A protocol computes a function f if it produces f x y on all inputs (x, y).

Equations

• p.Computes f = (p.run = f)

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

Swaps the roles of Alice and Bob, producing a protocol on Y × X from one on X × Y. Alice nodes become bob nodes and vice versa.

Equations

• (CommunicationComplexity.Deterministic.Protocol.output val).swap = CommunicationComplexity.Deterministic.Protocol.output val
• (CommunicationComplexity.Deterministic.Protocol.alice f P).swap = CommunicationComplexity.Deterministic.Protocol.bob f fun (b : Bool) => (P b).swap
• (CommunicationComplexity.Deterministic.Protocol.bob f P).swap = CommunicationComplexity.Deterministic.Protocol.alice f fun (b : Bool) => (P b).swap

@[simp]

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

@[simp]

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

@[simp]

theorem CommunicationComplexity.Deterministic.Protocol.swap_swap {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : p.swap.swap = p

Swapping Alice and Bob twice returns the original protocol.

theorem CommunicationComplexity.Deterministic.Protocol.alice_to_bob {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Bool) (P : Bool → Protocol X Y α) : ∃ (q : Protocol Y X α), (∀ (x : X) (y : Y), q.run y x = (alice f P).run x y) ∧ q.complexity = (alice f P).complexity

An alice protocol on X × Y can be converted into a bob protocol on Y × X with the same run behavior (up to argument swap) and complexity. Useful for reducing the bob case to the alice case in inductive proofs.

theorem CommunicationComplexity.Deterministic.Protocol.bob_to_alice {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : Y → Bool) (P : Bool → Protocol X Y α) : ∃ (q : Protocol Y X α), (∀ (x : X) (y : Y), q.run y x = (bob f P).run x y) ∧ q.complexity = (bob f P).complexity

A bob protocol on X × Y can be converted into an alice protocol on Y × X with the same run behavior (up to argument swap) and complexity. Useful for reducing the alice case to the bob case in inductive proofs.

def CommunicationComplexity.Deterministic.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 protocol along functions fX : X' → X and fY : Y' → Y. The resulting protocol over X' × Y' simulates the original by applying fX and fY to the inputs before each message function.

Equations

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

@[simp]

theorem CommunicationComplexity.Deterministic.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.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