Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

When are two proofs essentially the same? (2007)

gowers.wordpress.com

Post reply on HN
Print view View original

71–80 of 111 posts

Re: When are two proofs essentially the same? (2007)

#71

Post by Jtsummers »

Dylan16807 wrote: post #70
zeroonetwothree wrote: post #68

Earlier quoted context omitted.

I assume they mean the size of the address is log n, since there are >n addresses.

If we don't treat almost all integers in an algorithm as fixed size then the analysis gets really messy and annoying in a way that has nothing to do with real computers. And if the algorithm actually did anything with the value that made it grow or shrink with the recursion, the TCO version would stop being O(n) under such a framework. This only works because it's passing 0 around every iteration. And this probably a…

I was going to write something similar.

Regardless, the comment I replied to is fundamentally confused (presented a tail recursive algorithm and said it didn't have tail calls, presented a linear algorithm that uses a linear amount of memory and claims it's O(n log n) for some reason but no clarification if it's in time or space). I'd rather hear from the person I responded to than whatever guesses the rest of us can come up with because it needs several points of clarification to be understood.

Re: When are two proofs essentially the same? (2007)

#72

Post by tightbookkeeper »

jkaptur wrote: post #32

I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs to be identical. "... it has been argued that there are cases in which it is not possible to determine whether two programs are the same without making reference to an external semantics. Sprevak (2010) proposes to consider two programs for addition which diff…

Knuth answers this question in chapter 0.

Re: When are two proofs essentially the same? (2007)

#73

Post by tightbookkeeper »

pkoird wrote: post #2

If I were allowed a small philosophical leeway, I'd argue that two correct proofs are always the same. For sure they may contain different words or make use of different "abstractions", but it just seems to me that these abstractions should be equivalent if one were willing to unravel it all to a certain degree. Essentially, all proof is, is a statement that says "this is true" and no matter which language you use to…

No. Because the whole point of proof from a human perspective is to express understanding of the question, not merely answer it.

Re: When are two proofs essentially the same? (2007)

#74

Post by cloogshicer »

tightbookkeeper wrote: post #72
jkaptur wrote: post #32

I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs to be identical. "... it has been argued that there are cases in which it is not possible to determine whether two programs are the same without making reference to an external semantics. Sprevak (2010) proposes to consider two programs for addition which diff…

Knuth answers this question in chapter 0.

In which book? Sounds interesting.

Re: When are two proofs essentially the same? (2007)

#75

Post by mjcohen »

pkoird wrote: post #2

If I were allowed a small philosophical leeway, I'd argue that two correct proofs are always the same. For sure they may contain different words or make use of different "abstractions", but it just seems to me that these abstractions should be equivalent if one were willing to unravel it all to a certain degree. Essentially, all proof is, is a statement that says "this is true" and no matter which language you use to…

How abut the following proofs that sqrt{2} is irrational.

1. If 2=a^2/b^2 with a and b relatively prime then a^2=2b^2 so a is even, and, letting a=2c, b is also even a contradiction.

2. Use the lemma that a positive real r is rational if and only if there is a positive integer b such that br is an integer. (Proof left to the reader.) if sqrt{2} is ration then there is an integer b such that bsqrt{2}=a for some integer a. Let b be the smallest such integer. Then, if c=b(sqrt{2}-1) then c is smaller than b, c=bsqrt{2}-b is an integer, and sqrt{2}c=sqrt{2}b(sqrt{2}-1)=2b-b*sqrt{2} is an integer, a contradiction (this uses infinite descent).

3. Use the theorem that if x, y, and n are positive integers such that x^2-ny^2=1 then sqrt{n} is irrational, and apply with n=2, x=3, y=2. Proof of theorem. a. If x^2-ny^2=1, then using (x^2-ny^2)^2=(x^2+ny^2)^2-n(2xy)^2 to show that there are arbitrarily large solutions to x^2-ny^2=1. b. If n=a^2/b^2 then 1=x^2-(a^2/b^2)y^2 so b^2=b^2x^2-a^2y^2=(bx+ay)(bx-ay)>=bx+ay>bx so b>x but this contradicts the existence of arbitrarily large x.

How are any of these the same as any other?

Re: When are two proofs essentially the same? (2007)

#76

Post by chongli »

setopt wrote: post #47
chongli wrote: post #37

Earlier quoted context omitted.

I think it's also important to make a distinction between a pair of programs which compute the same function using an identical amount of space and time and a pair of programs which compute the same function with different amounts of either space or time (or both). Two programs might compute the same function and be considered formally identical in that sense but may be in radically different complexity classes [O(1)…

On the other hand, compiler tricks like tail call optimization can e.g. reduce an O(n) algorithm to an O(1) algorithm. Is it a “different program” if the same source code is compiled with a new compiler?

Tail call elimination is not an optimization because it changes the semantics of the program. The feature can take a program which would previously fail to terminate due to a stack overflow and cause it to terminate without error.

Perhaps TCO is better thought of as a language extension.

Re: When are two proofs essentially the same? (2007)

#77

Post by esrauch »

chongli wrote: post #76
setopt wrote: post #47

Earlier quoted context omitted.

On the other hand, compiler tricks like tail call optimization can e.g. reduce an O(n) algorithm to an O(1) algorithm. Is it a “different program” if the same source code is compiled with a new compiler?

Tail call elimination is not an optimization because it changes the semantics of the program. The feature can take a program which would previously fail to terminate due to a stack overflow and cause it to terminate without error. Perhaps TCO is better thought of as a language extension.

That seems no different than any other optimization: very directly tons of optimizations would reduce stack usage which would then change a given input from a stack overflow to a successful execution. Similarly anything that reduces heap memory usage or code size would also do the same.

Re: When are two proofs essentially the same? (2007)

#79

Post by smfjaw »

qubitly wrote: post #66

Reducing two mathematical proofs to being 'essentially the same' just because they reach the same conclusion overlooks something crucial: each proof isn’t merely a path to a result but a unique expression of understanding. A proof has its own logical and conceptual structure, and that structure isn’t interchangeable without losing some of its inherent value. Comparing proofs shouldn’t just focus on a shared outcome:…

computational reducibility/irreducibility is a big topic in computer science and is incredibly interesting. It allows us to prove that certain "computers" are the same through proofs and that they can carry out the same tasks regardless of the actions that take place within them. I would suggest looking into that as it really opens your eyes to just how similar computationally so many things are

Re: When are two proofs essentially the same? (2007)

#80

Post by chongli »

setopt wrote: post #48
joe_the_user wrote: post #46

Well, if you define a proof system as a series of potential manipulations of a space of true statements, a given proof is a sequence of manipulations and states and thus a path in a sort-of-metric space. Two proofs could said to be similar if their paths are "close" in that sort-of-metric space. Of course, you're left with the question of how close is close and whether "close" means close at one intermediate point or…

It’s also hard to prove that a statement definitely lies in the “space of true statements”. Moreover, whether a proof assumes “A = B” or “B = C” can make them closer together or further apart in such a space depending on whether it is established that “A = C” or not, which also makes it tricky to establish rigorously.

If you haven’t established that A = B and B = C implies A = C then you haven’t proven that = is an equivalence relation on that space including A, B, and C. Unless you’re going to prove it I would go so far as to call it an abuse of notation to continue using = when you mean some other relation where transitivity does not necessarily hold.
Post reply on HN