[FOM] Re: Automated bijective proofs
Timothy Y. Chow
tchow at alum.mit.edu
Tue Jun 29 16:29:14 EDT 2004
On Tue, 29 Jun 2004, Jacques Carette wrote:
> 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).
Thanks for the information. I know about species, but didn't know about
the project to use that theory to automate combinatorics. Such work would
certainly be relevant to my question, although my first instinct is to
suspect that it's almost the inverse problem---i.e., finding algebraic
proofs of combinatorial facts, rather than finding combinatorial proofs
of facts that are already known to be true by algebraic means. Going
from one combinatorial object to another via generating functions and
differential equations seems to me to be a circuitous route that is not,
in general, going to be the simplest way. It is akin to the Garsia-Milne
involution principle and other "brute-force" methods that mechanically
mimic algebraic operations with combinatorial constructions and that
typically don't yield much insight beyond the algebraic proof itself.
Here's an example I thought of that illustrates a difference between
combinatorics and algebra. If K is an invertible matrix, then it is an
algebraically trivial fact that K*K^(-1) = K^(-1)*K. However, there are
cases in which there are combinatorial interpretations of the entries of K
and K^(-1) and a combinatorial proof of K*K^(-1) = I, but no known
combinatorial proof that K^(-1)*K = I. One example is the case where K is
the so-called "Kostka matrix." See
O. Egecioglu and J. Remmel, "A combinatorial intepretation of the
inverse Kostka matrix," Lin. Multilin. Alg. 26 (1990), 59-84
B. Sagan and J. Lee, "An algorithmic sign-reversing involution for
special rim-hook tableaux," J. Algorithms B, to appear (available on
Bruce Sagan's homepage)
Tim
More information about the FOM
mailing list