Would it be possible for a compiler to convert a recursive sum into the average formula?

Question

def sum1(n):
    if n==0: return 0
    else: return n + sum1(n-1)

def sum2(n):
    return n*(n+1)/2

A compiler can not convert sum1 into sum2 because function equality in turing-complete languages is undecidable. My question is: is there a system strong enough to express both functions, that is also weak enough to a compiler can make the conversion? Or, even better, is there a simple system where the mere reduction of sum1 would fall into sum2?

Answer 1

I assume you are asking whether a "reasonable" system exists that can express these functions and also also decide whether any two expressible function definitions define the same function. (An unreasonable system would be, for example, the language which has only the two function definitions above in it...)

Both of functions are expressible in Buss's bounded arithmetic, so yes, to your first question, though I'm not aware that anyone has actually converted these systems into practical computer languages. For one thing, the algorithm should exist, but are (almost?) certainly unfeasible unless P==NP. (Almost: I'd guess that the problem of function equivalence in any of Buss's systems is at least NP hard, but I have no proof.)

For your second question, I guess we would have to define "reasonable" meant more carefully. It seems plausible to me that one could create a "combinatorics expert system" that could recognize and "automatically optimize" many such simple functions -- perhaps it would look something like "Mathematica" :) -- but I assume that isn't what you are talking about.

Answer 2

Adding to shaunc's answer: the first program (idealized over integers rather than "machine" integers) is a linear recurrence, and it turns out there are some very general methods for solving those:

http://en.wikipedia.org/wiki/Recurrence_relation#Solving

Note that this is similar to a discrete version of differential equations, so things get complicated rather fast, and non-linear relations are quite hard in general (undecidable in fact).