Comment by auggierose

> 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

    RUNTIME append [] ys ≤ 1
    RUNTIME append (x#xs) ys ≤ RUNTIME append xs ys + 1

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!