[deleted]
When are two proofs essentially the same? (2007)
91–100 of 111 posts
Re: When are two proofs essentially the same? (2007)
#92Earlier quoted context omitted.
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
It is a joke, but not related to Borges, at least not intentionally.
Re: When are two proofs essentially the same? (2007)
#93Earlier quoted context omitted.
Asymptotics and stability are different theorems. An algorithm is not a proof. It is a technique for proof. Two algorithms can be different, while not being meaningfully different profs that a list is sortable. To the extent that they are different, they proof different theorems, such as "list can be sorted in O(f) time" for an f of interest.
> An algorithm is not a proof. That is an opinion that many do not share. FWIW, I framed my response as an opinion; you gave yours as a blanket statement. It is not wrong to treat algorithms as valid proofs. In a dependent type theory, propositions are represented as types; the proposition that "all lists can be sorted" could be represented represented as the type "forall (t : Type) -> (le : Ordered t) -> forall (xs…
>> An algorithm is not a proof.
> That is an opinion that many do not share.
Say, we have an algorithm to color a planar graph with 4 colors, can we say that we have a proof for 4-coloring a planar graph?
Re: When are two proofs essentially the same? (2007)
#94Earlier quoted context omitted.
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.
We shouldn't, that's the point! At least not in mathematics, programming is a different story. It's perfectly fine to have type of all integers alongside type of all squares and types that only contain number 1 or number 1729.
Relations of these types will then reflect the relations of their respective proofs. There is no need to consider "proof equivalence" or other kind of proof properties. That's already accomplished by studying types themselves.
The choice of types already reflects what we want to study.
Re: When are two proofs essentially the same? (2007)
#95I 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…
Ahh, the language diffusion model! You start with a word salad and end up with a Shakespeare's play.
Re: When are two proofs essentially the same? (2007)
#96Earlier quoted context omitted.
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) ?
That's irrelevant - your assertion was that a change that changes semantics by preventing stack overflow cannot be called an optimization. The commenter showed that is false, and gave reasons why.
Whether tail call goes from O(n) to O(1) doesn't change any of the above.
Re: When are two proofs essentially the same? (2007)
#97Earlier quoted context omitted.
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.
What I mean is that at the time something is proven, it might not be clear that those assumptions are equivalent. Like assuming at the start of a proof that the Axiom of Choice holds vs that Zorn’s lemma holds. That those two proofs are “close” requires that you know it’s already proven that they are equivalent. In that sense, I believe whether proofs should be considered close or not is more subjective than objective, as it depends on the previous knowledge of the reader.
My point above is that one mathematician might assume A=B and another might assume A=C, and both prove the same things. That doesn’t mean they know that always B=C even if it’s true, in which case it’s hard to say whether the proofs are close.
Re: When are two proofs essentially the same? (2007)
#98I'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.
You've misunderstood the difference of "sameness" those two works are trying to address. Knuth is not using an equivalent idea of "sameness" as discussed above. Two people each going by Philosophy of Computer Science and the Art of Computer Programming exercise notion would not always agree if two programs are "the same".
It's also a bridge too far to make a blanket statement of Knuth "already answered this" (it's also not accurate to attribute that idea to Knuth; e.g. Church did work exactly on this decades before). Meaningful discourse and mathematical analysis requires nuance and degrees of equivalence and mixing them up makes it needlessly confusing and difficult.
Sameness as "same input same output" is NOT the same as the "isomorphic equivalence" which is more difficult, strict, and abstract. In this sense they are the same if they follow the same "steps" (also isomorphic between programs), i.e. they are different representations of the same algorithm.
Re: When are two proofs essentially the same? (2007)
#99Earlier quoted context omitted.
Knuth answers this question in chapter 0.
You've misunderstood the difference of "sameness" those two works are trying to address. Knuth is not using an equivalent idea of "sameness" as discussed above. Two people each going by Philosophy of Computer Science and the Art of Computer Programming exercise notion would not always agree if two programs are "the same". It's also a bridge too far to make a blanket statement of Knuth "already answered this" (it's al…
> same input same output
He doesn’t say this.
> NOT the same as the "isomorphic equivalence" which is more difficult, strict, and abstract.
This is what the exercise is about. So I would recommend reading before making assumptions.
Of course there are more than one definition of equivalence and isomorphism, but the one explored there is just as interesting as the comment I’m replying to.
drpossum you stop with these gotcha posts? This is our 3rd encounter.
Re: When are two proofs essentially the same? (2007)
#100Earlier quoted context omitted.
You've misunderstood the difference of "sameness" those two works are trying to address. Knuth is not using an equivalent idea of "sameness" as discussed above. Two people each going by Philosophy of Computer Science and the Art of Computer Programming exercise notion would not always agree if two programs are "the same". It's also a bridge too far to make a blanket statement of Knuth "already answered this" (it's al…
> same input same output He doesn’t say this. > NOT the same as the "isomorphic equivalence" which is more difficult, strict, and abstract. This is what the exercise is about. So I would recommend reading before making assumptions. Of course there are more than one definition of equivalence and isomorphism, but the one explored there is just as interesting as the comment I’m replying to. drpossum you stop with these…
I hadn't noticed, but it's a free board.