[isabelle-dev] Products over lists – naming convention for big sums and products.

[Florian Haftmann]

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-dev at in.tum.de 
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140927/5b1487c6/attachment.sig>