[isabelle-dev] Integers in Poly/ML

[Tobias Nipkow]

I value the guarantees we get from having proper integers a lot. No worries.

With bounded integers, we would have to worry about what happens to 
over/underflow exceptions: can handlers for such exceptions in a piece of user 
code lead to unsoundness in the inference system? At first it seems that if such 
an exception propagates out of the kernel, no incorrect theorems can arise 
(because control has left the kernel). However, in the presence of higher-order 
functions (e.g. user functions can be passed to kernel code) this is not so 
clear to me.

Tobias

On 02/11/2016 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.
>
> Larry
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- 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/cccdbc56/attachment.bin>