Karchmer–Wigderson games

A De Morgan formula has literal and constant leaves and binary AND and OR gates. The Karchmer–Wigderson game of f gives Alice an input x with f x = 1 and Bob an input y with f y = 0; they must agree on a coordinate where x and y differ. A deterministic protocol is a binary tree whose internal nodes are owned by one player and branch on that player's input, and whose leaves name a coordinate.

The Karchmer–Wigderson theorem says that formulas and protocols are the same trees: an OR gate is a node where Alice says which side of the disjunction her input satisfies, an AND gate is a node where Bob says which side his input violates, and a literal leaf names its coordinate (Formula.toProtocol). Conversely a protocol induces, at every node, a rectangle of inputs still consistent with the transcript, and the formula built with OR at Alice's nodes and AND at Bob's nodes is 1 on Alice's side and 0 on Bob's side of every rectangle (Protocol.toFormula). Depth and leaf count are preserved in both directions, so for n ≥ 1 the minimum formula depth of f equals the minimum protocol depth of its game (formulaDepth_eq_protocolDepth), and likewise for leaf size (formulaSize_eq_protocolSize). Both need [NeZero n]: with no coordinates there is no protocol at all (a leaf must name a coordinate), so the protocol measures are ⊤, while a constant formula has depth 0.

De Morgan formulas

inductive Algebraic.KW.Formula (n : ℕ) : Type

A De Morgan formula: literal leaves, constants, binary AND and OR.

• lit {n : ℕ} (index : Fin n) (positive : Bool) : Formula n

  The literal x_i when positive, otherwise ¬ x_i.

• const {n : ℕ} (value : Bool) : Formula n

  A Boolean constant.

• and {n : ℕ} (left right : Formula n) : Formula n

  Conjunction.

• or {n : ℕ} (left right : Formula n) : Formula n

  Disjunction.

def Algebraic.KW.Formula.eval {n : ℕ} : Formula n → (Fin n → Bool) → Bool

Evaluate a formula.

Equations

• (Algebraic.KW.Formula.lit i b).eval x✝ = (x✝ i == b)
• (Algebraic.KW.Formula.const b).eval x✝ = b
• (l.and r).eval x✝ = (l.eval x✝ && r.eval x✝)
• (l.or r).eval x✝ = (l.eval x✝ || r.eval x✝)

@[simp]

theorem Algebraic.KW.Formula.eval_lit {n : ℕ} (i : Fin n) (b : Bool) (x : Fin n → Bool) : (lit i b).eval x = (x i == b)

@[simp]

theorem Algebraic.KW.Formula.eval_const {n : ℕ} (b : Bool) (x : Fin n → Bool) : (const b).eval x = b

@[simp]

theorem Algebraic.KW.Formula.eval_and {n : ℕ} (l r : Formula n) (x : Fin n → Bool) : (l.and r).eval x = (l.eval x && r.eval x)

@[simp]

theorem Algebraic.KW.Formula.eval_or {n : ℕ} (l r : Formula n) (x : Fin n → Bool) : (l.or r).eval x = (l.eval x || r.eval x)

def Algebraic.KW.Formula.depth {n : ℕ} : Formula n → ℕ

The depth: the longest root-to-leaf path.

Equations

• (Algebraic.KW.Formula.lit index positive).depth = 0
• (Algebraic.KW.Formula.const value).depth = 0
• (l.and r).depth = max l.depth r.depth + 1
• (l.or r).depth = max l.depth r.depth + 1

def Algebraic.KW.Formula.leaves {n : ℕ} : Formula n → ℕ

The number of leaves, counting literals and constants, so every formula has at least one leaf. This differs from Algebraic.Binary.Formula.leaves, which counts only variable leaves and gives constants leaf size 0; formulaSize and the KRW statements use this convention.

Equations

• (Algebraic.KW.Formula.lit index positive).leaves = 1
• (Algebraic.KW.Formula.const value).leaves = 1
• (l.and r).leaves = l.leaves + r.leaves
• (l.or r).leaves = l.leaves + r.leaves

