Re: [isabelle-dev] Efficient code for Discrete.log
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] [isabelle] Good name for "sublist" predicates
Hi Manuel, Well, how about changing Sublist.subseq to Sublist.subsequence? And accordingly strict_subseq to strict_subsequence or ssubsequence? Andreas On 28/06/17 19:49, Manuel Eberl wrote: Yes, I noticed that as well. I decided to leave it that way since, well, we do have qualified names. If anybody has better suggestions, I am open to implementing them. Manuel On 2017-06-28 17:05, Andreas Lochbihler wrote: Dear all, While porting some of my theories to the current development version, I've just noticed that the renaming of sublisteq to subseq done by Manuel in May (639eb3617a86) has one bad effect: The name subseq is already used in Topological_Spaces to formalise the concept of a subsequence. This name is now hidden by the definition in Sublist, in particular when I import HOL-Probability. Can this name clash be eliminated before the next release such that I don't have to write Topological_Spaces.subseq everywhere? Thanks, Andreas On 26/05/17 08:16, Tobias Nipkow wrote: Thank you for your research. I am perfectly happy with "sublist" (for the contiguous case) and "subseq" (for the general case) and think we should adopt it. [Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒ nat set ⇒ 'a list" (in List) to something else, eg sublist_index) Tobias On 25/05/2017 21:13, Jasmin Blanchette wrote: On 25.05.2017, at 20:41, Tobias Nipkow wrote: I don't think that sublist, subsequence and substring really have much of a bias in either direction, except possibly substring, but the latter does indeed sound too specialized. Wikipedia has a clear bias (and I did not edit it, nor did I look it up before writing my previous email): https://en.wikipedia.org/wiki/Subsequence https://en.wikipedia.org/wiki/Substring Popular algorithm sbooks like Cormen et al. follow the same definition of subsequence. Standard expressions like "longest increasing subsequence" depend on this semantics. As for sublist, all the examples I see by Googling either "sublist", "is_sublist", "isSublist", or "indexOfSubList" in Java, Python, Scala, etc., have the contiguous semantics. Including this page: http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html I'm not saying we should rename the Isabelle concepts, just that Isabelle is the odd (wo)man out. Jasmin ___ 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 mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Efficient code for Discrete.log
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
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
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
