Re: [isabelle] Efficient Integers?


although it is generally unsound, is there still a simple way to get machine integers?

I have an application that uses only positive integers between 0 and 2^12 and the only operation performed on these numbers is bitwise disjunction (which leaves them in this range). In the logic, I used the nat type and define the bit-or using div/mod, but, of course, this is very slow when executed (proof checking takes almost half an hour since there is a lot computation involved). Since the range is bounded, there is a "meta-theoretic" argument that machine integers would not introduce unsoundness, so I wonder if it is possible to "cheat" and use them and instruct the code generator to call the target-language bit-or in place of my div/mod defined bit-or (I tried something like code_const "bitor" (SML "IntInf.orb ((_), (_))") (Haskell infixl 6 "(.|.)"), but it did not give expected efficiency since big integers are used). Evaluations are used within a "proof-by-evaluation" paradigm and I use the method "by eval".

I suppose the other option would be not to use nats but machine words in the logic level, but then the formalization would be a bit more complicated, and I not sure what theory I should start from (I assume there is such a formalization in the Library)?

Thank you very much,

On Fri, 10 Feb 2012, Tobias Nipkow wrote:

PS No, you don't get machine integers, that would be unsound. You get
big integers, which are language specific. I assume that in most of the
languages we support big integers are like machine integers plus some
fixed overhead, as long as you stay in the machine integer range.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.