Hi Mark, | Yes, big integers is the other possibility. I'm trying to do it as | light weight as possible, and yet keeping the user interface | "conventional" (using the classic types so that integer literals | supplied by the user do not have to be wrapped with 'Int'). However, | the HOL Zero natural number syntax functions already use big integers, | and so there is already an inconsistency in style here, and so maybe I | should follow your suggestion.
I rely quite heavily on the OCaml Num library for various things in HOL Light's arithmetic decision procedures. But I am a bit reluctant to introduce a dependency on this library into the logical kernel. It's pretty big and complicated, and I have found one or two bugs in it in the past (admittedly many years ago). Since the overflow is a bit of a theoretical rather than practical problem, I'm inclined to stick to the devil I know, machine arithmetic, or perhaps just use int64. (As Makarius pointed out, even the unary representation with unit lists has its issues too in OCaml.) But thinking through the implications here together has certainly been valuable, I think. John. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
