Re: [isabelle] size entry-point in signature TABLE

On 5 May 2015, at 22:09, Makarius <makarius at> wrote:
> On Tue, 5 May 2015, Michael Norrish wrote:
>> Is there any chance the signature TABLE (from src/Pure/General/table.ML) could be extended to support a constant time
>> size : 'a table -> int
>> operation?  At the moment, it seems as if I have to calculate this âby handâ (perhaps with fold), and with O(n) complexity.
> The reasons for not storing local sizes in the data structure for constant size operations are the same as for lists: extra redundancy that needs to be maintained at run-time and requires more space in memory.
> Our Table implementation is almost as fundamental as List.  It is at the bottom of large-scale data management.  Any change down there will impact almost everything, and many people will have to get 32 GB machines at last.

I appreciate the desire not to meddle with something fundamental, but I donât think the concern about wasted space is justified.  Assuming an extra int is going to take 8 bytes to store, in order to waste even 1MB (which is in turn just 1/16000th of a 16GB machine), youâd have to have 125000 live tables in memory.  Tables can get big (motivating the desire to avoid O(n) operations), but Iâd be surprised if a running Isabelle really had that many tables around.

Thanks for the pointers to the extended table examples.



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.