# [isabelle] Combinatorial functions

Hi all,

during some recent hobby work involving combinatorial coefficients, I
found that a lot of relevant stuff is already present in Binomial.thy.
But there are also some open questions / improvements here.

* The theory name ÂBinomialÂ is very specific, and from and outside
perspective you would not expect falling factorial etc. residing there.
How could we make this material more prominent? An extension / appendix
to ÂWhat's in MainÂ?

* There is the tendency to generalize combinatorial functions from
natural numbers to suitable algebraic type classes, as e.g. for âfactâ.
In the case of the falling factorial, this leads to something having a
dedicated name in literature, the pochhammer symbol. However, if I as a
theory writer was just looking for a vanilla falling factorial on the
natural numbers (cf. the AFP entry on discrete summation), I would not
have the idea for looking for ÂpochhammerÂ. Maybe an input abbreviation
would make sense here?

* There are two different binomial coefficients formalized separately,
the nat-based âbinomialâ and the generalized âgbinomialâ. In the long
run there should be only one generalized version.

* In Library/Stirling.thy there is a wonderful algorithm for computing
elements of a (Pascal, Stirling) triangle. Maybe it makes sense to be
generalized and used also here since it would avoid the big products
when computing binomial coefficients via factorials.

* In my eyes the existing infix syntax on binomial coefficients does not
make much sense. Its precedence is the same addition, which means that
precedence in âm choose n * qâ is different from âm choose n + qâ. It
does only meagrely improve readability, since the operation is usually
not nested, there is no kind of associativity (as far as I know), it
uses letters rather than symbols, and Âm choose nÂ is also customary
spelt as Ân over mÂ.

So much to say about that.

Cheers,
Florian

--

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.