Re: [isabelle-dev] Efficient code for Discrete.log

[Manuel Eberl]

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 :
>>
>> 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
>>
>> ___
>> 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

Re: [isabelle-dev] Efficient code for Discrete.log

[Thiemann, Rene]

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 :
> 
> 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
> 
> ___
> 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

Re: [isabelle-dev] Efficient code for Discrete.log

[Andreas Lochbihler]

Hi Manuel,

You are not the first to encouter this problem. Here's my experience:

In 4b1b85f38944, I added code_printings for gcd and decided to add Gcd to the imports of 
Code_Target_Nat. IIRC this broke a few things in the AFP, which I had to fix. Meanwhile, 
Gcd has become part of Main again.


Conversely, the AFP entry Native_Word sets up serialisation for bit operations, and there 
is a specific Code_Target_Bits_Int theory with the relevant adaptations for bit operations 
on integers.


I'd suggest that you setup two theories Code_Target_Complex_Int and 
Code_Target_Complex_Nat that will collect all the code declarations for constants that are 
defined in Complex. I think this is the cleanest approach, even though in the long run, we 
might have a huge number of these specific adaptation theories. Your efficient algorithm 
can go directly into Discrete.thy.


Best,
Andreas



On 29/06/17 15:29, Manuel Eberl wrote:

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



___
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