Re: [isabelle] Efficient Integers?

You can do anything you want, at your own risk, if you modify what the
code generator turns a certain type into. See the code generation
documentation and see what Code_Integer does.


Am 11/02/2012 20:06, schrieb Filip Maric:
> Hello,
> 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,
> Filip
> 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.