Karchmer--Wigderson protocols -- definitions

A protocol is indexed by its current zero-input and one-input rectangles. Alice partitions the one-input side and Bob partitions the zero-input side. At a leaf, one coordinate separates every zero input from every one input in the current rectangle.

inductive Complexity.KarchmerWigderson.Protocol (N : ℕ) : Set (BitString N) → Set (BitString N) → Type

A protocol for finding a coordinate where a zero input has value 0 and a one input has value 1.

The two Set indices record the current combinatorial rectangle. An Alice node partitions the one-input side; a Bob node partitions the zero-input side.

• leaf {N : ℕ} {zeroInputs oneInputs : Set (BitString N)} (index : Fin N) (zeroAt : ∀ input ∈ zeroInputs, input index = false) (oneAt : ∀ input ∈ oneInputs, input index = true) : Protocol N zeroInputs oneInputs

  A coordinate separating the entire current rectangle. The conditions are stated separately on the two sides, including for empty rectangles.

• alice {N : ℕ} {zeroInputs oneInputs : Set (BitString N)} (choice : BitString N → Bool) (ifFalse : Protocol N zeroInputs {input : BitString N | input ∈ oneInputs ∧ choice input = false}) (ifTrue : Protocol N zeroInputs {input : BitString N | input ∈ oneInputs ∧ choice input = true}) : Protocol N zeroInputs oneInputs

  Alice partitions the one-input side according to choice.

• bob {N : ℕ} {zeroInputs oneInputs : Set (BitString N)} (choice : BitString N → Bool) (ifFalse : Protocol N {input : BitString N | input ∈ zeroInputs ∧ choice input = false} oneInputs) (ifTrue : Protocol N {input : BitString N | input ∈ zeroInputs ∧ choice input = true} oneInputs) : Protocol N zeroInputs oneInputs

  Bob partitions the zero-input side according to choice.

def Complexity.KarchmerWigderson.Protocol.depth {N : ℕ} {zeroInputs oneInputs : Set (BitString N)} : Protocol N zeroInputs oneInputs → ℕ

Worst-case communication depth. Leaves have depth zero and every message adds one.

Equations

• (Complexity.KarchmerWigderson.Protocol.leaf index zeroAt oneAt).depth = 0
• (Complexity.KarchmerWigderson.Protocol.alice choice ifFalse ifTrue).depth = max ifFalse.depth ifTrue.depth + 1
• (Complexity.KarchmerWigderson.Protocol.bob choice ifFalse ifTrue).depth = max ifFalse.depth ifTrue.depth + 1

def Complexity.KarchmerWigderson.Protocol.toFormula {N : ℕ} {zeroInputs oneInputs : Set (BitString N)} : Protocol N zeroInputs oneInputs → MonotoneFormula N

Translate a protocol tree to a monotone formula. Alice nodes become disjunctions and Bob nodes become conjunctions.

Equations

• (Complexity.KarchmerWigderson.Protocol.leaf index zeroAt oneAt).toFormula = Complexity.MonotoneFormula.var index
• (Complexity.KarchmerWigderson.Protocol.alice choice ifFalse ifTrue).toFormula = ifFalse.toFormula.disj ifTrue.toFormula
• (Complexity.KarchmerWigderson.Protocol.bob choice ifFalse ifTrue).toFormula = ifFalse.toFormula.conj ifTrue.toFormula

def Complexity.KarchmerWigderson.zeroFiber {N : ℕ} (function : BitString N → Bool) : Set (BitString N)

The zero fiber of a Boolean function.

Equations

• Complexity.KarchmerWigderson.zeroFiber function = {input : Complexity.BitString N | function input = false}

def Complexity.KarchmerWigderson.oneFiber {N : ℕ} (function : BitString N → Bool) : Set (BitString N)

The one fiber of a Boolean function.

Equations

• Complexity.KarchmerWigderson.oneFiber function = {input : Complexity.BitString N | function input = true}

@[reducible, inline]

abbrev Complexity.KarchmerWigderson.RootProtocol {N : ℕ} (function : BitString N → Bool) : Type

A root protocol for the monotone Karchmer--Wigderson relation of function.

Equations

• Complexity.KarchmerWigderson.RootProtocol function = Complexity.KarchmerWigderson.Protocol N (Complexity.KarchmerWigderson.zeroFiber function) (Complexity.KarchmerWigderson.oneFiber function)