Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
On 25.09.2014 18:32, Tobias Nipkow wrote: Florian: But you agree that it should be uniformaly Sum or sum for all summation operators? Johannes already remarked on the discrepancy in your proposal. That would be »Sum_list« and »Prod_list«. The idea of having »sum« and »prod« was inspired by plain functional programming. But uniformity seems indeed more important here than succinctness at any cost. Florian Tobias On 25/09/2014 16:32, Florian Haftmann wrote: a) for lists: sum_list (← listsum), prod_list (← listprod) b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) c) for finite sets: Sum (← setsum), Prod (← setprod) I assume a) means Sum_list and Prod_list?! Why Sum and not Sum_set in c)? Is the intention that the canonical type always gets the short name? Like map instead of map_list. Indeed. And why upper case Sum instead of sum? I am less sure about that. Usually the capitalized versions are the Big operators, but sum is already big (the binary version is called plus) and sum_list is also a big operator. Unless we have a clear and simple policy, all lowercase would be better. The captialization is derived from existing Inf, Sup, Union, Inter (vs. inf, sup, union, inter). For binary operations like +, -, *, / there is a preference to prefer the name of the operation (plus, mult) over the algebraic concept (sum, product). But these are exceptions. PS: Maybe c) could be tackled in the future when we have a hypothetical constant/lemma renaming tool. The issue is the renaming of lemmas, which is not so straighforward. Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
a) for lists: sum_list (← listsum), prod_list (← listprod) b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) c) for finite sets: Sum (← setsum), Prod (← setprod) I assume a) means Sum_list and Prod_list?! Why Sum and not Sum_set in c)? Is the intention that the canonical type always gets the short name? Like map instead of map_list. Indeed. And why upper case Sum instead of sum? I am less sure about that. Usually the capitalized versions are the Big operators, but sum is already big (the binary version is called plus) and sum_list is also a big operator. Unless we have a clear and simple policy, all lowercase would be better. The captialization is derived from existing Inf, Sup, Union, Inter (vs. inf, sup, union, inter). For binary operations like +, -, *, / there is a preference to prefer the name of the operation (plus, mult) over the algebraic concept (sum, product). But these are exceptions. PS: Maybe c) could be tackled in the future when we have a hypothetical constant/lemma renaming tool. The issue is the renaming of lemmas, which is not so straighforward. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
Am Donnerstag, den 18.09.2014, 15:47 +0200 schrieb Florian Haftmann: Changeset #fe083c681ed8 introduces products over lists. There has been some private discussion whether there could be a serious attempt to establish a new consistent naming scheme for summation and products over collections. a) for lists: sum_list (← listsum), prod_list (← listprod) b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) c) for finite sets: Sum (← setsum), Prod (← setprod) I assume a) means Sum_list and Prod_list?! Why Sum and not Sum_set in c)? Is the intention that the canonical type always gets the short name? Like map instead of map_list. And why upper case Sum instead of sum? - Johannes PS: Maybe c) could be tackled in the future when we have a hypothetical constant/lemma renaming tool. As far as can be forseen, 58 theories would be affected by a switch as suggested by a). b) is no big issue. c) is maybe beyond what should be reasonably attempted (218 affected theories). Suggestions welcome. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
One could argue that sets are the canonical indexing structure. On the other hand, we have syntax to make the actual names irrelevant. Larry On 24 Sep 2014, at 11:18, Johannes Hölzl hoe...@in.tum.de wrote: Why Sum and not Sum_set in c)? Is the intention that the canonical type always gets the short name? Like map instead of map_list. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
On 18/09/2014 15:47, Florian Haftmann wrote: Changeset #fe083c681ed8 introduces products over lists. There has been some private discussion whether there could be a serious attempt to establish a new consistent naming scheme for summation and products over collections. a) for lists: sum_list (← listsum), prod_list (← listprod) b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) c) for finite sets: Sum (← setsum), Prod (← setprod) Looking again at the result of our discussion I still like it. Tobias As far as can be forseen, 58 theories would be affected by a switch as suggested by a). b) is no big issue. c) is maybe beyond what should be reasonably attempted (218 affected theories). Suggestions welcome. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
A gain in legibility for sure. Larry On 18 Sep 2014, at 15:11, Tobias Nipkow nip...@in.tum.de wrote: On 18/09/2014 15:47, Florian Haftmann wrote: Changeset #fe083c681ed8 introduces products over lists. There has been some private discussion whether there could be a serious attempt to establish a new consistent naming scheme for summation and products over collections. a) for lists: sum_list (← listsum), prod_list (← listprod) b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) c) for finite sets: Sum (← setsum), Prod (← setprod) Looking again at the result of our discussion I still like it. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
