Email Gateway (Aug 22 2022 at 13:51): Email Gateway (Aug 22 2022 at 13:51):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Last updated: Apr 27 2024 at 01:05 UTC