<p>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.</p>

<p>The way you do things is to define a <em>cost semantics</em> 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.  </p>

<p>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. :) </p>

<p>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.</p>

<p>A good example of this is the <a href="http://cerco.cs.unibo.it/" rel="noreferrer"><em>CerCo project</em></a>, which did verified compilation from C to microcontroller assembly in a way that enabled source-level reasoning about things like worst-case execution times. </p>

CC BY-SA 3.0
2017-08-16T10:36:37.940Z
2017-08-16T10:36:37.940Z
Neel Krishnaswami
<p>For verified complexity analysis in other theorem proving systems, see e.g. Tobias Nipkow's paper on this subject using the Isabelle theorem prover ("<a href="https://www21.in.tum.de/~nipkow/pubs/itp15.pdf" rel="nofollow noreferrer">Amortised Complexity Verified</a>" 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 <a href="https://www.isa-afp.org/entries/Amortized_Complexity.html" rel="nofollow noreferrer">AFP</a>. I don't think anything Nipkow does is tied to Isabelle and could be easily ported into e.g. Coq.</p>

CC BY-SA 3.0
2017-08-19T16:17:20.013Z
2017-08-19T18:52:23.283Z
2017-08-19T18:52:23.283Z
Dominic Mulligan
<p>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 <a href="https://cstheory.stackexchange.com/questions/1370/shallow-versus-deep-embeddings">Shallow versus Deep Embeddings</a>).</p>

<p>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 <em>extremely difficult</em> to predict, given cache and pipelining considerations (among others). There is a whole body of work on this, <a href="http://ieeexplore.ieee.org/abstract/document/968618/" rel="nofollow noreferrer">this</a> is one but it's a bit dated. I know of no formalization of such systems in theorem provers though.</p>

<hr>

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

<p><strong>However</strong>, you could imagine a <em>variant</em> 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):</p>

<pre><code>let fact n = if n == 0 then (1, 0) else
    let (k, r) = fact (n-1) in
        (n * k, r+1)
</code></pre>

<p>It's a bit boring, but now <code>fact 6</code> is <code>(720, 6)</code> 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.</p>

<p>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.</p>

<hr>

<p>Finally, it's of academic interest to note that any definition in a total language like Coq or Agda must have an <em>intrinsic</em> 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, <em>much</em> faster).</p>

CC BY-SA 3.0
2017-08-19T13:29:16.477Z
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
CC BY-SA 3.0
2017-08-19T16:20:18.400Z
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
CC BY-SA 3.0
2017-08-20T22:04:22.440Z
@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
CC BY-SA 3.0
2017-08-20T22:32:46.517Z
@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
CC BY-SA 3.0
2017-08-20T22:34:57.850Z
with $\omega$-many universes. I think. A nice overview can be found [here](https://msh.revues.org/pdf/2959) and [this classic article](https://www1.maths.leeds.ac.uk/~rathjen/typeOHIO.pdf) by Rathjen seems still very relevant.
cody
CC BY-SA 3.0
2017-08-18T15:38:52.737Z
2017-08-18T15:38:52.737Z
cody
<p>Proof assistants are a valuable tool for verifying
the correctness of proofs of mathematical theorems.</p>

<p>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.</p>

<p>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?</p>

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

<p><strong>Obs:</strong> 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. </p>

CC BY-SA 3.0
2017-08-16T12:49:17.323Z
For "lightweight" and "semi-formal" time complexity analysis cf. [Nils Anders Danielsson's work](http://www.cse.chalmers.se/~nad/publications/danielsson-popl2008.html).
gallais
<type-theory><dependent-type><proof-assistants>
Proving running time upper bounds for algorithms in dependent type theory
verifying
# Proving running time upper bounds for algorithms in dependent type theory

(Asked by: username_0 on 2017-08-16)

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.

**Tags:** type-theory, dependent-type, proof-assistants
> **Comments:**
> **username_1**: For "lightweight" and "semi-formal" time complexity analysis cf. [Nils Anders Danielsson's work](http://www.cse.chalmers.se/~nad/publications/danielsson-popl2008.html).  

---

## 3 answers

### Answer by username_2 on 2017-08-16. Score: 7

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*](http://cerco.cs.unibo.it/), which did verified compilation from C to microcontroller assembly in a way that enabled source-level reasoning about things like worst-case execution times.


---

### Answer by username_3 on 2017-08-19. Score: 4

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](https://www21.in.tum.de/~nipkow/pubs/itp15.pdf)" 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](https://www.isa-afp.org/entries/Amortized_Complexity.html). I don't think anything Nipkow does is tied to Isabelle and could be easily ported into e.g. Coq.


---

### Answer by username_4 on 2017-08-18. Score: 4

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

> **Comments:**
> **username_5**: 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.  
> **username_3**: 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.  
> **username_4**: @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.  
> **username_4**: @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...  
> **username_4**: with $\omega$-many universes. I think. A nice overview can be found [here](https://msh.revues.org/pdf/2959) and [this classic article](https://www1.maths.leeds.ac.uk/~rathjen/typeOHIO.pdf) by Rathjen seems still very relevant.  

---

