Comment by dwohnitmok
3 hours ago
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
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.