[FOM] Computer searches for combinatorial bijections
Timothy Y. Chow
tchow at alum.mit.edu
Wed Feb 28 10:47:44 EST 2007
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
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.
More information about the FOM