[FOM] Automated bijective proofs

[Jacques Carette]

"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 
more information.

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.

Jacques