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

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?

• Should somatorio be replaced with sum1? $\:$ If yes, then those functions behave very differently on inputs that are not non-negative integers. $\;\;\;\;$
– user6973
Commented May 16, 2014 at 3:11
• "A compiler can not convert sum1 into sum2 because function equality in turing-complete languages is undecidable." No, this is not true. There surely exists a compiler that will convert sum1 into sum2. Commented May 17, 2014 at 4:39
• Take your favorite compiler. Augment it to check for the code of sum1 and program it to convert it to sum2. Done. You misunderstand what undecidability means: it means that for any compiler, there exist two equivalent programs whose equivalence the compiler can't detect. But you can always make a compiler that recognizes two particular pieces of code as equal. Commented May 17, 2014 at 15:04
• I have replied a few minutes ago the same @shaunc said, but for some reason it didn't go. So, he is correct. I don't mean you can't hardcode a compilation from sum1 to sum2 - I mean that compilers can't, in general, for turing-complete languages, find the most optimal (in number of reductions) equivalent program. I'm asking if there are simpler systems/languages with that property. Commented May 18, 2014 at 6:06
• The problem is that is a very imprecise question. What kinds of programs would you want to be expressible in the programming language? Be more specific than "things like sum1". And you may want to edit your questions so that it does not make claims that are not true. Commented May 19, 2014 at 3:43

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.

• I "guess" your answer is correct but after reading a few pages I still had no idea what bounded arithmetic is, but, certainly, it is not what I am looking for ): great answer netherless... so, thanks. Commented May 17, 2014 at 1:42
• The general topic you might want to explore is "implicit computational complexity" which tries to study systems whose expressiveness is inherently limited (by some complexity class). You might find systems based on linear logic a bit more comprehensible (...perhaps... :)) ... good luck! Commented May 17, 2014 at 3:30

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

• Thanks, Cody -- I suspected that there was a suitable system weaker than bounded arithmetic. Commented May 21, 2014 at 3:47