Comment by dwohnitmok
1 day ago
What I mean is that there is no relationship in Isabelle between their cost function and their actual algorithm.
The process the book goes through for a function f is the following:
1. Define `f`
2. Create a correctness predicate (call it `Correct`) and prove `forall x, Correct(f(x))`
3. Use a script to do some code generation to generate a function `time_f`
4. Prove that `time_f` fulfills some asymptotic bound (e.g. `exists c, forall x, x > c -> time_f(x) < a * x^2`)
Nowhere is `time_f` actually ever formally related to `f`. From Isabelle's point of view they are two completely separate functions that have no relationship to one another. There is only an informal, English argument given that `time_f` corresponds to `f`.
Ideally you'd be able to define some other predicate `AsymptoticallyModelsRuntime` such that `AsymptoticallyModelsRuntime(f, time_f)` holds, with the obvious semantic meaning of that predicate also holding true. But the book doesn't do that. And I don't know how they could. Hence my original question of whether there's any system that lets you write `AsymptoticallyModelsRuntime`.
Yes, I know what you mean, but there is a relationship, it is just that some of that relationship is described outside of Isabelle, but nevertheless provably. Ultimately, math is like that, provably so.
You could do what you want by making that argument explicit formally and machine-checked, but then you have to do a lot more work, by translating all of the components of the informal proof into formal ones. This will not give you any more insight than what the book already describes. But of course you could take it as an example of something that should be easy once you grasp the informal proof, but is actually quite a lot of work.
> You could do what you want by making that argument explicit formally and machine-checked, but then you have to do a lot more work, by translating all of the components of the informal proof into formal ones.
I don't see how you can. This is why I posed my question originally. Let me make the question sharper.
Here's some Isabelle code on the very simple function `double` that just doubles a natural number.
How do I even begin to write the formal argument that `double` has asymptotic runtime complexity that is linear in the size of its argument without resorting to `time_f`-style shenanigans?
I don't know how to even state it in Isabelle. Let alone prove it.
This is a great example! First, you can see that time_f only gives you upper bounds for the runtime (they say this in the book explicitly, but in a different context), because who is to say that you cannot find even "faster" equations. There are different ways you could assemble equations for computing double, and each of these ways would give you some upper bound; naturally, you would pick the lowest of these upper bounds so far.
Second, you refer to time_f as "shenanigans", but this is only because you are allowed to see how the sausage is made. As is often the case, familiarity breeds contempt. If Isabelle had time_f built into its kernel from the start (the script just runs invisibly to you inside the kernel), would you then say that there is a formal connection in Isabelle between f and its runtime complexity?
Third, if you wanted to do it not axiomatically (which is what this is: it is an axiomatic approach to runtime complexity), but definitionally, then you have to come up with a lot of definitions: You have to define a machine model (e.g. Turing Machine, or Apple M1), you have to define what it means to run functions like double on your machine (you would do this by proving morphisms between your Isabelle functions, and your Isabelle machine functions; or you only look at Isabelle machine functions), you have to say what the runtime of that is, and THEN you can start proving theorems about it. Which will be mostly just more complicated versions of what you can already prove now via time_f; but on the other hand you could then prove exact runtime costs in "machine steps", if you so like.
1 reply →