Comment by dwohnitmok
1 day ago
> 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.
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.