# Richard Stanley, Captain of Counting

I recently received an email about a math conference in honor of Richard Stanley’s 70th birthday. For those of you who don’t know, Stanley is an expert in combinatorics and author of the two volume magnum opus Enumerative Combinatorics which (among a bunch of other very interesting math) champions the idea of the combinatorial proof—a way of proving a combinatorial identity by showing that both sides of the equation are in different fact ways of counting the same thing.

Stanley’s Enumerative Combinatorics also goes into great detail about the Catalan Numbers, a sequence of numbers that arises in tree enumeration problems. In fact, Stanley’s interest in these numbers—which he dubs ‘‘Catalan disease’’ or ‘‘Catalania’’—goes so far that he offers 66 combinatorial interpretations of them in EC vol. 2 and dozens more in an addendum published online. See the OEIS page for more.

# Catalania, meet Haskell

In the interest of learning more Haskell, I decided to take some inspiration and play with Catalan numbers in that decidedly mathematical programming language. To start off with, I have some helpful imports and auxiliary functions:

The QuickCheck import will be important later.

Next, with the help of Rosetta Code and Wikipedia, I have the following Catalan Number definitions:

Finally, we’d like to show (or at least, verify for a certain number of test cases) that these varying definitions all describe the same thing; to do that, I decided to use a bit of QuickCheck’s magic to test various items from these lists for equality:

This isn’t perhaps the most elegant check—note that I restrict the integers tested to \( \lbrace 0, 1, \ldots, 999 \rbrace = \phantom{ }^\mathbb{Z} /_{1000 \mathbb{Z}} \) to make sure that indices are nonnegative and we don’t overtax my poor laptop’s CPU. Of course, I’m open to criticism from any Haskell/QuickCheck gurus who’d like to help me tighten up my code. Feel free to download the code.

# To Be Continued

That was fun; programming in Haskell almost always is, for me, and I’m by no
means an expert.
However, it leaves a little to be desired.
The program above at best demonstrates that the various infinite lists agree at
several (pseudo-)randomly chosen indices.
I suppose that taking this to the next level would involve some sort of
automatic theorem proving
assistant—Agda comes to
mind, due to its relationship with Haskell.
That being said, using something like Agda will at best give me *algebraic*
proofs that \( cat_i = cat_j \) by exploiting various mathematical
properties of the definitions of two lists.
I highly doubt that it would be able to produce a *combinatorial* proof that
two descriptions of the Catalan numbers are the same, though I’d be very
happy to be proven wrong.