[FOM] Computer searches for combinatorial bijections

[Timothy Y. Chow]

Doron Zeilberger gave a talk at Harvey Mudd College this past Saturday 
entitled, "Beautiful and Insightful Computer-Generated Bijective Proofs."  
This described some preliminary research into the problem of automatically 
discovering proofs of a certain special type, namely proofs that construct 
explicit bijections between two classes of combinatorial objects.

Elegant bijective proofs are prized by many combinatorialists; one can get 
considerable accolades for finding a bijective proof of a result that 
previously had no known bijective proof, or even for finding a bijection 
that is considerably nicer than previously known bijections (the bijective 
proof by Pak, Novelli, and Stoyanovskii of the hook-length formula for 
standard Young tableaux is a good example).  Currently, constructing 
bijective proofs is something of a "black art," requiring large doses of 
human ingenuity.  On the other hand, it is a sufficiently narrowly defined 
domain that computerizing it doesn't seem hopeless.

The examples described by Zeilberger still require the programmer to 
create data structures and algorithms that are highly specific to the 
particular pair of combinatorial objects in question.  But ideally, one 
would like to create a general environment with a language that is 
flexible enough to allow the description of a wide variety of 
combinatorial objects.  The user would then describe two classes of 
combinatorial objects in this formal language, and the program would then 
go off in search of a bijection between the two, returning with a 
description of a bijection and a proof that it is correct.  Even without a 
proof of correctness, such a program could be enormously valuable, since 
in many cases the hard part of a bijective proof is coming up with a 
candidate bijection in the first place.

The question I have is, is there any existing environment or language that 
might be adaptable to such a project?

I'll say a little bit more about what I have in mind, at least for the 
case in which the computer just searches for bijections without proving 
anything.  A "combinatorial object" or a "class of combinatorial objects" 
would be something like a countable union of finite sets S_1, S_2, S_3, 
... of finite structures.  So for example, S_n might be the set of all 
binary words of length n, or the set of all permutations of an n-element 
set, or the set of all standard Young tableaux with n cells.  (Actually 
one probably wants to allow indexing by multiple subscripts, e.g., S_{m,n} 
might be the set of all partitions of an n-element subset into m blocks, 
but I'll stick to one subscript to keep the notation uncluttered.)  The 
first problem is that one cannot directly present a countably infinite set 
to a computer, so we have to decide how to represent it.  Whatever choice 
we make, it should allow the computer to generate, for any given n, the 
set S_n.

Given two classes S = {S_n} and T = {T_n}, the computer would then need 
to, in some systematic fashion, explore the space of bijections between S 
and T---or rather, the space of maps from S into T that take S_n into 
T_n.  The exploration procedure, in its most naive form, would consist of
enumerating all possible maps from S into T---a map would be a *rule* for 
taking an element of S_n to an element of T_n---and, for each map, 
applying it to S_n and seeing if it produces T_n.  If the map sends two 
different elements of S_n to the same element of T_n then it is obviously 
not a bijection and so one would stop and go on to the next candidate.  If 
a particular map seems to work for a lot of values of n then at some point 
one would output it as a promising candidate and either terminate the 
search or keep looking for other candidates.

What's still unclear from this description is exactly what kind of 
language to use to describe combinatorial objects and maps between them 
that would allow such a search procedure to be executed in a manner that 
is not hopelessly inefficient.  If all we cared about was empirically 
testing the hypothesis that there *exists* a bijection between S_n and 
T_n, without constructing it explicitly, then all we would need to do is 
to find the sizes of the sets S_n and T_n and test for numerical equality.  
But we want more than that; we want to be able to describe maps that say 
something like, "take the smallest j > i to the right of i and move it to 
the end and then..."  Even if we don't set our sights very high and 
restrict ourselves to a rather limited class of combinatorial objects, I'm 
not sure what a good representation might be.  I suspect that Joyal's 
theory of species may be helpful, but as it stands, the theory of species 
is still too abstract for the kind of application I have in mind here.

Any suggestions?

Tim