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

[isabelle-dev] Efficient code for Discrete.log

[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

theory Efficient_Log2
imports
  Main
  "~~/src/HOL/Library/Discrete" 
  "~~/src/HOL/Library/Code_Target_Numeral"
begin

context
includes integer.lifting
begin

qualified lift_definition intlog2 :: "integer \ integer" is
  "\n. int (Discrete.log (nat n))" .

qualified function intlog2_aux :: "integer \ integer \ 
integer" where
  "intlog2_aux n acc = (if n < 2 then acc else intlog2_aux (n div 2) (acc + 1))"
  by auto
termination proof (relation "measure (nat_of_integer \ fst)")
  fix n acc :: integer
  assume "\n < 2"
  hence "nat_of_integer (n div 2) < nat_of_integer n"
by transfer auto
  thus "((n div 2, acc + 1), (n, acc)) \ measure (nat_of_integer \ 
fst)" 
by simp
qed simp_all

declare intlog2_aux.simps [simp del]
  
qualified lemma intlog2_aux_correct: "acc \ 0 \ intlog2_aux 
n acc = intlog2 n + acc"
proof (induction n acc arbitrary: acc rule: intlog2_aux.induct)
  case (1 n acc)
  show ?case
  proof (cases "n < 2")
case True
hence "intlog2 n = 0" by transfer (simp add: Discrete.log.simps)
with True show ?thesis by (subst intlog2_aux.simps) auto
  next
case False
hence "intlog2 n = intlog2 (n div 2) + 1"
proof (transfer, goal_cases)
  case (1 m)
  hence "int (Discrete.log (nat m)) = int (Discrete.log (nat m div 2)) + 1"
by (subst Discrete.log.simps) auto
  also have "nat m div 2 = nat (m div 2)" by simp
  finally show ?case .
qed
with False show ?thesis by (subst intlog2_aux.simps) (auto simp: 1)
  qed
qed
  
qualified lemma intlog2_code [code]: "intlog2 n = intlog2_aux n 0"
  by (simp add: intlog2_aux_correct)

lemma Discrete_log_code [code abstract]:
  "integer_of_nat (Discrete.log n) = (if n = 0 then 0 else intlog2 (of_nat n))"
  by transfer simp

end

code_printing
  constant "Efficient_Log2.intlog2 :: integer \ _" 
\ 
(SML) "IntInf.log2" and
(Eval) "IntInf.log2"

value [code] "Discrete.log 12345"

export_code Discrete.log checking SML Eval Scala Haskell? OCaml?

end___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev