Symmetric Formulas for Products of Permutations

We study the formula complexity of the word problem Word_{S_n,k} : {0,1}^{kn²} → {0,1}: given n-by-n permutation matrices M₁,… ,M_k, compute the (1,1)-entry of the matrix product M₁⋯ M_k. An important feature of this function is that it is invariant under action of S_n^{k-1} given by (π₁,… ,π_{k-1})(M₁,… ,M_k) = (M₁π₁^{-1},π₁M₂π₂^{-1},… ,π_{k-2}M_{k-1}π_{k-1}^{-1},π_{k-1}M_k). This symmetry is also exhibited in the smallest known unbounded fan-in {and,or,not}-formulas for Word_{S_n,k}, which have size n^O(log k). In this paper we prove a matching n^{Ω(log k)} lower bound for S_n^{k-1}-invariant formulas computing Word_{S_n,k}. This result is motivated by the fact that a similar lower bound for unrestricted (non-invariant) formulas would separate complexity classes NC¹ and Logspace. Our more general main theorem gives a nearly tight n^d(k^{1/d}-1) lower bound on the G^{k-1}-invariant depth-d {maj,and,or,not}-formula size of Word_{G,k} for any finite simple group G whose minimum permutation representation has degree n. We also give nearly tight lower bounds on the G^{k-1}-invariant depth-d {and,or,not}-formula size in the case where G is an abelian group.