[FOM] Re: Automated bijective proofs

[Timothy Y. Chow]

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