*To*: Isabelle-Users Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Combinatorial functions*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Mon, 4 Jul 2016 21:17:53 +0200*Organization*: TU Munich*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

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**

- Previous by Date: [isabelle] Mean value theorem for has_vector_derivative
- Next by Date: [isabelle] new AFP entry: DFS_Framework
- Previous by Thread: Re: [isabelle] Mean value theorem for has_vector_derivative
- Next by Thread: [isabelle] new AFP entry: DFS_Framework
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list