Hi Manual, thanks for your efforts, but I believe there is already a more efficient way to compute log2.
In your implementation, consider your intlog2_aux which roughly requires y iterations if log2(x) = y, since you always just add 1 to the accumulator. For some of my applications this implementation is not efficient enough, which was the reason to develop Sqrt_Babylonian/Log_Impl.thy, which is much faster since it only needs log2(y) iterations: in log_main the accumulator is roughly doubled in every iteration. To test, try to compute "log_2 (3 ^ n)” for some reasonably large n. Cheers, René PS: Unfortunately, Sqrt_Babylonian.log_floor and log_ceiling are not connected to Discrete.log. > Am 29.06.2017 um 15:29 schrieb Manuel Eberl <ebe...@in.tum.de>: > > Hallo, > > I'm considering adding efficient code for Discrete.log (the dual logarithm on > natural numbers). PolyML does provide an IntInf.log2 function that seems > reasonably efficient so that one can set up code printing. However, I am > struggling with one detail: > > Where would the code that does this actually reside? I cannot really put it > into Discrete.thy, because then that would have to import > Code_Target_Numeral. I could put it into Code_Target_Integer.thy, but then > that would have to import Discrete, which does not sound right to me either. > > I attached what I have so far. > > Manuel > > <Efficient_Log2.thy>_______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
