Email Gateway (Aug 22 2022 at 12:27): Email Gateway (Aug 22 2022 at 12:27):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I just noticed that the "power" function is exported as
power :: forall a. (Power a) => a -> Nat -> a;
power a n =
(if equal_nat n zero_nat then one
else times a (power a (minus_nat n one_nat)));
This looks pretty inefficient to me; something like iterated squaring
should be much faster, and it's pretty easy to do. However, this only
works in the type class mult_monoid; power, on the other hand, is
defined in the type class "power". (the difference is essentially that
the latter does not demand associativity, if I am not mistaken)
Is it still possible to use the more efficient iterative squaring when
applicable? I attached something using code_unfold, but I'm not sure if
that really does what one would want it to do.
Moreover, for rational numbers, one could optimise this even futher:
multiplication on rational numbers reduces the numerator and denominator
after the multiplication. In the case of "power", this is unnecessary,
since the numerator and denominator of the result will always be coprime
if they were coprime before. Perhaps this would be a worthwhile
optimisation?
Lastly, I was wondering whether there was something like "divmod" in
Isabelle, i.e. an operation that returns both the quotient and the
remainder, since most languages have a corresponding operation that is
more efficient than computing the two separately.
Cheers,
Manuel
MyPower.thy
Email Gateway (Aug 22 2022 at 12:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Manuel,
I just noticed that the "power" function is exported as
power :: forall a. (Power a) => a -> Nat -> a;
power a n =
(if equal_nat n zero_nat then one
else times a (power a (minus_nat n one_nat)));This looks pretty inefficient to me; something like iterated squaring should be much
faster, and it's pretty easy to do. However, this only works in the type class
mult_monoid; power, on the other hand, is defined in the type class "power". (the
difference is essentially that the latter does not demand associativity, if I am not
mistaken)
mult_monoid assumes associativity of and neutrality of 1 for times. power does not impose
any constraints; it is a superclass of mult_monoid.
Is it still possible to use the more efficient iterative squaring when applicable? I
attached something using code_unfold, but I'm not sure if that really does what one would
want it to do.
The code_unfold works if the call to power in the code equations is types with something
of sort mult_monoid. So if the code equation uses power on one of the standard numeric
types, everything is fine. But if you use power polymorphically for some 'a, then this
does not work if mult_monoid is not a supersort of 'a's sort. For example, if you have
something like
definition map_power :: "'a :: power list => 'a list"
where "map_power = map power"
then if you use map_power, you will end up with the original slow implementation.
Moreover, for rational numbers, one could optimise this even futher: multiplication on
rational numbers reduces the numerator and denominator after the multiplication. In the
case of "power", this is unnecessary, since the numerator and denominator of the result
will always be coprime if they were coprime before. Perhaps this would be a worthwhile
optimisation?
Custom implementations for power are not possible with the current setup. You can have
type-dependent implementations for a function only if that function is a type class
parameter (unless you play some sophisticated tricks like in the Containers AFP entry).
From what I can see, it does not seem reasonable to make power a type class parameter,
because then power cannot be a superclass of mult_monoid any more (you'd have to add power
as a type class parameter to the whole algebraic type class hierarchy). But you could
achieve something similar like this:
class power_impl = power +
fixes power_impl :: "'a => nat => 'a"
assumes power_impl: "power = power_impl"
declare power_impl [code]
Then, of course, you have to instantiate the new class power_impl for all types that
instantiate power and all users have to do the same for their own types. Unfortunately, we
do not (yet) have a mechanism to instantiate such definitional type classes automatically.
With this approach, you could declare custom code equations for instances like rat.
Lastly, I was wondering whether there was something like "divmod" in Isabelle, i.e. an
operation that returns both the quotient and the remainder, since most languages have a
corresponding operation that is more efficient than computing the two separately.
There are various specialised divmod constants in HOL, e.g., divmod_integer,
semiring_numeral_div_class.divmod and Divides.divmod_nat, but no systematic, algebraic
treatment.
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:28):From: Manuel Eberl <eberlm@in.tum.de>
I guess that's a pretty good compromise, isn't it? Most of the time,
exported code using the "power" operation will probably be dealing with
types that fulfil at least monoid_mult, and then this fast variant could
be used.
Perhaps this should be put in the library?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 12:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
I think that this can work for power, but it can also lead to surprises because the
rewrite does not trigger always and users then have to understand the whole setup to find
out. I had experimented with such rewrites for subset tests (end of theory
Library/Cardinality), but this never worked as well as I had hoped, because the rewrite
needed the sort card_UNIV, which was hardly present in any code equation.
René Thiemann and Christian Sternagel faced the same problem for linorders and
comparators. They have implemented a custom function in ML that transforms the code
equations, but users have to call this manually (see their ITP2015 paper). This approach
is less convenient, but more robust.
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:29):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Manuel,
If you care about efficiency, you might also have a look at improved code equations for divmod, e.g., under
http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Improved_Code_Equations.html
for Isabelle 2015
and under
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Divmod_Int.html
for Isabelle 2016-RC0.
Best,
René
Last updated: Apr 19 2024 at 04:17 UTC