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. LarryOn 2 Nov 2016, at 14:43, Makarius <makar...@sketis.net <mailto:makar...@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
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
