On Mon, 26 Aug 2013, Michael Norrish wrote:
Anyway, being able to lie about a string's size for the benefit of the Oppen algorithm is definitely more important.
Or telling the true size of the string ...
It is up to David Matthews to comment on that, to say if he wants to add it to Poly/ML. If not, I can show how it is done in user-space, but it needs some digging into the Isabelle/ML sources.
Anyway, here are some more hints about "tree size optimization", or rather the irrelevance of it according to the following isabelle-dev thread from 31-Jul-2013: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-Ju...
The main extract is this:
Making a few performance tests recently revealed that fully immutable theory values merely increase the stamp size by a factor of 5, leading to approx. 100000 in main HOL and 300000 in JinjaThreads, with hardly any measurable impact of performance. It leads to approx. 20 table lookups in every kernel inference, just as in ancient times.
So this issue is now on the historic list of "premature optimizations that complicate code", namely that of the kernel. Even just practically, the "stale theory error" has probably wasted more time of tool developers that it saved CPU time.
It other words, the Isabelle inference kernel carries around large immutable tables of "stamps" at the order of 10^5, checks them in every single inference, and updates them in every elementary definition or declaration of theory content. Poly/ML 5.5.0 is able to digest that without problems, and hardly measurable performance impact compared to the "optimized" version that would re-use old stamp collections (basically a linear type implemented manually).
One motivation to get rid of this premature optimization was to make it easier for other prover guys to imitate the explicit theory context of Isabelle: it is very relevant for robustness and performance of the kernel. A bit like a hardware management unit to implement virtual memory, something you take for granted in mainstream computing, while most theorem provers still poke around physically in the context.
Makarius