4 ms·

> Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code. Wh

> Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code. What is the difference? You are aware that the code is also only an abstraction, right?

zelphirkalt 11mo ago
The difference is, that proving something about an abstraction doesn't prove, that you made no mistakes when translating that abstraction into the actual code running, and therefore you have not proven anything of value about the actually running code.
- auggierose 11mo ago
  If the abstraction maintains the properties you care about, PROVABLY, there is no problem. As is the case in this case. Again, the code you see in Isabelle is already an abstraction, it is not "running".
  - dwohnitmok 11mo ago
    > If the abstraction maintains the properties you care about, PROVABLY, there is no problem. This approach doesn't do that. The translation from the actual executing code to the representation used for runtime analysis is done entirely informally and not checked at all by Isabelle.
    - auggierose 11mo ago
      It explains the underlying runtime model they assume, and derives abstractions for the runtime t based on that, which are provably correct up to O(t) under the assumptions. That does not help you much if you want to know how many seconds this will run. Instead, it tells you the asymptotic runtime complexity of the various algorithms, which is all you can really expect for general functional programs without a concrete machine model.
      - dwohnitmok 11mo 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`.
        auggierose 11mo ago
        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.
        dwohnitmok 11mo ago
        > 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. theory Double imports Main begin fun double :: "nat => nat" where "double 0 = 0" | "double (Suc n) = Suc (Suc (double n))" lemma double_eq_plus: "double x = x + x" by (induction x) auto lemma double_eq_times: "double x = 2 \* x" by (induction x) auto end 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.

zelphirkalt 11mo ago

The difference is, that proving something about an abstraction doesn't prove, that you made no mistakes when translating that abstraction into the actual code running, and therefore you have not proven anything of value about the actually running code.

auggierose 11mo ago
If the abstraction maintains the properties you care about, PROVABLY, there is no problem. As is the case in this case. Again, the code you see in Isabelle is already an abstraction, it is not "running".
- dwohnitmok 11mo ago
  > If the abstraction maintains the properties you care about, PROVABLY, there is no problem. This approach doesn't do that. The translation from the actual executing code to the representation used for runtime analysis is done entirely informally and not checked at all by Isabelle.
  - auggierose 11mo ago
    It explains the underlying runtime model they assume, and derives abstractions for the runtime t based on that, which are provably correct up to O(t) under the assumptions. That does not help you much if you want to know how many seconds this will run. Instead, it tells you the asymptotic runtime complexity of the various algorithms, which is all you can really expect for general functional programs without a concrete machine model.
    - dwohnitmok 11mo 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`.
      - auggierose 11mo ago
        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.
        dwohnitmok 11mo ago
        > 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. theory Double imports Main begin fun double :: "nat => nat" where "double 0 = 0" | "double (Suc n) = Suc (Suc (double n))" lemma double_eq_plus: "double x = x + x" by (induction x) auto lemma double_eq_times: "double x = 2 \* x" by (induction x) auto end 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.