Hi :) I am trying to use the Akra_Bazzi theory to show asymptotic runtime statements. Most of the times, the proofs succeed automatically. However, for one specific function the
master_theorem tactic fails.
My function is of the following form:
theory Scratch imports "Akra_Bazzi.Akra_Bazzi" "Akra_Bazzi.Akra_Bazzi_Method" begin function f :: "nat ⇒ real" where "n ≤ 4 ⟹ f n = 100" | "n > 4 ⟹ f n = n * 2 ^ n + 2 ^ (nat (floor (real n / 2))) * f (nat (floor (real n / 2)))" by fastforce+ termination by akra_bazzi_termination simp_all
The application of the master theorem for the runtime bound fails:
lemma "f ∈ O(λn. (n * 2 ^ n) * ln n)" apply (master_theorem 2.3)
Is there some specific format in which I have to write the lemma so that
master_theorem succeeds? I read the summary, but didn't find more information.
Also, as a side question: initially I defined the function as
function g :: "nat ⇒ nat" where "n ≤ 4 ⟹ g n = 100" | "n > 4 ⟹ g n = n * 2 ^ n + 2 ^ (n div 2) * g (n div 2)" by fastforce+
With this definition,
akra_bazzi_termination canot be applied in the termination proof, whereas
termination by (relation "Wellfounded.measure (λn. n)") simp_all
does the trick. With this definition,
master_theorem 2.3 throws the following exception when applied to the runtime statement:
exception TERM raised (line 541 of "$AFP/Akra_Bazzi/akra_bazzi.ML"): Could not obtain function info record. λx. real (g x)
so I guess Akra_Bazzi is only for real-valued functions?
Thanks in advance!
Hey, sorry for the very late answer. I've been a bit busy. I doubt anyone in the community other than me really knows very much (or anything) about this stuff since I was the one who wrote it and it is very special-purpose. In fact it amazes me that there are people who are actually getting this to work at all without asking me for help, since it's not very polished.
It's been many years since I wrote that code and I haven't used it very much myself since, but I'll look into it and try to answer your questions. But just so you know, the proof methods don't actually do that much work themselves. If they don't work for you, you can always apply the ‘Master Theorems’ they are based on yourself by hand.
Ah, the answer is pretty simple: the Master Theorem I proved can only handle polynomials.
The Akra--Bazzi Theorem I formalised is more flexible than that, so you might be able to get what you need from that.
In your case a direct proof of the bound might be easier. It's hard to tell.
Actually there are more problems here. First of all, I don't think your term satisfies the growth condition imposed by the Akra--Bazzi Theorem. But more crucially, your term is not allowed by the Akra--Bazzi Theorem.
For the Akra--Bazzi Theorem, you can have a weighted sum of ‘recursive calls’ to
f with weights attached to them, but the weights must not depend on
n. In your case, the sum only has one element but the weight is .
If you want to attack this directly one approach would be to make a change of variables , which turns it into a linear recurrence that should be solvable with standard techniques. That will give you a closed-form expression for . Using the monotonicity of you should then be able to nail down the growth of on its full domain well enough.
If I haven't made a typo, Mathematica claims that (assuming that the recurrence holds for all instead of like in your case, but obviously that doesn't change much).
The correctness of that solution should be verifiable easily by induction.
Due to this extreme growth you probably won't be able to get a bound for out of this, but you will at least get some lower/upper bound.
Thank you very much for the detailed answer! In the meantime, I derived an explicit bound manually - but I will try your ideas at a later point and see if I can simplify the proof.
Last updated: Dec 07 2023 at 20:16 UTC