The index gadget and lifted search problems

A search problem on n bits is a relation R : (Fin n → Bool) → O → Prop: on input z, any o with R z o is a correct answer. Composing it with n copies of the index gadget Ind_m : [m] × {0, 1}^m → {0, 1}, Ind_m (a, w) = w a, gives a two-party search problem. Alice holds pointers x : Fin n → Fin m, Bob holds blocks y : Fin n → Fin m → Bool, and the i-th input bit is y i (x i) (Communication.Lifting.ind). The lifted problem Communication.Lifting.lift R asks for an answer to R on that input Göös, Pitassi and Watson.

A decision tree for R gives a protocol for the lifted problem: to query bit i, Alice sends x i in ⌈log₂ m⌉ bits and Bob answers with y i (x i) (Communication.Lifting.ofDecisionTree). So the communication complexity of the lifted problem is at most ⌈log₂ m⌉ + 1 times the depth of any decision tree for R (Communication.Lifting.ecomplexity_lift_le) Göös, Pitassi and Watson, (1). The lifting theorem says that this protocol is optimal up to a constant factor when m is a large enough polynomial in n.

Main definitions

• Cslib.Communication.Lifting.ind: n copies of the index gadget.
• Cslib.Communication.Lifting.lift: the lifted search problem.
• Cslib.Communication.Lifting.ofDecisionTree: the protocol simulating a decision tree.

Main results

• Cslib.Communication.Lifting.run_ofDecisionTree, Cslib.Communication.Lifting.depth_ofDecisionTree_le: the simulation is correct and costs ⌈log₂ m⌉ + 1 bits per query.
• Cslib.Communication.Lifting.ecomplexity_lift_le: the upper bound of the lifting theorem.

References

• M. Göös, T. Pitassi and T. Watson, Deterministic communication vs. partition number
• R. Raz and P. McKenzie, Separation of the monotone NC hierarchy

def Cslib.Communication.Lifting.ind {n m : ℕ} (x : Fin n → Fin m) (y : Fin n → Fin m → Bool) : Fin n → Bool

n copies of the index gadget: the i-th bit is the bit of Bob's block y i at Alice's pointer x i.

@[simp]

theorem Cslib.Communication.Lifting.ind_apply {n m : ℕ} (x : Fin n → Fin m) (y : Fin n → Fin m → Bool) (i : Fin n) : ind x y i = y i (x i)

def Cslib.Communication.Lifting.lift {n m : ℕ} {O : Type u_1} (R : (Fin n → Bool) → O → Prop) : (Fin n → Fin m) → (Fin n → Fin m → Bool) → O → Prop

The search problem R lifted by the index gadget: Alice holds x, Bob holds y, and o is a correct answer when it answers R on ind x y.

def Cslib.Communication.Lifting.ofDecisionTree {n m : ℕ} {O : Type u_1} : DecisionTree (Fin n) O → Protocol (Fin n → Fin m) (Fin n → Fin m → Bool) O

The protocol simulating a decision tree: to query bit i, Alice sends the binary numeral of x i, and Bob announces y i (x i).

@[simp]

theorem Cslib.Communication.Lifting.run_ofDecisionTree {n m : ℕ} {O : Type u_1} (t : DecisionTree (Fin n) O) (x : Fin n → Fin m) (y : Fin n → Fin m → Bool) : (ofDecisionTree t).run x y = t.eval (ind x y)

The simulating protocol outputs what the decision tree outputs on ind x y.

theorem Cslib.Communication.Lifting.depth_ofDecisionTree_le {n m : ℕ} {O : Type u_1} (t : DecisionTree (Fin n) O) : (ofDecisionTree t).depth ≤ t.depth * (Nat.clog 2 m + 1)

Each query costs ⌈log₂ m⌉ + 1 bits.

theorem Cslib.Communication.Lifting.ecomplexity_lift_le {n m : ℕ} {O : Type u_1} {R : (Fin n → Bool) → O → Prop} {t : DecisionTree (Fin n) O} (ht : ∀ (z : Fin n → Bool), R z (t.eval z)) : Protocol.ecomplexity (lift R) Set.univ Set.univ ≤ ↑(t.depth * (Nat.clog 2 m + 1))

The upper bound of the lifting theorem. If a decision tree of depth d solves R, then the lifted problem has communication complexity at most d (⌈log₂ m⌉ + 1) Göös, Pitassi and Watson, (1).