Email Gateway (Aug 22 2022 at 15:50): Email Gateway (Aug 22 2022 at 15:50):From: Peter Gammie <peteg42@gmail.com>
Dear BNF experts,
The size function for fmap in HOL/Library/Finite_Map in Isabelle2016-1 seems sub-optimal: it appears to ignore the sizes of the things in the map.
I tried implementing this using the approach taken in FSet and Multiset, but the fmap constructor is binary and I’m not sure what shape the theorems should be (specifically the final one that composes size functions somehow).
Thanks!
cheers,
peter
Email Gateway (Aug 22 2022 at 15:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Pete,
You need a function size_fmap that takes a size function for every type argument, even the
dead ones. So it should have the type
('a => nat) => ('b => nat) => ('a, 'b) fmap => nat
Typically, the instantiation for the type class then puts "%_. 0" for the arguments.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 15:50):From: Lars Hupel <hupel@in.tum.de>
This is an oversight – I'll try to add this to the theory over the next
couple of days.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:50):From: Peter Gammie <peteg42@gmail.com>
Great, thanks!
cheers,
peter
Email Gateway (Aug 22 2022 at 15:51):From: Lars Hupel <hupel@in.tum.de>
This is an oversight – I'll try to add this to the theory over the next
couple of days.
See now <http://isabelle.in.tum.de/repos/isabelle/rev/4d2ce596f505>.
Peter, please try it out and tell me if it works for you.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:51):From: Peter Gammie <peteg42@gmail.com>
Lars, Andreas:
Thanks Lars. I backported it to Isabelle2016-1 and indeed my termination proof now goes through.
Another question for you and Andreas: what is the substantive difference in intent between Finite_Map and FinFun? I used Finite_Map as I needed the BNF setup, but I reached for FinFun first as I knew it was there. In the fullness of time, could they perhaps be merged?
And another, but perhaps more directly for the BNF people: I’ve been tripped up on products uniformly having a constant size a few times now. Here’s a quick theorem search:
Basic_BNF_LFPs.prod.size(2): size (?x1.0, ?x2.0) = Suc 0
Could it too be made more useful by returning the sum of the sizes of its arguments?
(These arose in termination arguments, and the fun package seems to avoid using size on products. I wonder if such a change would impact it.)
cheers,
peter
Email Gateway (Aug 22 2022 at 15:51):From: Lars Hupel <hupel@in.tum.de>
Another question for you and Andreas: what is the substantive difference in intent between Finite_Map and FinFun? I used Finite_Map as I needed the BNF setup, but I reached for FinFun first as I knew it was there. In the fullness of time, could they perhaps be merged?
Here's a mailing list thread on that issue:
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-September/msg00015.html>.
And another, but perhaps more directly for the BNF people: I’ve been tripped up on products uniformly having a constant size a few times now. Here’s a quick theorem search:
Basic_BNF_LFPs.prod.size(2): size (?x1.0, ?x2.0) = Suc 0
Could it too be made more useful by returning the sum of the sizes of its arguments?
There is such a function: "size_prod". However, you have to tell the
function package about it.
(These arose in termination arguments, and the fun package seems to avoid using size on products. I wonder if such a change would impact it.)
Here's a contrived example:
fun contrived :: "('a list × 'a list) ⇒ ('a list × 'a list)" where
"contrived (xs, y1 # y2 # ys) = contrived (y1 # xs, ys)" |
"contrived (x1 # x2 # xs, ys) = contrived (xs, x1 # ys)" |
"contrived _ = ([], [])"
By default, the function package won't be able to derive a termination
measure for this. But you can add the following before the definition:
lemma [measure_function]: "is_measure (size_prod size size)"
by (rule is_measure.intros)
There's probably a good reason why this doesn't happen by default.
(Possibly time complexity of the termination prover.) If this thing
keeps happening to you (or you need nesting), try this:
lemma [measure_function]: "is_measure f ⟹ is_measure g ⟹ is_measure
(size_prod f g)"
by (rule is_measure.intros)
This might mess up things elsewhere though, so try it at your own risk.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:51):From: Peter Gammie <peteg42@gmail.com>
Lars,
Thanks for the pointers. I don’t recall seeing the stuff you mentioned about [measure_function] being mentioned in the functions manual; perhaps it could be added?
cheers,
peter
Email Gateway (Aug 22 2022 at 15:51):From: Lars Hupel <hupel@in.tum.de>
Thanks for the pointers. I don’t recall seeing the stuff you mentioned about [measure_function] being mentioned in the
functionsmanual; perhaps it could be added?
Possibly. Though I'll have to defer to someone who actually understands
the implications of declaring [measure_functions], in particular the
parametrized variants.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:52):From: Tobias Nipkow <nipkow@in.tum.de>
I learned about
lemma [measure_function]: "is_measure f ⟹ is_measure g ⟹ is_measure (size_prod f g)"
by (rule is_measure.intros)
from Peter Lammich who probably uses it more often. He may have some insight as
to the dangers of using this by default.
Not that the recursive function need not be tupled for this to help because
internally the arguments are tupled anyway.
It would indeed be nice if this were mention in the "function manual". In case
somebody feel sufficiently au fait with this feature ...
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 15:52):From: Peter Lammich <lammich@in.tum.de>
On Di, 2017-08-15 at 12:14 +0200, Tobias Nipkow wrote:
I learned about
lemma [measure_function]: "is_measure f ⟹ is_measure g ⟹ is_measure
(size_prod f g)"
by (rule is_measure.intros)from Peter Lammich who probably uses it more often. He may have some
insight as
to the dangers of using this by default.
I have not used this very often, too. Only for small isolated examples,
but not in the basis of some big developments.
Nevertheless, I would be curious what would happen if one adds this
lemma by default (e.g. to Main)
Email Gateway (Aug 22 2022 at 15:57):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter and Peter,
The termination proof methods (lexicographic_order and size_change) use the
[measure_function] theorems to generate all candidate functions in a Prolog style. If this
rule for size_prod is added globally, then these methods will try many more candidates for
functions which use pairs. In detail, every tuple argument gets two changes, namely with
"size" and with "size_prod ... ...". In case of nested tuples, this lead to quadratically
many candidates. Accordingly, the matrix output by a failing lexicographic order may
become harder to read because there are more columns and more failed goals.
My feeling would be that it would not make a big difference for most function definitions,
but some could experience a significant slow-down. AFAIK, the size plugin of the datatype
package does not generate these [measure_function] theorems for the size_F functions,
either, probably for the same reason.
Andreas
Last updated: Apr 23 2024 at 16:19 UTC