Can compilers deduce/prove mathematically?

Question

I'm starting to learn functional programming language like Haskell, ML and most of the exercises will show off things like:

   foldr (+) 0 [ 1 ..10]

which is equivalent to

   sum = 0
     for( i in [1..10] ) 
         sum += i

So that leads me to think why can't compiler know that this is Arithmetic Progression and use O(1) formula to calculate? Especially for pure FP languages without side effect? The same applies for

  sum reverse list == sum list

Given a + b = b + a and definition of reverse, can compilers/languages prove it automatically?

Answer 1

Compilers generally don't try to prove this kind of thing automatically, because it's hard to implement.

As well as adding the logic to the compiler to transform one fragment of code into another, you have to be very careful that it only tries to do it when it's actually safe - i.e. there are often lots of "side conditions" to worry about. For example in your example above, someone might have written an instance of the type class Num (and hence the (+) operator) where the a + b is not b + a.

However, GHC does have rewrite rules which you can add to your own source code and could be used to cover some relatively simple cases like the ones you list above, particularly if you're not too bothered about the side conditions.

For example, and I haven't tested this, you might use the following rule for one of your examples above:

{-# RULES
  "sum/reverse"    forall list .  sum (reverse list) = sum list
    #-}

Note the parentheses around reverse list - what you've written in your question actually means (sum reverse) list and wouldn't typecheck.

EDIT:

As you're looking for official sources and pointers to research, I've listed a few. Obviously it's hard to prove a negative but the fact that no-one has given an example of a general-purpose compiler that does this kind of thing routinely is probably quite strong evidence in itself.

• As others have pointed out, even simple arithmetic optimisations are surprisingly dangerous, particularly on floating point numbers, and compilers generally have flags to turn them off - for example Visual C++, gcc. Even integer arithmetic isn't always clear-cut and people occasionally have big arguments about how to deal with things like overflow.

• As Joachim noted, integer variables in loops are one place where slightly more sophisticated optimisations are applied because there are actually significant wins to be had. Muchnick's book is probably the best general source on the topic but it's not that cheap. The wikipedia page on strength reduction is probably as good an introduction as any to one of the standard optimisations of this kind, and has some references to the relevant literature.

• FFTW is an example of a library that does all kinds of mathematical optimization internally. Some of its code is generated by a customised compiler the authors wrote specifically for the purpose. It's worthwhile because the authors have domain-specific knowledge of optimizations that in the specific context of the library are both worth the effort and safe

• People sometimes use template metaprogramming to write "self-optimising libraries" that again might rely on arithmetic identities, see for example Blitz++. Todd Veldhuizen's PhD dissertation has a good overview.

• If you descend into the realms of toy and academic compilers all sorts of things go. For example my own PhD dissertation is about writing inefficient functional programs along with little scripts that explain how to optimise them. Many of the examples (see Chapter 6) rely on applying arithmetic rules to justify the underlying optimisations.

Also, it's worth emphasising that the last few examples are of specialised optimisations being applied only to certain parts of the code (e.g. calls to specific libraries) where it is expected to be worthwhile. As other answers have pointed out, it's simply too expensive for a compiler to go searching for all possible places in an entire program where an optimisation might apply. The GHC rewrite rules that I mentioned above are a great example of a compiler exposing a generic mechanism for individual libraries to use in a way that's most appropriate for them.

Answer 2

The answer

No, compilers don’t do that kind of stuff.

One reason why

And for your examples, it would even be wrong: Since you did not give type annotations, the Haskell compiler will infer the most general type, which would be

foldr (+) 0 [ 1 ..10]  :: Num a => a

and similar

(\list -> sum (reverse list)) :: Num a => [a] -> a

and the Num instance for the type that is being used might well not fulfil the mathematical laws required for the transformation you suggest. The compiler should, before everything else, avoid to change the meaning (i.e. the semantics) of your program.

More pragmatically: The cases where the compiler could detect such large-scale transformations rarely occur in practice, so it would not be worth it to implement them.

An exception

Note notable exceptions are linear transformations in loops. Most compilers will rewrite

for (int i = 0; i < n; i++) {
   ... 200 + 4 * i ...
}

to

for (int i = 0, j = 200; i < n; i++, j += 4) {
   ... j ...
}

or something similar, as that pattern does often occur in code working on array.