Can one automate algorithmic analysis?

Question

Has anyone thought about the possibility of a programming language, and a compiler, such that the compiler can automatically do worst-case asymptotic analysis? The use case I have in mind is a programming language where I write code, and compile. The compiler tells me that my code runs in O(n^2) (for example). It does this by doing what the smart people who do algorithmic analysis do, possibly counting loops and so on.

• Because of halting problem issues, and since one can have programs that work by dovetailing, for example Levin's algorithm for SAT that runs in polynomial time iff P=NP, I suspect that one may have to design the programming language to be sufficiently restrictive to allow something like this. Are there negative results, which rule out certain kinds of programming languages from having such compilers.

• I would also be interested in systems that give not an exact asymptotic analysis, but an "interesting" upper bound.

• I am specifically NOT interested in black box and statistical methods that sample from inputs of particular length, and find out how long the program takes. These methods are very interesting, but they are not what I'm looking for. I am interested in exact methods that may give approximate bounds.

I would be very grateful if someone could point me to some references on work in this direction.

Answer 1

Implicit Complexity has taught us that (some) complexity classes can be classified by type systems, in the sense that there are type systems that only accept polynomial programs, for example. One more practical-minded offshoot of this research is RAML (Resource Aware ML), a functional programming language with a type system that will give you precise information of the running times of its programs. It is more precise, in fact, than big-O complexity, are constant factors are also included, parametrized by a cost model for the base operations.

You may think that this is cheating: surely some algorithms have a complexity that is very hard to compute precisely, so how could this language easily determine the complexity of its programs? The trick is that there are many ways to express a given algorithm, some which the type-system will reject (it rejects some fine programs), and some, maybe, that it accept. So the user doesn't get the world for free: he or she doesn't have to compute cost estimations anymore, but need to figure how to express code in a way that is accepted by the system.

(It is always the same trick, as with programming languages with only terminating computations, or provable security properties, etc.)

Answer 2

The COSTA tool developed by the COSTA research group does exactly what you want. Given a program (in Java bytecode format), the tool produces a cost equation based on a cost model provided by the programmer. The cost model can involve entities such as runtime, memory usage, or billable events (such as sending text messages). The runtime equation is then solved using a dedicated tool to produce a closed form, worst-case upper bound of the cost model.

Naturally, the tool does not work in all cases, either by failing to produce a runtime equation or by failing to find a closed form. This is not surprising.

Answer 3

I actually thought about the same question a while ago. Here is the train of thought I had:

As you said the halting problem is an issue. To avoid this we need a language which only allows programs that always halt. On the other hand our language needs to be expressive enough to deal with most common problems(e.g. it should at least capture all of the complexity class EXP).

So, let's look at LOOP programs. A LOOP program always halts and its expressiveness is way beyond EXP - to get a better idea: you can simulate any TM for which the runtime function can be expressed as LOOP program.

Now, we can look at the nesting depth and the magnitude of the number of repetitions for every loop from a syntactic point of view and we have a starting point(dont know how far this takes us though). However, consider the following problem:

We want to implement the function $f(n)$:

$f(n) = y$ such that $y$ is the first prime number after $n$ with $y > n$

Let's assume we have a function $p(n)$ which tells us whether a number $n$ is prime or not. Then to implement $f(n)$ most of us would probably write something like:

y := n + 1
while not prime(y) 
    y++
return y

Now, how are we going to do this with only bounded loops? The problem now becomes to think about an upper bound for the range of numbers we have to search.

But that was what we wanted our compiler to tell us in some sense! So, we just shifted the problem of pondering about time complexiy to the programmer. By the way, the following sentence gives us the upper bound for our problem: $$ \forall \text{ prime } p \phantom{a} \exists \text{ prime } p' : p < p' \leq p! + 1 $$

My intuition here is that the only information a compiler can give you is from carefully analyzing the syntax which in the end is provided by the programmer. So, enabling the compiler to make any meaningful statement about the time complexity of a program means to force the programmer to incorporate this information into the program.

However, the last paragraph is subjective and there certainly might be other possible approaches which yield interesting results. I just wanted to give an idea of what not to expect when going down this road.