[FOM] Computer searches for combinatorial bijections
Timothy Y. Chow
tchow at alum.mit.edu
Tue Oct 10 15:06:56 EDT 2006
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
More information about the FOM
mailing list