theorem Algebraic.KW.Formula.one_le_leaves {n : ℕ} (F : Formula n) : 1 ≤ F.leaves

def Algebraic.KW.Formula.neg {n : ℕ} : Formula n → Formula n

The De Morgan dual, computing the negation with the same shape.

Equations

• (Algebraic.KW.Formula.lit index positive).neg = Algebraic.KW.Formula.lit index !positive
• (Algebraic.KW.Formula.const value).neg = Algebraic.KW.Formula.const !value
• (l.and r).neg = l.neg.or r.neg
• (l.or r).neg = l.neg.and r.neg

@[simp]

theorem Algebraic.KW.Formula.eval_neg {n : ℕ} (F : Formula n) (x : Fin n → Bool) : F.neg.eval x = !F.eval x

@[simp]

theorem Algebraic.KW.Formula.depth_neg {n : ℕ} (F : Formula n) : F.neg.depth = F.depth

@[simp]

theorem Algebraic.KW.Formula.leaves_neg {n : ℕ} (F : Formula n) : F.neg.leaves = F.leaves

def Algebraic.KW.Formula.Computes {n : ℕ} (F : Formula n) (f : Cslib.BooleanFunction n) : Prop

A formula computes f when it agrees with f everywhere.

Equations

• F.Computes f = ∀ (x : Fin n → Bool), F.eval x = f x

Protocols

inductive Algebraic.KW.Protocol (n : ℕ) : Type

A deterministic two-party protocol whose leaves name a coordinate. Each internal node is owned by Alice or Bob and branches on the owner's input.

• answer {n : ℕ} (index : Fin n) : Protocol n

  Output a coordinate.

• alice {n : ℕ} (choose : (Fin n → Bool) → Bool) (left right : Protocol n) : Protocol n

  Alice branches on her input; true selects the right child.

• bob {n : ℕ} (choose : (Fin n → Bool) → Bool) (left right : Protocol n) : Protocol n

  Bob branches on his input; true selects the right child.

def Algebraic.KW.Protocol.run {n : ℕ} : Protocol n → (Fin n → Bool) → (Fin n → Bool) → Fin n

The coordinate output on inputs x for Alice and y for Bob.

Equations

• (Algebraic.KW.Protocol.answer i).run x✝¹ x✝ = i
• (Algebraic.KW.Protocol.alice c l r).run x✝¹ x✝ = if c x✝¹ = true then r.run x✝¹ x✝ else l.run x✝¹ x✝
• (Algebraic.KW.Protocol.bob c l r).run x✝¹ x✝ = if c x✝ = true then r.run x✝¹ x✝ else l.run x✝¹ x✝

def Algebraic.KW.Protocol.depth {n : ℕ} : Protocol n → ℕ

The depth: the longest root-to-leaf path.

Equations

• (Algebraic.KW.Protocol.answer index).depth = 0
• (Algebraic.KW.Protocol.alice choose l r).depth = max l.depth r.depth + 1
• (Algebraic.KW.Protocol.bob choose l r).depth = max l.depth r.depth + 1

def Algebraic.KW.Protocol.leaves {n : ℕ} : Protocol n → ℕ

The number of leaves.

Equations

• (Algebraic.KW.Protocol.answer index).leaves = 1
• (Algebraic.KW.Protocol.alice choose l r).leaves = l.leaves + r.leaves
• (Algebraic.KW.Protocol.bob choose l r).leaves = l.leaves + r.leaves

def Algebraic.KW.Protocol.Solves {n : ℕ} (P : Protocol n) (A B : (Fin n → Bool) → Prop) : Prop

The protocol solves the game on the rectangle A × B: on inputs from A for Alice and B for Bob, the output coordinate distinguishes them.

Equations

• P.Solves A B = ∀ (x y : Fin n → Bool), A x → B y → x (P.run x y) ≠ y (P.run x y)

