[isabelle-dev] Integers in Poly/ML
nipkow at in.tum.de
Wed Nov 2 15:37:03 CET 2016
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.
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev