Re: [isabelle] Efficient Integers?
although it is generally unsound, is there still a simple way to get
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