def Algebraic.KW.Protocol.SolvesKW {n : ℕ} (P : Protocol n) (f : Cslib.BooleanFunction n) : Prop

The protocol solves the Karchmer–Wigderson game of f.

Equations

• P.SolvesKW f = P.Solves (fun (x : Fin n → Bool) => f x = true) fun (y : Fin n → Bool) => f y = false

From formulas to protocols

def Algebraic.KW.Formula.toProtocol {n : ℕ} (i₀ : Fin n) : Formula n → Protocol n

The protocol of a formula: Bob resolves conjunctions, Alice resolves disjunctions, literals name their coordinate. A constant leaf, which can only be reached on an empty rectangle, answers the default coordinate i₀.

Equations

• Algebraic.KW.Formula.toProtocol i₀ (Algebraic.KW.Formula.lit index positive) = Algebraic.KW.Protocol.answer index
• Algebraic.KW.Formula.toProtocol i₀ (Algebraic.KW.Formula.const value) = Algebraic.KW.Protocol.answer i₀
• Algebraic.KW.Formula.toProtocol i₀ (l.and r) = Algebraic.KW.Protocol.bob (fun (y : Fin n → Bool) => l.eval y) (Algebraic.KW.Formula.toProtocol i₀ l) (Algebraic.KW.Formula.toProtocol i₀ r)
• Algebraic.KW.Formula.toProtocol i₀ (l.or r) = Algebraic.KW.Protocol.alice (fun (x : Fin n → Bool) => !l.eval x) (Algebraic.KW.Formula.toProtocol i₀ l) (Algebraic.KW.Formula.toProtocol i₀ r)

theorem Algebraic.KW.Formula.toProtocol_solves {n : ℕ} (i₀ : Fin n) (F : Formula n) : (toProtocol i₀ F).SolvesKW F.eval

@[simp]

theorem Algebraic.KW.Formula.depth_toProtocol {n : ℕ} (i₀ : Fin n) (F : Formula n) : (toProtocol i₀ F).depth = F.depth

@[simp]

theorem Algebraic.KW.Formula.leaves_toProtocol {n : ℕ} (i₀ : Fin n) (F : Formula n) : (toProtocol i₀ F).leaves = F.leaves

From protocols to formulas

noncomputable def Algebraic.KW.Protocol.toFormula {n : ℕ} : Protocol n → ((Fin n → Bool) → Prop) → ((Fin n → Bool) → Prop) → Formula n

The formula of a protocol, relative to the rectangle A × B of inputs reaching the current node: OR at Alice's nodes, AND at Bob's nodes, and at a leaf naming i the literal that is 1 on A and 0 on B.

Equations

• One or more equations did not get rendered due to their size.
• (Algebraic.KW.Protocol.alice c l r).toFormula x✝¹ x✝ = (l.toFormula (fun (x : Fin n → Bool) => x✝¹ x ∧ c x = false) x✝).or (r.toFormula (fun (x : Fin n → Bool) => x✝¹ x ∧ c x = true) x✝)
• (Algebraic.KW.Protocol.bob c l r).toFormula x✝¹ x✝ = (l.toFormula x✝¹ fun (y : Fin n → Bool) => x✝ y ∧ c y = false).and (r.toFormula x✝¹ fun (y : Fin n → Bool) => x✝ y ∧ c y = true)

theorem Algebraic.KW.Protocol.toFormula_spec {n : ℕ} (P : Protocol n) (A B : (Fin n → Bool) → Prop) : P.Solves A B → (∀ (x : Fin n → Bool), A x → (P.toFormula A B).eval x = true) ∧ ∀ (y : Fin n → Bool), B y → (P.toFormula A B).eval y = false

The formula of a protocol solving the game on A × B is 1 on A and 0 on B.

@[simp]

theorem Algebraic.KW.Protocol.depth_toFormula {n : ℕ} (P : Protocol n) (A B : (Fin n → Bool) → Prop) : (P.toFormula A B).depth = P.depth

