[isabelle-dev] Integers in Poly/ML

[Lawrence Paulson]

I have to say, I’m absolutely mystified by the response to my suggestion.

MetiTarski, which during execution relies heavily on large integers, nevertheless benefits to the tune of 30% to having all other integers fixed-precision. During its execution, Isabelle makes very heavy use of small integers, in the representation of bound variables and flexible variables, which are renamed by having an offset before each and every resolution step.

We have spent a lot of time discussing problems caused by the cost of regression testing, and now we have the possibility of reducing that by 30%.

As to changes in behaviour that could be caused by overflows, I checked: exception Overflow is explicitly caught in only two places throughout the sources, both in HOL decision procedures (and therefore well outside the kernel) while the wildcard exception is caught in three places in Pure. No exception handlers had to be added when I converted MetiTarski to use fixed integers. An uncaught exception doesn’t prove anything, of course.

Larry

> On 2 Nov 2016, at 14:43, Makarius <makarius at sketis.net> wrote:
> 
> On 02/11/16 15:30, Lawrence Paulson wrote:
>> 
>> I actually can’t think of many places where Isabelle would need large
>> integers, so it would probably benefit even more than MetiTarski does.
> 
> "Can't think of" merely indicates a lack of empirical tests, against the
> Isabelle repository and AFP. Afterwards the situation usually looks
> quite different, and the initial hypothesis needs to be changed.
> 
> When we moved to proper int by default some years ago, there were
> several tool implementors approaching me, asking to be delivered from
> the curse of many different "int" types.
> 
> We also have conceptual reasons to stay true to the concept of an
> integer that is an integer, a string that is a string etc. -- and thus
> not using a machine word instead of an integer, or a "char" type that
> cannot hold a textual character (not even in Unicode). Isabelle/ML is
> meant to be a programming environment free from bad jokes like that.
> 
> 
> Nonetheless, I do think that proper use of machine words in isolated
> situations can help, but they should not be called "int" and used by
> default.
> 
> 
> 	Makarius
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161102/38184b2d/attachment-0002.html>