Recently I've started to feel a little weird about complexity analysis in programming languages. It's started to feel a little arbitrary to me. By this I mean analysis of space/time complexity of certain programs in any arbitrary programming language.

Let me explain myself. Take for instance time complexity analysis. We all know Big O/Omega/Theta notation, and what it basically comes down to (lower/upper bound on the asymptotic amount of instructions a specific program/algorithm takes to execute to an arbitrary input, depending on the case).

But the connection between the maths behind it (e.g the actual mathematical definition of O(f(n)) ) and the specific programming language you are analysing seems blurry to me.

For instance, if imagine I have this program below:

public int foo(int n){ int res = 0; for(i = 1; i <= n; i++){ res += i; } return res; }

We can easily analyse it and say it has O(n) complexity. But why? The usual argument seems to be a little ad hoc to the specific language. Like in this case, you'd say something like

*"Hmm, well, we can assume that we take the unit as an assignment or operator application, like ":=" or "+", so we try to count the number of times those are called. Also, the parameter is an integer 'n', so we know that the input is this 'n', so that will be the domain of our Big O function. Then, we know that for-loops represent an interation of n amount of instructions when they have the specific form "for(i = 0; i < n; i++)", so we can figure out this whole function is O(n)"*

But to me, all of the claims you would make in a statement like the above are not subtantiated. I mean, they are intuitive and make sense, but there is no formal process that

**proves**that this function has O(n) time complexity. You just basically figured that out of thin air.

But this is in no way a good way to reason about arbitrary programs. Arbitrary programs are not pure, don't have a neatly defined interface where the "inputs" are nicely shown, nor they have the specific constructs (like this specific for-loop, assignments, etc) that allow you to reason about its time complexity as neatly as you did above.

In those cases there is no way to reason about the asymptotic complexity of the program, other than trying some ad hoc reasoning, greatly simplifying it. But in that case it's very possible you get it wrong, and have no way to verify it (other than thinking about it harder).

One of the problems I find is that this type of complexity analysis is defined abstractly. It's basically pure math, which we then try to "bring down" to specific languages and their behavior. Big O never says anything about for-loops, or assignments. No, it only talks about mathematical functions. The rest is all on us. The translation between the mathematical realm of the analysis, and the computational realm doesn't seem well defined to me.

Is it possible to have a formal theory of complexity analysis, at the very least for a specific programming language, or a subset of such a programming language? I want to be able to deconstruct a program into its abstract syntax tree, and be able to traverse it using logic rules to find out its time and space complexity in a sure way, just like a typechecker traverses the abstract syntax tree, following logic rules to find out if the program is correctly typed in a sure way.

Is this possible?

This post has been edited by **gonzaw**: 22 March 2015 - 05:44 PM