[isabelle-dev] Products over lists – naming convention for big sums and products.
florian.haftmann at informatik.tu-muenchen.de
Sat Sep 27 09:15:20 CEST 2014
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
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.
> 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.
>>>> 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.
>> _______________________________________________ isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev