182 Communication Complexity — Indexing: Basic
182.1 Overview
This module introduces the Index problem \(\mathrm{IND}_n\): Alice holds an \(n\)-bit string \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), Bob holds an index \(i \in \mathrm{Fin}\, n\), and the answer is the bit \(x_i\). It defines the function and the trivial one-way protocol, shows that the deterministic one-way communication complexity of \(\mathrm{IND}_n\) is exactly \(n\) and that the two-way deterministic complexity is at most \(\lceil \log _2 n \rceil + 1\), and packages the uniform distribution on input pairs \((x, i)\) used by the distributional lower bound in the companion module. Throughout, \(n\) is a positive natural number.
182.2 Declarations
The Index function on \(n\) bits: given Alice’s string \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\) and Bob’s index \(i \in \mathrm{Fin}\, n\), it returns Alice’s \(i\)-th bit, \(\mathrm{indexing}_n(x, i) := x_i\).
The one-way protocol for Index in which Alice sends her entire string \(x\) as the message (the message type is \(\mathrm{Fin}\, n \to \mathrm{Bool}\) and the send map is the identity), and Bob outputs the \(i\)-th bit of the received message.
The deterministic one-way communication complexity of \(\mathrm{IND}_n\) is at most \(n\):
as witnessed by the trivial protocol in which Alice sends all \(n\) bits of her string.
The (two-way) deterministic communication complexity of \(\mathrm{IND}_n\) is at most \(\lceil \log _2 n \rceil + 1\):
where \(\lceil \log _2 n \rceil \) is formalised as \(\mathrm{Nat.clog}\, 2\, n\). This is the protocol in which Bob sends his index \(i\) and Alice replies with the single bit \(x_i\).
Every correct deterministic one-way protocol for \(\mathrm{IND}_n\) has cost at least \(n\); that is,
The deterministic one-way communication complexity of \(\mathrm{IND}_n\) is exactly \(n\):
The hard input distribution for Index: the uniform probability measure on pairs \((x, i)\) in \(\mathrm{BoolInput}\, n \times \mathrm{Fin}\, n\), so that Alice’s string \(x\) and Bob’s index \(i\) are chosen independently and uniformly at random. It is packaged as a finite probability space whose measure is \(\mathrm{uniformOn}\, \mathrm{Set.univ}\).