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

<p>Both of functions are expressible in Buss's <a href="http://www.math.ucsd.edu/~sbuss/ResearchWeb/BAthesis/" rel="nofollow">bounded arithmetic</a>, 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.)</p>

<p>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. </p>

CC BY-SA 3.0
2014-05-17T01:42:13.660Z
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.
MaiaVictor
CC BY-SA 3.0
2014-05-17T03:30:32.513Z
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!
shaunc
CC BY-SA 3.0
2014-05-16T02:16:38.463Z
2014-05-21T03:49:15.467Z
2014-05-21T03:49:15.467Z
shaunc
<p>Adding to shaunc's answer: the first program (idealized over integers rather than "machine" integers) is a <em>linear recurrence</em>, and it turns out there are some very general methods for solving those:</p>

<p><a href="http://en.wikipedia.org/wiki/Recurrence_relation#Solving" rel="nofollow">http://en.wikipedia.org/wiki/Recurrence_relation#Solving</a></p>

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

CC BY-SA 3.0
2014-05-21T03:47:43.390Z
Thanks, Cody -- I suspected that there was a suitable system weaker than bounded arithmetic.
shaunc
CC BY-SA 3.0
2014-05-21T00:37:10.893Z
2014-05-21T00:37:10.893Z
cody
<pre><code>def sum1(n):
    if n==0: return 0
    else: return n + sum1(n-1)

def sum2(n):
    return n*(n+1)/2
</code></pre>

<p>A compiler can not convert <code>sum1</code> into <code>sum2</code> 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 <code>sum1</code> would fall into <code>sum2</code>?</p>

CC BY-SA 3.0
2014-05-16T18:15:31.413Z
Yes, suppose the type system is strong enough to determine sum1 only receive naturals. Sorry for the mistake. This is just an example, please let me know if it is not clear what I am asking!
MaiaVictor
CC BY-SA 3.0
2014-05-16T20:55:52.343Z
Have I interpreted you correctly? I'll try to clarify if my answer is unclear.
shaunc
CC BY-SA 3.0
2014-05-16T22:37:19.570Z
These sums are http://en.wikipedia.org/wiki/Triangular_number Note that $T_{a+b} =T_{a} +T_{b}+ab$ is legal too.
Chad Brewbaker
CC BY-SA 3.0
2014-05-17T04:39:33.333Z
"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.
Sasho Nikolov
CC BY-SA 3.0
2014-05-17T05:03:00.540Z
Please elaborate.
MaiaVictor
CC BY-SA 3.0
2014-05-17T15:04:15.537Z
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.
Sasho Nikolov
CC BY-SA 3.0
2014-05-18T05:50:27.383Z
@SashoNikolov I interpret his question to mean: "A compiler cannot convert *functions like* sum1 into sum2 *in general*... but is there a restricted system *(=language)*, which still includes these two functions (and lots of other similar functions...), in which ... functional equivalence can be computed?
shaunc
CC BY-SA 3.0
2014-05-18T06:06:11.947Z
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.
MaiaVictor
CC BY-SA 3.0
2014-05-19T03:43:59.543Z
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.
Sasho Nikolov
<pl.programming-languages><computability><compilers>
Would it be possible for a compiler to convert a recursive sum into the average formula?
MaiaVictor
# Would it be possible for a compiler to convert a recursive sum into the average formula?

(Asked by: username_0 on 2014-05-16)

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?

**Tags:** pl.programming-languages, computability, compilers

> **Comments:**
> **username_0**: Yes, suppose the type system is strong enough to determine sum1 only receive naturals. Sorry for the mistake. This is just an example, please let me know if it is not clear what I am asking!  
> **username_1**: Have I interpreted you correctly? I'll try to clarify if my answer is unclear.  
> **username_2**: These sums are http://en.wikipedia.org/wiki/Triangular_number Note that $T_{a+b} =T_{a} +T_{b}+ab$ is legal too.  
> **username_3**: "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.  
> **username_0**: Please elaborate.  
> **username_3**: 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.  
> **username_1**: @SashoNikolov I interpret his question to mean: "A compiler cannot convert *functions like* sum1 into sum2 *in general*... but is there a restricted system *(=language)*, which still includes these two functions (and lots of other similar functions...), in which ... functional equivalence can be computed?  
> **username_0**: I have replied a few minutes ago the same @username_1 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.  
> **username_3**: 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.  

---

## 2 answers

### Answer by username_1 on 2014-05-16. Score: 8

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](http://www.math.ucsd.edu/~sbuss/ResearchWeb/BAthesis/), 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.

> **Comments:**
> **username_0**: 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.  
> **username_1**: 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!  

---

### Answer by username_4 on 2014-05-21. Score: 4

Adding to username_1'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).

> **Comments:**
> **username_1**: Thanks, Cody -- I suspected that there was a suitable system weaker than bounded arithmetic.  

---

