[isabelle-dev] Integers in Poly/ML

[Tobias Nipkow]

On 02/11/2016 15:58, Lawrence Paulson wrote:
> I have to say, I’m absolutely mystified by the response to my suggestion.

This is a nontrivial change in the semantics. The programming language community 
has tried to get away from the "looks ok" approach to "here is some sound 
reasoning why it is ok". I could indeed not construct an example where a new 
incorrect result arises because of a caught over/underflow exception (only new 
ways to construct results that could already arise before). But that isn't 
exactly a proof (although the proposition may well be a thm).

Otherwise I agree with Makarius.

Tobias

> 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
>> <mailto: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 --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161102/2d15d7e6/attachment.bin>