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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Sep 25 16:32:15 CEST 2014


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

-------------- 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/20140925/33b60805/attachment.sig>


More information about the isabelle-dev mailing list