Stream: Beginner Questions

Topic: Using Akra_Bazzi

Jakob Schulz (May 19 2023 at 10:43):

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!

Manuel Eberl (Jun 06 2023 at 11:00):

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.

Manuel Eberl (Jun 06 2023 at 11:01):

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.

Manuel Eberl (Jun 06 2023 at 11:39):

Ah, the answer is pretty simple: the Master Theorem I proved can only handle polynomials.

Manuel Eberl (Jun 06 2023 at 11:40):

The Akra--Bazzi Theorem I formalised is more flexible than that, so you might be able to get what you need from that.

Manuel Eberl (Jun 06 2023 at 11:40):

In your case a direct proof of the bound might be easier. It's hard to tell.

Manuel Eberl (Jun 06 2023 at 11:47):

Actually there are more problems here. First of all, I don't think your $n 2^n$ term satisfies the growth condition imposed by the Akra--Bazzi Theorem. But more crucially, your term $2^{n/2} f(n/2)$ 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 $2^{n/2}$.

Manuel Eberl (Jun 06 2023 at 11:56):

If you want to attack this directly one approach would be to make a change of variables $n = 2^k$, which turns it into a linear recurrence that should be solvable with standard techniques. That will give you a closed-form expression for $f(2^k)$. Using the monotonicity of $f$ you should then be able to nail down the growth of $f$ on its full domain well enough.

Manuel Eberl (Jun 06 2023 at 11:59):

If I haven't made a typo, Mathematica claims that $f(2^k) = 2^{2^k+1} (2^k-1) + 2^{2^k-2} f(1)$ (assuming that the recurrence holds for all $n > 1$ instead of $n > 4$ like in your case, but obviously that doesn't change much).

Manuel Eberl (Jun 06 2023 at 11:59):

The correctness of that solution should be verifiable easily by induction.

Manuel Eberl (Jun 06 2023 at 12:02):

Due to this extreme growth you probably won't be able to get a $\Theta$ bound for $f$ out of this, but you will at least get some lower/upper bound.

Jakob Schulz (Jun 07 2023 at 19:07):

Hi Manuel,

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 21 2024 at 16:20 UTC