Proof assistants are a valuable tool for verifying the correctness of proofs of mathematical theorems.

When dealing with proofs of correctness of algorithms, one is not only interested on showing that the algorithm indeed works correctly, but also on showing some upper bound on the execution of the algorithm.

Can proof assistants based on dependent type theory be used in a natural way to prove upper bounds on the running time of algorithms (besides of course of proving their correctness)? What is the standard approach to do so?

If such assistants are not appropriate, is there some other kind of proof assistant that can do the job?

Obs: When I say time, I mean the complexity theorist notion of time, in the sense of number of steps in an idealized RAM machine. I don't care about formalization of actual hardware and physical time. Therefore, although Neel Krishnaswami is interesting, I'm not accepting it because it is far more complicated than what I'm looking for.

As usual, (a) the high-level conceptual approach is basically the same as it is on paper, but (b) mechanization makes new things reasonable to attempt.

The way you do things is to define a cost semantics for a programming language, where you assign a cost for each of the operations in the language. Next, you define a machine model, with its own cost semantics assigning costs to each of the primitive machine operations. Next, you prove that translating programs into the machine model is cost-preserving, so that the language-level costs correspond to the machine-level costs.

Then, you can take any particular program written in the language and prove things about its running time, memory usage, or whatever other costs your cost semantics tracks. You prove these things with math, the same as on paper. :)

However, once you have a computer checking all the details of all your proofs, new things become possible. For example, it is fairly common in paper proofs to only give the machine cost model, and handwave the language and its cost model (people say "pseudocode" when they don't want to specify the details of the language). But this is only plausible when the language and machine are very close to each other, and when you don't care about constant factors. If you need the compiler to make nontrivial optimizations, or if you need to reason about exact (and not just asymptotic) complexity, then you need to be more precise about the language.

A good example of this is the CerCo project, which did verified compilation from C to microcontroller assembly in a way that enabled source-level reasoning about things like worst-case execution times.

As Neel answered, you can (theoretically) prove anything in a proof assistant that you can prove on paper, including idealized run-times or resource usage for a program modeled using a deep embedding (see Shallow versus Deep Embeddings).

How closely your idealized representation of the run-time corresponds to the actual run-time (in milliseconds, say) of a program on a real piece of hardware depends on the fidelity of your model of operational semantics and running time, which is a rather complex question. Certainly proving $O(n)$-type bounds is feasible. Neel mentions CerCo, which allows exploring run-time in terms of assembly instructions corresponding to the source. However, the run-time of a sequence of assembly instructions is also extremely difficult to predict, given cache and pipelining considerations (among others). There is a whole body of work on this, this is one but it's a bit dated. I know of no formalization of such systems in theorem provers though.


If you have a deep embedding, then functions written in your proof language can not directly prove anything about the evaluation behavior, since the un-evaluated programs are indistinguishable from the evaluated ones: if you could prove "fact 6 reduces in $k$ steps" then you could prove the same thing about the numeral 720, which is in reduced form.

However, you could imagine a variant of the factorial function, which returns not only the result of the computation, but also a natural number denoting, say, the number of recursive calls made by the computation. This would look something like this (in OCaml notation):

let fact n = if n == 0 then (1, 0) else
    let (k, r) = fact (n-1) in
        (n * k, r+1)

It's a bit boring, but now fact 6 is (720, 6) where the second number is the number of recursions, which can be seen as a kind of run-time bound. If the definition required several recursive calls, you would add the recursion depths together to get the final result.

Elaborating on these ideas naturally leads to the kind of work by Danielsson and various others, as mentioned in the comments by gallais. It's perhaps unsurprising that these considerations lead to a "resource monad" in which to describe these recursive definitions.


Finally, it's of academic interest to note that any definition in a total language like Coq or Agda must have an intrinsic run-time upper bound: any program of size $n$ must fully evaluate in time $O(f(n))$ where $f$ is some computable function to be described by some clever proof theorist. Sadly, that bound is so enormous so as to be effectively useless; for example it is easy to describe the Ackermann function in both systems, so $f$ must grow faster than any given tower of exponentials (much, much, much faster).

  • About "academic interest": do you know of a good, up-to-date overview that lists the known best upper bounds? Proof theorists have done a lot of work on this over the last few decades, but there is terminological confusion, and proof theorists don't always name calculi in the same way that the PL community does. – Martin Berger Aug 19 '17 at 13:29
  • 1
    CerCo had a precise cost model for machine code as the microcontroller that we were targeting (a variant of the MCS51) was simple enough to guarantee that an e.g. MOV instruction always took 2 processor cycles to execute no matter what the processor's state. As a result, we could guarantee that our source level cost annotations were precise reflections of how long a basic block would take to execute. For more complex processors one would need to embrace existing WCET technology like AbsInt's aiT to generate the machine code cost model to be lifted by the compiler. – Dominic Mulligan Aug 19 '17 at 16:20
  • @DominicMulligan a clear and precise machine formalization of the execution-time properties (or a low level abstraction of these) for modern processors seems to me to be a pressing and important research problem. – cody Aug 20 '17 at 22:04
  • 1
    @MartinBerger I don't think I know better than you do! My understanding is that it is possible to take $f$ as the function $f_\alpha$ in the fast-growing hierarchy, where $\alpha$ is the proof-theoretic ordinal of the system. It's a well-known open problem to describe such an ordinal for strong systems such as Coq. The consensus is that it is hopeless, for now. For Agda the question is less hopeless but a bit confused. I don't think anyone knows the answer for the full system with induction-recursion, but without it, the answer should be close to that of simple Martin-Lof type theory... – cody Aug 20 '17 at 22:32
  • 1
    with $\omega$-many universes. I think. A nice overview can be found here and this classic article by Rathjen seems still very relevant. – cody Aug 20 '17 at 22:34

For verified complexity analysis in other theorem proving systems, see e.g. Tobias Nipkow's paper on this subject using the Isabelle theorem prover ("Amortised Complexity Verified" at ITP 2015) which presented a framework for deriving amortised cost bounds of functional data structures and applied it to a number of well known data structures. The code is freely available on the AFP. I don't think anything Nipkow does is tied to Isabelle and could be easily ported into e.g. Coq.

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.