"The power of expander-based reasoning"
Antonina Kolokolova
(Memorial University of Newfoundland)
Monday, May 16th, 2016, 2:00 pm
EBU3B, Room 4258
Abstract:
Several major results in complexity theory such as undirected graph reachability in logspace (Reingold, Rozenman-Vadhan) and monotone formulas for sorting (Ajtai-Komlos-Szemeredi sorting networks) are based on properties of expander graphs. However, the original constructions of expander graphs use algebraic reasoning, proving bounds on the spectral gap; subsequent more combinatorial constructions also use spectral gap at least for some of the analysis.
I will talk about our work in progress with Sam Buss, Valentine Kabanets and Michal Koucky on a fully combinatorial construction of expander graphs, which we are working on formalizing in the theory of NC1 reasoning. Together with Jerabek's formalization of AKS sorting networks in such theory, this would show that monotone sequent calculus MLK can polynomially simulate non-monotone sequent calculus LK with respect to monotone sequents, improving on quasipolynomial simulation by Atserias, Galesi and Pudlak.
The talk will be fairly non-technical, in particular I am assuming no background in bounded arithmetic.