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

81–90 of 111 posts

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

#81

Post by chongli »

esrauch wrote: post #77
chongli wrote: post #76

Earlier quoted context omitted.

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.

How many of those other optimizations reduce stack usage from O(n) to O(1)?

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

#82

Post by pkoird »

justinpombrio wrote: post #45
pkoird wrote: post #39

Earlier quoted context omitted.

I'm responding to your second example simply because it's easy to argue about. I'd say that both proofs that you have presented are equivalent ways of saying that "since when you sum all the numbers from 1 to N you obtain a number that's N(N+1)/2, therefore, it is true that the sum of numbers from 1 to N is N(N+1)/2". Now, this argument may appear trite but do consider that both of your proofs essentially do the same…

If two programs are equivalent, you can typically show that they're equivalent with a sequence of small refactorings. Replace `x + x` with `2 * x`. Inline that function call. Etc. Can you do that with these two proofs? What's a proof that's halfway in between the two? If you can get from one proof to the other with small "refactorings", then I agree that they're fundamentally the same. If you can't---if there's an in…

But can you not? Assume sum, 1..(N+1)/2..N

Have you not actually built the same proof via induction in both cases with one of them starting from the middle and subsequently including left and right terms at a unit away (you actually do it in reverse but the crux still holds)? Such that S[0] gives you (N+1)/2 and S[(N-1)/2] gives you the total sum.

The argument would be like S[i] = (2i-1)(N+1)/2 only you'd be proving it using induction i.e. given S[i-1], finding S[i].

All it ever matters for this problem is that to prove it as such, you somehow have to add up all of the numbers. The "different" proofs you presented are actually the same since for addition, the order of operation does not matter due to associative and commutative properties. A good question would be to see if any of the proofs still remain valid when either of these properties are removed from an operation.

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

#84

Post by samatman »

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:…

But where is the line?

Proof A and Proof A' are identical, except that Proof A says "and therefore" where Proof A' says "and so we see that". Different proofs?

Proof A'' is a faithful translation of Proof A into French, is it now different? Or is it a trivial translation of the same proof into different language?

This is, in fact, the topic of the Fine Article. The layman (myself included) sees easily that proof is something more durable than the exact words chosen, or even the language the proof is written in. Mathematicians (and patzers such as yours truly) will tend to view trivial transformations of a step in a proof, or trivially equivalent tactics, as resulting in the same proof.

What makes such a transformation trivial? Good question.

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

#85

Post by casey2 »

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?

Yes, same source code; different program. The point of compilers is to output a different program that (hopefully) has similar enough I/O but it better suited to the hardware. The program that runs when a human has to adds 1+1 is still largely unknown to us but the source '1+1' isn't.

Why use a new compiler if your program isn't meaningfully changed by it? I'd consider running on two completely different machines to already constitute "meaningfully different"

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

#86

Post by drdeca »

js8 wrote: post #19
drdeca wrote: post #7

Earlier quoted context omitted.

A proof is not a statement that something is true, but a demonstration that it is true. Are you familiar with the proofs-as-programs idea? The uh, something isomorphism? Idr the name. Not all programs that implement a function are the same. When you boil things down to the fundamental steps of the logic you are working on, you needn’t get the same thing. For one thing, it may be that axioms A and B suffice to prove Z…

I think "propositions-as-types" is exactly why we should consider proofs to be the same if they prove the same type. As others have already said, if you want to distinguish between different proofs, it's better to encode those distinctions formally into types (and thus potentially into another mathematical theory).

There are multiple values of type integer? I don’t see why we should truncate the types representing propositions so that they have at most one element each.

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

#87

Post by mentalically »

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…

In the most general case there is no technique that can determine if two programs are equivalent other than running both programs on some set of inputs and verifying that the outputs (after termination) are the same. Every other technique must cut out all possible sources of non-termination to get around the halting problem in order to make the resulting equivalence relation on the set of programs effectively computable and constructively provable.

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

#88

Post by lanstin »

colechristensen wrote: post #69
VirusNewbie wrote: post #64

Earlier quoted context omitted.

Why not make this rigorous and actually quantify how similar proofs are? I assume this could be done.

You would need a rigorous way to encode proofs likely akin to Gödel numbering or at least something related to automated theorem proving and then add on transformation mechanisms and then rigorously prove that all proofs have transforms from one to the other. I strongly assume this would be hard .

Some sort of Hamming distance in Lean proofs perhaps? Seems unlikely to capture the difference in what a person would say are different proofs tho. And even when people say a proof is different from another one there is usually some notion of "according to our current understanding" with the idea that some further result could show that the apparently unrelated results are aspects of some deeper unity.

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

#89

Post by lanstin »

lisper wrote: post #52
VikingCoder wrote: post #41

I was working with a friend writing a paper about the Ship of Theseus, but my friend kept replacing all of my arguments.

I had a similar experience, but my collaborator had a touch of OCD and just kept micro-editing my original draft, each time replacing exactly one word with a different word that had nearly the same meaning. By the end of the process, my collaborator had produced a word-for-word copy of William Shakespeare's "Julius Caesar". It is a remarkable coincidence that my original draft just happened to have the same number of…

I assume this is a joke related to Borges' don Quixote story?

https://news.ycombinator.com/item?id=19143496

Post reply on HN