Comment by auggierose
8 hours ago
> 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.