Hi John/Ramana,
John Harrison wrote:
> I shouldn't have tempted fate by mentioning you! But I'm not yet
> completely convinced. It's true that it would create a type operator
> with recorded arity 0, but (at least in the HOL Light implementation)
> it would still end up applied to the sorted list of type variables
> ("tyvars") as if it had arity 2^31. That's not to say this is an ideal
> situation, but it seems to fall into the "anomalous" cetegory rather
> than the actually inconsistent. Or am I missing something?
Ah yes, you're absolutely right - the theorem still has the correct arity
and so this is not a route to unsoundness. Phew!
But I still get a fundamental sense of unease that types can be constructed
that are not well-formed (i.e. where the arities are wrong), so I'll adapt
HOL Zero to stop this.
John Harrison wrote:
> Mark wrote:
>> I always thought that this would be impossible to exploit in practice,
>> but now I'm thinking 2^31 =~ 2 billion, and this is perhaps doable ...
>
> Well, I hope that's impossible for pragmatic reasons: wraparound on
> 2^31 would only happen on a 32-bit platform, and then I don't think
> you could address enough memory directly to put this to the test since
> pointers are also 32-bit. And on a 64-bit machine the bar becomes
> much higher because integers won't wrap till 2^63. But perhaps there
> is some weird way of setting up OCaml where pointers are 64-bit but
> type int is 32-bit?
Yes, you're right again. 64-bit machines will have 63-bit integers unless
using special tricks, and 32-bit machines won't be able to address enough
RAM unless using special tricks. So looks like it couldn't be a problem in
practice. (note that my bounty qualification criteria aim to ban what I
mean by "special tricks")
Ramana Kumar wrote:
> And what about switching to big integers? (for HOL Zero and/or HOL Light)
> I thought HOL Zero might be switching to SML at some point anyway?
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. And yes, I
will be switching to SML, but this is several months away, and in any case,
I want everything to be as watertight as possible in the OCaml
implementation.
Mark.
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
