Comment by dwohnitmok

3 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.