2
$\begingroup$ 
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?

Improve this question
$\endgroup$
10
  • 2
    $\begingroup$ Should somatorio be replaced with sum1? $\:$ If yes, then those functions behave very differently on inputs that are not non-negative integers. $\;\;\;\;$ $\endgroup$ – user6973 May 16 '14 at 3:11
  • 2
    $\begingroup$ "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. $\endgroup$ – Sasho Nikolov May 17 '14 at 4:39
  • 2
    $\begingroup$ 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. $\endgroup$ – Sasho Nikolov May 17 '14 at 15:04
  • 1
    $\begingroup$ 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. $\endgroup$ – MaiaVictor May 18 '14 at 6:06
  • 1
    $\begingroup$ 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. $\endgroup$ – Sasho Nikolov May 19 '14 at 3:43
8
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ – MaiaVictor May 17 '14 at 1:42
  • $\begingroup$ 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! $\endgroup$ – shaunc May 17 '14 at 3:30
4
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks, Cody -- I suspected that there was a suitable system weaker than bounded arithmetic. $\endgroup$ – shaunc May 21 '14 at 3:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.