[FOM] Computer searches for combinatorial bijections

[Timothy Y. Chow]

I'm picking up this old thread from a few months ago, because I have a 
small additional insight.  Mitchell Harris reminded me that I broached the 
same topic ("Automated bijective proofs") back in 2004.

On Wed, 11 Oct 2006, Jacques Carette wrote:
> The framework of species gives one a lot of canonical maps and tools 
> between species, which help tremendously in the automation of possible 
> bijections.

Having just finished a paper in which I constructed a couple of nontrivial 
bijections between sets of lattice paths in the plane---partly aided by 
generating function manipulations---I have an additional observation about 
what seems to be involved here.

Canonical maps are certainly important, and categories/species are 
certainly helpful as a language for them.  However, when a 
combinatorialist seeks an *explicit bijection*, usually this is something 
decidedly *non-canonical*.  The (verbal) description of the bijection 
typically involves some non-canonical choices, e.g., "pick the first node 
with such-and-such a property and then..."  Another way to put it is that 
one attaches labels to unlabeled structures, or one tries to "remember" 
what some forgetful functor forgot.

In my lattice-path example, I had conjectured that two sets of lattice 
paths were equinumerous.  I derived a generating function equation from 
the conjecture, manipulated it to an equivalent but different-looking 
form, and then stared at it, asking, "What are these terms counting?"  
Using intuition or guesswork or whatever you call it, I eventually 
constructed the appropriate combinatorial structure that allowed the 
bijection to be constructed.  Given the structure, passing to the 
generating function was a functorial forgetting process, but finding the 
proof required going in the opposite direction.

Therefore what an automated search for candidate bijections needs to do is 
to try a bunch of "possible labelings" of the given objects and look for 
canonical maps between the tentatively labeled objects.  The space of 
possible labelings is vast and hence a lot of thought needs to go into the 
problem of structuring this space so that it can be explored fruitfully.  
However, if this hurdle can be surmounted then potentially a computer can 
search the space much better than an unaided human can.

To make further progress I think one needs to fix a toy domain that is 
relatively well understood and that one can play with concretely.  I'm not 
sure what a good candidate would be.

Tim Chow