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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to