bisc

Hjalti Magnússon and Henning Úlfarsson

"Algorithms for discovering and proving theorems involving permutation patterns"

Theorems relating permutations with objects in other fields of mathematics are often stated in terms of avoided patterns. Examples include various classes of Schubert varieties from algebraic geometry (Billey and Abe 2013), commuting functions in analysis (Baxter 1964), beta-shifts in dynamical systems (Elizalde 2011) and homology of representations (Sundaram 1994). We present a new algorithm, called BiSC, that describes the patterns avoided by a given set of permutations, and automatically conjectures the statements of known theorems such as the descriptions of smooth (Lakshmibai and Sandhya 1990) and forest-like permutations (Bousquet-Melou and Butler 2007), Baxter permutations (Chung et al. 1978), stack-sortable (Knuth 1975) and West-2-stack-sortable permutations (West 1990). The algorithm has also been used to discover new theorems related to the dihedral and alternating subgroups of the symmetric group, Young tableaux, Wilf-equivalences and sorting devices. We further provide a general framework for algorithms that not only conjecture, but prove, a complete description of preimages of pattern classes under several sorting devices. These provide proofs of the theorems of Knuth and West mentioned above, as well as allowing us to give the first linear-time algorithm for finding occurrences of a non-monotone pattern of length four.