[FOM] Automated bijective proofs
carette at mcmaster.ca
Tue Jun 29 15:10:58 EDT 2004
"Timothy Y. Chow" <tchow at alum.mit.edu> wrote:
> I wonder if there has been any effort to automate the process of finding
> bijective proofs in combinatorics?
There is a wealth of knowledge in the ``enumerative combinatorics'' community which deals with this in many ways,
although I am not aware of any project to attack your problem directly.
Indirectly however, there are two clearly relevant research threads: Joyal's Theory of Species and the work of the
ALGO project at INRIA (http://algo.inria.fr).
Species represent combinatorial structures via endofunctors of (FinSet, bijection). However, all the theory is always
presented in a very constructive fashion, with operations of sum, product, substitution and (!) derivative being
explicitly given, and then used to generate most structures in common use. One can then naturally associate various
formal series to these objects; isomorphic (under various definitions) structures give equal formal series. There is
a wonderful exposition of all this theory in the very readable book
Combinatorial Species and Tree-like Structures by Bergeron, F., Labelle, G. and Leroux, P.
Note that although there is a lot of category theory lurking about, the authors are writing for an audience of
combinatorialists, and thus eschew actually using category theory in their exposition.
In any case, one of the big ideas in the book is that most natural combinatorial species are ``properly'' viewed as
solutions of *combinatorial differential equations on species*. These DEs are the key to much of the theory.
This is where the work of the ALGO project comes in. They are working on using Computer Algebra to automate as many
parts of Combinatorics as current technology allows. The theory of holonomic functions is their ``key''. This of
course is exactly the bridge to combinatorics as seen above, via generating functions. See their web site for a lot
The global approach to automated proofs of bijection is then to give constructions of two different combinatorial
objects, derive (automatically) which combinatorial differential equations these satisfy, and then show that these are
in fact ``the same''. The hardest part is actually to give a construction of the combinatorial objects starting just
from the primitives of Species; this part of the theory is now mature enough that there are an increasing number
techniques that have been developped to achieve this.
The really amazing part is that not only can one show bijections, one can often also obtain (exact!) asymptotic
information about various statistics on these combinatorial objects, in a completely automated fashion.
Caveat: I am not an expert in this area, but I was co-located with the ALGO group for 3 years.
More information about the FOM