IIRC this book unfortunately only proves correctness directly and not runtime. Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code.
Does anybody know of any languages that let you prove properties about the runtime of a function directly implemented in the language?
> 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?
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.
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".
> 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.
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.
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.
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.
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.
> 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.
I don't understand the relevance. I'm not asking for exact computation of steps. Big O is fine. And provisional on the current implementation would be the whole point.
> 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?
No. That would be a clear hack. And it would break a lot of stuff in Isabelle. For example, you would introduce a distinction between first-order and higher-order functions. E.g. how do you calculate the runtime of a function like `map` when you don't have a concrete function to do the substitution on? This kind of thing only works when you have the concrete syntax of a function, which is different from the entire rest of the way the kernel works. (BTW the way the authors of this particular book deal with `map` is they just hard-coded it by hand).
Another illustration of this problem is that you wouldn't be able to state or prove very natural theorems such as "the asymptotic runtime of a sort function based on pairwise comparison can't be less than O(n log(n))".
Just jamming it in the kernel mixes syntactic and semantic concerns together. Depending on how awkward it's done it could affect the soundness of the underlying logic.
E.g. you could just say "oh we'll just make a logical relation `T` that is filled in by the compiler as necessary so e.g. in `map` it'll just have a placeholder that can then get put in" but then what is `T` in the kernel? What's its type? Can you abstract over `T`? What's its runtime representation? Does it even have a runtime representation? What are its deductive rules? So and so forth. And the answers to all these questions are all linked together.
There's a reason why `time_f` approaches haven't been adopted. It's very easy to blow up your logical system accidentally. It's a subtle problem and why I was asking for production examples. There's been some efforts here such as RAML, but it's a thing where you need to find the right balance between a full-blown macro system and a pure denotational deductive system.
> 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
The problem isn't axiomatic vs definitional, the problem is denotational vs operational. Once you decide one way or the other then the rest comes after that. Right now you can't even write a morphism between an Isabelle function and a machine function, let alone prove it.
> I don't understand the relevance. I'm not asking for exact computation of steps. Big O is fine. And provisional on the current implementation would be the whole point.
What do you mean by "the current implementation"? Isabelle defines mathematical functions, not running code.
> No. That would be a clear hack. And it would break a lot of stuff in Isabelle.
You are thinking a little bit too simplistic here. Of course you have to do some work to integrate it properly. In particular, you would need to have to generate inequalities (upper bounds) as runtime theorems. Just as code generation (for example to Ocaml) is integrated with Isabelle, this approach could be integrated similarly, and I don't think there would be any danger to the logic. Note that for code generation, you also have to provide special theorems for higher-order functions. But it would definitely be interesting to work this out in detail.
> wouldn't be able to state or prove very natural theorems such as "the asymptotic runtime of a sort function based on pairwise comparison can't be less than O(n log(n))"
No, you wouldn't, because the approach only proves upper bounds. As stated before. So lower bounds on runtime complexity would not be natural at all in this framework.
> The problem isn't axiomatic vs definitional, the problem is denotational vs operational.
You have to explain what you mean by that. Of course you can write these morphisms, you need to define your machines and machine functions first though, which is a lot of work. Maybe start with just a Turing machine first. The upside of all this work: you could also prove theorems about lower bounds now.
> What do you mean by "the current implementation"? Isabelle defines mathematical functions, not running code.
This is the whole problem! The line gets blurry with `primrec`, `fun`, and `function` and indeed the book is treating Isabelle definitions as runnable code (and a lot of uses of Isabelle with code extraction do the same).
But precisely because Isabelle technically doesn't define running code it's really hard to make cost functions and relate them to the original Isabelle function.
E.g. here's another definition of `double`.
definition double :: "nat => nat" where
"double n = (THE y. y + n = 3 * n)"
Perfectly reasonable in Isabelle. How do you generate the cost function for it? A reasonable answer is "well you don't, you only generate them for certain kinds of definitions, just like other lemmas in Isabelle," which then leads me to...
> Of course you have to do some work to integrate it properly. In particular, you would need to have to generate inequalities (upper bounds) as runtime theorems. Just as code generation (for example to Ocaml) is integrated with Isabelle, this approach could be integrated similarly, and I don't think there would be any danger to the logic.
Okay so how would you do this? Again the point here is to have some formal connection between the runtime cost function and the original function. This boils down to one of two ways in Isabelle (which technically are both the same, but they have meaningful ergonomic differenes). One is as a relation so e.g. a `T` such that
T_rel(f, time_f)
or as a function such that
T_fun(f) = time_f
If you introduce these, then in the former case, how do you prove `not(T_rel(f, time_f))`? In the latter case, what is `T_fun(T_fun)`?
> Of course you can write these morphisms, you need to define your machines and machine functions first though, which is a lot of work.
That would also be Isabelle, but with an explicitly defined machine model as parameter of the functions of interest, which would also be phrased in terms of the machine parameter. But yes, let's ignore this possibility, it would not be pretty, for sure.
> Okay so how would you do this?
Ok, let's try to define some sort of built-in function RUNTIME.
You cannot just define RUNTIME for arbitrary expressions, and proceed with the approach in the book, as for example RUNTIME(nil) = 0 would lead to a non-sensical RUNTIME(f x1 ... xn) = 0 whenever f x1 ... xn evaluates to nil, i.e. f x1 ... xn = nil.
You would need to modify the type system so that applications of RUNTIME are properly typed,
you cannot just give it type RUNTIME : ('a => 'b) => 'a => nat,
as then RUNTIME : ('a => 'b => 'c) => 'a => nat would follow, but it should act in this case as if it had type RUNTIME : ('a => 'b => 'c) => 'a => 'b => 'nat (which it cannot actually have for the same reason).
You also cannot define RUNTIME simply as described in the book via generating equations,
as different sets of input equations (like for your double example) might lead to different runtime costs, and therefore inconsistency in the logic.
So you can only generate theorems involving RUNTIME for certain cases, and the theorems
you generate must be inequalities, not equalities.
You can do that by implementing an oracle (or kernel function) that takes in a user-defined
function f and an equation for f, and returns an inequality as a theorem for RUNTIME f ..., as otherwise explained in the book, using auxiliary functions ℰ and T. Because ℰ and T are extra-logical, you cannot return the inequality if it still contains ℰ or T after simplification.
You will want to distinguish between user-defined functions, primitive functions for which you have built-in / configured upper bounds for ℰ and T, and functions where you cannot say (expressions involving such functions will not simplify enough, and thus block theorem generation).
For example for the append example on page 8 of the (free draft of the) book, you would get inequalities
You will be able to prove what these generated inequalities allow you to prove, which are upper bounds on runtime complexity. Note that for practical purposes, these upper bounds only hold under the assumption that you actually select the best (or at least good enough) equations for evaluating the function, i.e. those equations which you used for deriving the upper bounds via the oracle. RUNTIME itself is obviously one of the functions for which you cannot say (you don't have equations for RUNTIME from which to derive anything via the oracle, just inequalities), so you should not be able to get any meaningful RUNTIME statements about RUNTIME itself.
I am not sure if you can derive inconsistencies from this by considering "non-terminating" functions, but if so, then it should be possible to deal with this by making the range of RUNTIME not just ℕ, but ℕ ∪ {∞}, or Option nat.
The next step would be to prove that this approach actually works, or to come up with examples of inconsistencies induced by it.
You're saying that RUNTIME should be a built-in function, but then all the paragraphs succeeding that demonstrate that RUNTIME cannot be a function. All the typing judgments I can think of that would let RUNTIME become an actual function would lead to being able to prove false.
Moreover, RE
> RUNTIME for certain cases, and the theorems you generate must be inequalities, not equalities.
this is impossible under Isabelle's logic. I can easily turn any theorem about an inequality into a theorem about equality via an existential statement. E.g. given `RUNTIME f y <= n` I can easily write
definition my_constant :: "nat" where
"my_constant = (THE x. RUNTIME f y = x)"
which must logically exist by the classical nature of Isabelle. And now I get to work with `my_constant`. But I can always arbitrary force `my_constant` to be `1` or `0`. Because e.g. I can always just find another function `g` equal to `f` everywhere but just hard coding the answer for `y` (such that `RUNTIME` proves it to be less than or equal to `1`) and then prove `f = g` and then substitute it in, proving `my_constant` to be less than or equal to `1`.
In fact based on this definition of RUNTIME and Leibniz equality I could "prove" that every function runs in constant time. Because e.g. I can always make another append function `append_m_n` that hard codes what the result of `append` is on lists of constant size `m` and `n` and then I prove that `append_m_n` is equal to `append` and then I get to substitute it in every theorem because of equality so on and so forth.
Going down automatically generated `RUNTIME`s seems like a dead end. It seems to be missing some form of quantification over the implementation of a function, not just the function itself. And to the extent that functions do not have implementations, it doesn't seem you can retrofit formal runtime analysis.
RUNTIME would not be an actual function, but a built-in construct with its own typing rules that don't give RUNTIME a type, but only its applications. That's why you need to modify the type system, obviously. That is not a problem.
Yes, RUNTIME cannot talk about the implementation of a function, because there is no such thing as a unique implementation of a mathematical function. It will never be able to, it just computes upper bounds of runtime complexity based on the best implementations in the form of equations you can come up with. That on its own is not a dead end, that is the design. If you want to talk about implementations, you will need to come up with an explicit machine model, as mentioned a few times before now.
Your examples are a bit too handwavy for me to see exactly how you would come up with counter examples for the proper functioning of RUNTIME. I've played around with it a bit as well, and while counter intuitive in some aspects (for example RUNTIME append ys [] <= 1 could also be shown) it encodes an interesting notion of "optimal runtime" of a mathematical function. I might be wrong though, but you'd need to come up with an actual concrete example to convince me of that. For example, how exactly would you "hardcode" a value for g at y such that g y = f y = arbitrary constant you choose? You can show g y = f y = my_constant, but how does that help you to prove my_constant <= 1? "y" is just a constant as well, it cannot be a variable, because otherwise your definition of my_constant would not be closed. Note that equalities including THE would not yield anything usable from the inequalities generator.
Furthermore, note that just because f x = g x may hold for some x, that does not mean you can prove RUNTIME f x = RUNTIME g x for that x. On the other hand, if you can prove f x = g x for all x, then you should be able to prove RUNTIME f x = RUNTIME g x as well, simply by noting that f = g, and x = x, and therefore RUNTIME f x = RUNTIME g x as well by the usual extensionality rule that would also apply to RUNTIME.
> That's why you need to modify the type system, obviously. That is not a problem.
What typing judgment rules would you have for RUNTIME?
> On the other hand, if you can prove f x = g x for all x, then you should be able to prove RUNTIME f x = RUNTIME g x as well, simply by noting that f = g, and x = x, and therefore RUNTIME f x = RUNTIME g x as well by the usual extensionality rule that would also apply to RUNTIME.
Yes that's the problem.
Take factorial.
fun factorial :: "nat => nat" where
"factorial 0 = 1"
| "factorial (Suc n) = (Suc n) * factorial n
Clearly `factorial_10_hardcoded = factorial` for all `x`. Hence `RUNTIME f x = RUNTIME g x`. `RUNTIME factorial_10_hardcoded 10 <= 1` and therefore `RUNTIME factorial 10 <= 1`. So that gives you constant time for any particular constant input. But it gets even worse!
factorial_hardcoded_a_b "nat => nat => nat => nat" where
"factorial_hard_coded_a_b a b x = if x=a then b else factorial x
And of course `RUNTIME factorial_hardcoded_a_b x b x <= 1`.
Then I can prove
FORALL n. EX b. factorial n = factorial_hardcoded_a_b n b n
which then means I can conclude `RUNTIME factorial n <= 1`.
Yes, factorial_10_hardcoded convinces me that RUNTIME is not a good idea, although it works actually as RUNTIME is supposed to work: Hardcoding the computed value for a given input is the ultimate optimisation.
Not sure about the factorial_hardcoded_a_b example, because you still need to get rid of the existential somehow, maybe via skolemisation b[n], but that does not really matter in light of factorial_10_hardcoded.
The typing rules for RUNTIME would have been simply that if f has type a_1 => ... => a_n => b for n >= 1, and x_i has type a_i, then RUNTIME f x_1 ... x_n has type b.
That would exclude the clearly problematic case RUNTIME x for n = 0, but it seems to me hardcoding is basically how you can get that case back in via extensionality.
Although, I am starting to wonder how bad the constant hardcoding case really is.
As I said before, it is to be expected: Providing a precomputed value is a very fast implementation!
I am not entirely convinced yet that it would damage what RUNTIME can say about variable inputs, so I guess a complete analysis of your hardcoded_a_b example is necessary after all.
Unfortunately proving anything about a concrete imperative implementation is orders of magnitude more complex than working with an abstraction, because you have to deal with pesky 'reality' and truly take care of every possible edge-case, so it only makes sense for the most critical applications. And sometimes there just isn't a framework to do even that, depending on your use case, and you'd have to sit down a PhD student for a while to build it. And even then you're still working with an abstraction of some kind, since you have to assume some kind of CPU architecture etc.
It really is more difficult to work with 'concrete implementations' to a degree that's fairly unintuitive if you haven't seen it first-hand.
I can't fathom how crazy it gets to model once you try to consider compilers, architectures, timings, temperatures, bit-flips & ECCs, cache misses, pseudo and "truly" random devices, threads, other processes, system load, I/O errors, networking.
To me it seems mandatory to work with some abstraction underneath that allows factoring a lot of different cases into a smaller set of possibilities that needs to be analysed.
It's also how we manage to think in a world where tiny little details do give you a likely insignificantly different world-state to think about.
Some algorithms such as binary search give an incorrect view of the overall cost. The search has a prerequisite of sorting. So, the assumption is, the data is sorted once, and searched several times, making the sorting cost insignificant.
What if the data is used for only a single lookup? For this case, actually a sequential search would have lower cost compared to sorting and binary search. Infact, sequential search may beat sorting and binary search for upto about 100 lookups. So I think it is important to consider overall cost.
It is not an "incorrect view of the overall cost".
Binary search talks about how long the search takes with this particular algorithm assuming the data is sorted. It does not talk at all about scenarios where the data is not sorted. In particular, it does not provide any views on costs without this assumption, let alone an incorrect one.
Yes, YOU need to consider when it is appropriate to use binary search. That is the case with all algorithms you will ever apply, and goes without saying.
But how the data got sorted is irrelevant to the speed of the algorithm: for example, you could use binary search as part of an algorithm to find the insertion point of a new element in an always sorted data structure, meaning that sorting the data is never necessary.
The overall journey matters. For example, for some flight journeys, the flight-time is only a fraction of the overall time taken by the journey, which could makes it faster if you use road or rail transport. Flight speed doesn't matter.
But that is an unanswerable question which depends on how the data structure is used. The reasonable thing is to calculate the cost for the operations separately and let whoever uses the algorithms figure out what that means for their use case.
IIRC this book unfortunately only proves correctness directly and not runtime. Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code.
Does anybody know of any languages that let you prove properties about the runtime of a function directly implemented in the language?
Eiffel is the language you are looking for. It's pre-conditions and post-conditions prove the properties of the code that you actually are executing.
The book that does the equivalent but with the properties checked at runtime is: Object Structures (like data structures but with objects).
Here is the link:
https://openlibrary.org/works/OL2979696W/Object_structures?e...
> 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?
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.
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".
> 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.
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.
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.
> 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.
I don't understand the relevance. I'm not asking for exact computation of steps. Big O is fine. And provisional on the current implementation would be the whole point.
> 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?
No. That would be a clear hack. And it would break a lot of stuff in Isabelle. For example, you would introduce a distinction between first-order and higher-order functions. E.g. how do you calculate the runtime of a function like `map` when you don't have a concrete function to do the substitution on? This kind of thing only works when you have the concrete syntax of a function, which is different from the entire rest of the way the kernel works. (BTW the way the authors of this particular book deal with `map` is they just hard-coded it by hand).
Another illustration of this problem is that you wouldn't be able to state or prove very natural theorems such as "the asymptotic runtime of a sort function based on pairwise comparison can't be less than O(n log(n))".
Just jamming it in the kernel mixes syntactic and semantic concerns together. Depending on how awkward it's done it could affect the soundness of the underlying logic.
E.g. you could just say "oh we'll just make a logical relation `T` that is filled in by the compiler as necessary so e.g. in `map` it'll just have a placeholder that can then get put in" but then what is `T` in the kernel? What's its type? Can you abstract over `T`? What's its runtime representation? Does it even have a runtime representation? What are its deductive rules? So and so forth. And the answers to all these questions are all linked together.
There's a reason why `time_f` approaches haven't been adopted. It's very easy to blow up your logical system accidentally. It's a subtle problem and why I was asking for production examples. There's been some efforts here such as RAML, but it's a thing where you need to find the right balance between a full-blown macro system and a pure denotational deductive system.
> 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
The problem isn't axiomatic vs definitional, the problem is denotational vs operational. Once you decide one way or the other then the rest comes after that. Right now you can't even write a morphism between an Isabelle function and a machine function, let alone prove it.
> I don't understand the relevance. I'm not asking for exact computation of steps. Big O is fine. And provisional on the current implementation would be the whole point.
What do you mean by "the current implementation"? Isabelle defines mathematical functions, not running code.
> No. That would be a clear hack. And it would break a lot of stuff in Isabelle.
You are thinking a little bit too simplistic here. Of course you have to do some work to integrate it properly. In particular, you would need to have to generate inequalities (upper bounds) as runtime theorems. Just as code generation (for example to Ocaml) is integrated with Isabelle, this approach could be integrated similarly, and I don't think there would be any danger to the logic. Note that for code generation, you also have to provide special theorems for higher-order functions. But it would definitely be interesting to work this out in detail.
> wouldn't be able to state or prove very natural theorems such as "the asymptotic runtime of a sort function based on pairwise comparison can't be less than O(n log(n))"
No, you wouldn't, because the approach only proves upper bounds. As stated before. So lower bounds on runtime complexity would not be natural at all in this framework.
> The problem isn't axiomatic vs definitional, the problem is denotational vs operational.
You have to explain what you mean by that. Of course you can write these morphisms, you need to define your machines and machine functions first though, which is a lot of work. Maybe start with just a Turing machine first. The upside of all this work: you could also prove theorems about lower bounds now.
> What do you mean by "the current implementation"? Isabelle defines mathematical functions, not running code.
This is the whole problem! The line gets blurry with `primrec`, `fun`, and `function` and indeed the book is treating Isabelle definitions as runnable code (and a lot of uses of Isabelle with code extraction do the same).
But precisely because Isabelle technically doesn't define running code it's really hard to make cost functions and relate them to the original Isabelle function.
E.g. here's another definition of `double`.
Perfectly reasonable in Isabelle. How do you generate the cost function for it? A reasonable answer is "well you don't, you only generate them for certain kinds of definitions, just like other lemmas in Isabelle," which then leads me to...> Of course you have to do some work to integrate it properly. In particular, you would need to have to generate inequalities (upper bounds) as runtime theorems. Just as code generation (for example to Ocaml) is integrated with Isabelle, this approach could be integrated similarly, and I don't think there would be any danger to the logic.
Okay so how would you do this? Again the point here is to have some formal connection between the runtime cost function and the original function. This boils down to one of two ways in Isabelle (which technically are both the same, but they have meaningful ergonomic differenes). One is as a relation so e.g. a `T` such that
or as a function such that If you introduce these, then in the former case, how do you prove `not(T_rel(f, time_f))`? In the latter case, what is `T_fun(T_fun)`?> Of course you can write these morphisms, you need to define your machines and machine functions first though, which is a lot of work.
I meant writing them in Isabelle.
> I meant writing them in Isabelle.
That would also be Isabelle, but with an explicitly defined machine model as parameter of the functions of interest, which would also be phrased in terms of the machine parameter. But yes, let's ignore this possibility, it would not be pretty, for sure.
> Okay so how would you do this?
Ok, let's try to define some sort of built-in function RUNTIME.
You cannot just define RUNTIME for arbitrary expressions, and proceed with the approach in the book, as for example RUNTIME(nil) = 0 would lead to a non-sensical RUNTIME(f x1 ... xn) = 0 whenever f x1 ... xn evaluates to nil, i.e. f x1 ... xn = nil.
You would need to modify the type system so that applications of RUNTIME are properly typed, you cannot just give it type RUNTIME : ('a => 'b) => 'a => nat, as then RUNTIME : ('a => 'b => 'c) => 'a => nat would follow, but it should act in this case as if it had type RUNTIME : ('a => 'b => 'c) => 'a => 'b => 'nat (which it cannot actually have for the same reason).
You also cannot define RUNTIME simply as described in the book via generating equations, as different sets of input equations (like for your double example) might lead to different runtime costs, and therefore inconsistency in the logic.
So you can only generate theorems involving RUNTIME for certain cases, and the theorems you generate must be inequalities, not equalities.
You can do that by implementing an oracle (or kernel function) that takes in a user-defined function f and an equation for f, and returns an inequality as a theorem for RUNTIME f ..., as otherwise explained in the book, using auxiliary functions ℰ and T. Because ℰ and T are extra-logical, you cannot return the inequality if it still contains ℰ or T after simplification.
You will want to distinguish between user-defined functions, primitive functions for which you have built-in / configured upper bounds for ℰ and T, and functions where you cannot say (expressions involving such functions will not simplify enough, and thus block theorem generation).
For example for the append example on page 8 of the (free draft of the) book, you would get inequalities
You will be able to prove what these generated inequalities allow you to prove, which are upper bounds on runtime complexity. Note that for practical purposes, these upper bounds only hold under the assumption that you actually select the best (or at least good enough) equations for evaluating the function, i.e. those equations which you used for deriving the upper bounds via the oracle. RUNTIME itself is obviously one of the functions for which you cannot say (you don't have equations for RUNTIME from which to derive anything via the oracle, just inequalities), so you should not be able to get any meaningful RUNTIME statements about RUNTIME itself.I am not sure if you can derive inconsistencies from this by considering "non-terminating" functions, but if so, then it should be possible to deal with this by making the range of RUNTIME not just ℕ, but ℕ ∪ {∞}, or Option nat.
The next step would be to prove that this approach actually works, or to come up with examples of inconsistencies induced by it.
Hope this helps!
This approach seems entirely unworkable.
You're saying that RUNTIME should be a built-in function, but then all the paragraphs succeeding that demonstrate that RUNTIME cannot be a function. All the typing judgments I can think of that would let RUNTIME become an actual function would lead to being able to prove false.
Moreover, RE
> RUNTIME for certain cases, and the theorems you generate must be inequalities, not equalities.
this is impossible under Isabelle's logic. I can easily turn any theorem about an inequality into a theorem about equality via an existential statement. E.g. given `RUNTIME f y <= n` I can easily write
which must logically exist by the classical nature of Isabelle. And now I get to work with `my_constant`. But I can always arbitrary force `my_constant` to be `1` or `0`. Because e.g. I can always just find another function `g` equal to `f` everywhere but just hard coding the answer for `y` (such that `RUNTIME` proves it to be less than or equal to `1`) and then prove `f = g` and then substitute it in, proving `my_constant` to be less than or equal to `1`.In fact based on this definition of RUNTIME and Leibniz equality I could "prove" that every function runs in constant time. Because e.g. I can always make another append function `append_m_n` that hard codes what the result of `append` is on lists of constant size `m` and `n` and then I prove that `append_m_n` is equal to `append` and then I get to substitute it in every theorem because of equality so on and so forth.
Going down automatically generated `RUNTIME`s seems like a dead end. It seems to be missing some form of quantification over the implementation of a function, not just the function itself. And to the extent that functions do not have implementations, it doesn't seem you can retrofit formal runtime analysis.
RUNTIME would not be an actual function, but a built-in construct with its own typing rules that don't give RUNTIME a type, but only its applications. That's why you need to modify the type system, obviously. That is not a problem.
Yes, RUNTIME cannot talk about the implementation of a function, because there is no such thing as a unique implementation of a mathematical function. It will never be able to, it just computes upper bounds of runtime complexity based on the best implementations in the form of equations you can come up with. That on its own is not a dead end, that is the design. If you want to talk about implementations, you will need to come up with an explicit machine model, as mentioned a few times before now.
Your examples are a bit too handwavy for me to see exactly how you would come up with counter examples for the proper functioning of RUNTIME. I've played around with it a bit as well, and while counter intuitive in some aspects (for example RUNTIME append ys [] <= 1 could also be shown) it encodes an interesting notion of "optimal runtime" of a mathematical function. I might be wrong though, but you'd need to come up with an actual concrete example to convince me of that. For example, how exactly would you "hardcode" a value for g at y such that g y = f y = arbitrary constant you choose? You can show g y = f y = my_constant, but how does that help you to prove my_constant <= 1? "y" is just a constant as well, it cannot be a variable, because otherwise your definition of my_constant would not be closed. Note that equalities including THE would not yield anything usable from the inequalities generator.
Furthermore, note that just because f x = g x may hold for some x, that does not mean you can prove RUNTIME f x = RUNTIME g x for that x. On the other hand, if you can prove f x = g x for all x, then you should be able to prove RUNTIME f x = RUNTIME g x as well, simply by noting that f = g, and x = x, and therefore RUNTIME f x = RUNTIME g x as well by the usual extensionality rule that would also apply to RUNTIME.
> That's why you need to modify the type system, obviously. That is not a problem.
What typing judgment rules would you have for RUNTIME?
> On the other hand, if you can prove f x = g x for all x, then you should be able to prove RUNTIME f x = RUNTIME g x as well, simply by noting that f = g, and x = x, and therefore RUNTIME f x = RUNTIME g x as well by the usual extensionality rule that would also apply to RUNTIME.
Yes that's the problem.
Take factorial.
I can then define Clearly `factorial_10_hardcoded = factorial` for all `x`. Hence `RUNTIME f x = RUNTIME g x`. `RUNTIME factorial_10_hardcoded 10 <= 1` and therefore `RUNTIME factorial 10 <= 1`. So that gives you constant time for any particular constant input. But it gets even worse! And of course `RUNTIME factorial_hardcoded_a_b x b x <= 1`.Then I can prove
which then means I can conclude `RUNTIME factorial n <= 1`.Yes, factorial_10_hardcoded convinces me that RUNTIME is not a good idea, although it works actually as RUNTIME is supposed to work: Hardcoding the computed value for a given input is the ultimate optimisation.
Not sure about the factorial_hardcoded_a_b example, because you still need to get rid of the existential somehow, maybe via skolemisation b[n], but that does not really matter in light of factorial_10_hardcoded.
The typing rules for RUNTIME would have been simply that if f has type a_1 => ... => a_n => b for n >= 1, and x_i has type a_i, then RUNTIME f x_1 ... x_n has type b.
That would exclude the clearly problematic case RUNTIME x for n = 0, but it seems to me hardcoding is basically how you can get that case back in via extensionality.
Although, I am starting to wonder how bad the constant hardcoding case really is.
As I said before, it is to be expected: Providing a precomputed value is a very fast implementation!
I am not entirely convinced yet that it would damage what RUNTIME can say about variable inputs, so I guess a complete analysis of your hardcoded_a_b example is necessary after all.
Unfortunately proving anything about a concrete imperative implementation is orders of magnitude more complex than working with an abstraction, because you have to deal with pesky 'reality' and truly take care of every possible edge-case, so it only makes sense for the most critical applications. And sometimes there just isn't a framework to do even that, depending on your use case, and you'd have to sit down a PhD student for a while to build it. And even then you're still working with an abstraction of some kind, since you have to assume some kind of CPU architecture etc.
It really is more difficult to work with 'concrete implementations' to a degree that's fairly unintuitive if you haven't seen it first-hand.
I can't fathom how crazy it gets to model once you try to consider compilers, architectures, timings, temperatures, bit-flips & ECCs, cache misses, pseudo and "truly" random devices, threads, other processes, system load, I/O errors, networking.
To me it seems mandatory to work with some abstraction underneath that allows factoring a lot of different cases into a smaller set of possibilities that needs to be analysed.
It's also how we manage to think in a world where tiny little details do give you a likely insignificantly different world-state to think about.
https://markushimmel.de/blog/my-first-verified-imperative-pr...
Lean
Verification of "runtimes" in the sense of GP is not mentioned at all in the article you linked.
Some algorithms such as binary search give an incorrect view of the overall cost. The search has a prerequisite of sorting. So, the assumption is, the data is sorted once, and searched several times, making the sorting cost insignificant.
What if the data is used for only a single lookup? For this case, actually a sequential search would have lower cost compared to sorting and binary search. Infact, sequential search may beat sorting and binary search for upto about 100 lookups. So I think it is important to consider overall cost.
It is not an "incorrect view of the overall cost".
Binary search talks about how long the search takes with this particular algorithm assuming the data is sorted. It does not talk at all about scenarios where the data is not sorted. In particular, it does not provide any views on costs without this assumption, let alone an incorrect one.
Yes, YOU need to consider when it is appropriate to use binary search. That is the case with all algorithms you will ever apply, and goes without saying.
But how the data got sorted is irrelevant to the speed of the algorithm: for example, you could use binary search as part of an algorithm to find the insertion point of a new element in an always sorted data structure, meaning that sorting the data is never necessary.
The overall journey matters. For example, for some flight journeys, the flight-time is only a fraction of the overall time taken by the journey, which could makes it faster if you use road or rail transport. Flight speed doesn't matter.
But that is an unanswerable question which depends on how the data structure is used. The reasonable thing is to calculate the cost for the operations separately and let whoever uses the algorithms figure out what that means for their use case.