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
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
