Comment by dwohnitmok
5 hours 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.
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 . Because ℰ and are extra-logical, you cannot return the inequality if it still contains ℰ or after simplification.
You will want to distinguish between user-defined functions, primitive functions for which you have built-in / configured upper bounds for ℰ and , 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. RUNTIME itself is obviously one of the functions for which you cannot say, so you should not be able to get any meaningful inequalities from equations involving RUNTIME.
I am not sure if you can derive inconsistencies from this by considering "non-terminating" functions, but 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!