@[simp]

theorem Algebraic.KW.Protocol.leaves_toFormula {n : ℕ} (P : Protocol n) (A B : (Fin n → Bool) → Prop) : (P.toFormula A B).leaves = P.leaves

theorem Algebraic.KW.Protocol.exists_formula_of_solvesKW {n : ℕ} {P : Protocol n} {f : Cslib.BooleanFunction n} (h : P.SolvesKW f) : ∃ (F : Formula n), F.Computes f ∧ F.depth = P.depth ∧ F.leaves = P.leaves

A protocol for the game of f yields a formula for f of the same shape.

The Karchmer–Wigderson theorem

theorem Algebraic.KW.Formula.exists_protocol_of_computes {n : ℕ} (i₀ : Fin n) {F : Formula n} {f : Cslib.BooleanFunction n} (h : F.Computes f) : ∃ (P : Protocol n), P.SolvesKW f ∧ P.depth = F.depth ∧ P.leaves = F.leaves

A formula for f yields a protocol for its game of the same shape.

noncomputable def Algebraic.KW.formulaDepth {n : ℕ} (f : Cslib.BooleanFunction n) : ℕ∞

The minimum depth of a formula computing f.

Equations

• Algebraic.KW.formulaDepth f = ⨅ (F : { F : Algebraic.KW.Formula n // F.Computes f }), ↑(↑F).depth

noncomputable def Algebraic.KW.formulaSize {n : ℕ} (f : Cslib.BooleanFunction n) : ℕ∞

The minimum number of leaves of a formula computing f.

Equations

• Algebraic.KW.formulaSize f = ⨅ (F : { F : Algebraic.KW.Formula n // F.Computes f }), ↑(↑F).leaves

noncomputable def Algebraic.KW.protocolDepth {n : ℕ} (f : Cslib.BooleanFunction n) : ℕ∞

The minimum depth of a protocol for the game of f.

Equations

• Algebraic.KW.protocolDepth f = ⨅ (P : { P : Algebraic.KW.Protocol n // P.SolvesKW f }), ↑(↑P).depth

noncomputable def Algebraic.KW.protocolSize {n : ℕ} (f : Cslib.BooleanFunction n) : ℕ∞

The minimum number of leaves of a protocol for the game of f.

Equations

• Algebraic.KW.protocolSize f = ⨅ (P : { P : Algebraic.KW.Protocol n // P.SolvesKW f }), ↑(↑P).leaves

theorem Algebraic.KW.formulaDepth_le {n : ℕ} {F : Formula n} {f : Cslib.BooleanFunction n} (h : F.Computes f) : formulaDepth f ≤ ↑F.depth

theorem Algebraic.KW.formulaSize_le {n : ℕ} {F : Formula n} {f : Cslib.BooleanFunction n} (h : F.Computes f) : formulaSize f ≤ ↑F.leaves

theorem Algebraic.KW.protocolDepth_le {n : ℕ} {P : Protocol n} {f : Cslib.BooleanFunction n} (h : P.SolvesKW f) : protocolDepth f ≤ ↑P.depth

theorem Algebraic.KW.protocolSize_le {n : ℕ} {P : Protocol n} {f : Cslib.BooleanFunction n} (h : P.SolvesKW f) : protocolSize f ≤ ↑P.leaves

theorem Algebraic.KW.formulaDepth_eq_protocolDepth {n : ℕ} [NeZero n] (f : Cslib.BooleanFunction n) : formulaDepth f = protocolDepth f

Karchmer–Wigderson, depth. For n ≥ 1, the minimum formula depth of f is the minimum depth of a protocol for its game.

theorem Algebraic.KW.formulaSize_eq_protocolSize {n : ℕ} [NeZero n] (f : Cslib.BooleanFunction n) : formulaSize f = protocolSize f

Karchmer–Wigderson, size. For n ≥ 1, the minimum leaf size of a formula for f is the minimum number of leaves of a protocol for its game.