Thanks for the hint! I'll try to use that then. However, the main goal was to use PolyML's native log2 function anyway, which is likely much faster than anything we can implement in Isabelle.
Manuel On 2017-06-29 20:12, Thiemann, Rene wrote: > 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