[isabelle-dev] Integers in Poly/ML

[Makarius]

On 02/11/16 13:07, Lawrence Paulson wrote:
> David Matthews is working on a new release of Poly/ML in which the default type of integers is fixed-precision. A configuration option can restore the former set up, but that might be a mistake: I modified MetiTarski to use large integers only where needed and saw runtime decrease by around 30%. We could do the same. I imagine that we need large integers almost nowhere. Now consider that every bound variable is represented internally by an integer.

I am surprised that MetiTarski shows such a relatively big speedup. Does
it really happen in a sustained manner for typical uses, and not just in
isolated cases?

My guess for Isabelle is between 0.1-5%, but it needs to be proven by
concrete measurements. Changing type int to be a fixed-width machine
word (and thus no int at all), will not work without significant work on
the sources. Already about 10 years ago, we switched in the opposite
direction, to make type int a proper integer even for SML/ML. That was a
great improvement for tool development, and a slowdown for SML/NJ of
20-40% -- its IntInf implementation is very poor.


Anyway, I have always been in close contact with David Matthews
concerning various performance improvements. The present idea is to
introduce a new type (e.g. called "index") that is a short machine word
and used for the de-Bruijn index in a term and also for indexname.

Further experimentation will be needed to see how far such a symbolic
index can be pushed elsewhere. E.g. type "serial" is another candidate,
but FixedInt has only 31 bits on our standard platform, and overflows at
approx. 10E9. This limits the total livetime of an Isabelle process,
notably an interactive one or a dumped image.

Switching to 64bit by default would avoid this, but it costs 20-30%
overall performance penalty, and requires a reasonably big machine (16
GB or better 32 GB). I am still trying to avoid the discontinuity
towards 64bit -- after the release I will look again how to reduce
overall resource requirements -- just another round of Tetris.


	Makarius