Want to read Slashdot from your mobile device? Point it at m.slashdot.org and keep reading!

 



Forgot your password?
typodupeerror

Comment: Re:prove that the program works (Score 1) 189

by ThanatosMinor (#46280409) Attached to: A Mathematical Proof Too Long To Check

Um, excuse me. If you're going to quote me and change what I said, then indicate your edits. I have done so above, in bold. Not that I can make sense of them.

Sorry, I realized at one point I was editing the quote rather than my own text and thought I fixed it but apparently missed one of my edits and there's no reason it should make sense there. Entirely my fault.

Wha...? That's just plain wrong. I can think up all kinds of invalid proofs of the Pythagorean Theorem. But showing that a proof is invalid does not mean the theorem is incorrect. It just means your proof is.

Double wha...? I never claimed the theory behind the algorithm is incorrect, just that if an algorithm designed to produce correct proofs produces a fautly proof, the algorithm is faulty. If you think up an invalid proof of the Pythagorean Theorem, you're at fault for violating the rules of the system and I don't know why anyone would claim it's a fault of the system itself.

As for the rest, please see my other reply to your first post, relating to specific vs. universal algorithms. The gist is that a specific algorithm can be written to check the validity of this proof, but doing so is functionally equivalent to manual verification, but a universal algorithm to verify all correct proofs is impossible.

I never said that one couldn't produce either an algorithm that generates proofs or one that verifies proofs, but the fact is, since there exist true statements that are unprovable the latter algorithm cannot be universal. It can only check whether the symbols follow its understanding of the rules of manipulation.

I get what you're saying. Since Program A can be written to conform to certain rules, Program B can be written to confirm the output of A conforms to the rules that A was given, so yes the proof can be "verified" that way, but by definition you're still only covering some of the proofs A might generate.

But note that the poster I originally responded to said that the output need not be evaulated, but rather only the generating algorithm. I never even said this was a useless approach, since it will likely converge to a correct result, but it hardly counts as a proof of the result. Checking programming isn't the same as checking output, and checking output isn't the same as proving mathematical validity, though of course it can be the same as proving that what you get is what you expected to get, which may be good enough in many cases but wasn't even what I was originally responding to.

It may be that I'm assigning too much power to the algorithm that generated the proof. While it's impossible to program an algorithm with the axioms of a system and tell it to generate all the valid proofs of the system, and equally impossible to similarly program one to verify all proofs of the system, some smaller tasks (maybe this one) are certainly within the realm of algorithmic possibility. I was thinking of the original poster's comment in a very general context and not just in that of this specific problem.

Comment: Re:prove that the program works (Score 1) 189

by ThanatosMinor (#46279347) Attached to: A Mathematical Proof Too Long To Check
Note also the poster I responded to didn't say prove the algorithm is correct and error-free, but rather that it "works," which means generates a correct proof, the checking of which (probably) invokes the halting problem. I say probably because it's likely no easier to write an algorithm that is designed specifically to check this "proof" for correctness than it is for a mathematician to verify it manually, and therefore it would be verified by a general one designed to verify proofs. The halting problem doesn't apply to the former case since it would involve a single-use algorithm to verify one single input, but it surely applies to the latter.

Comment: Re:prove that the program works (Score 1) 189

by ThanatosMinor (#46279183) Attached to: A Mathematical Proof Too Long To Check
I think the issue here stems from the concept of "correct" and how knowable that value is.

Turing's halting problem is a statement about limitations in the ability of algorithms to examine other algorithms. Again, it doesn't mean you can't prove that an algorithm is correct, no matter how "correct" the algorithm appears.

That's kind of my point. Given this proof, it would show that the algorithm is incorrect if the proof is shown to be invalid, yet the proof is too long to be verified by anything but another algorithm, so the halting problem is definitely relevant in a discussion about algorithm-generated proofs which can't be verified by humans.

Sure, if errors are found in a generating algorithm, then they will be fixed and it will be run again, but that again doesn't show that its "proof" is a real proof without independent verification, which again invokes the halting problem if its proof is horrendously long since what it creates must be evaluated by another algorithm. There is no way to demonstrate that such an algorithm as this generates only correct proofs.

Yes, some proofs can be generated by algorithms and others can be checked by algorithms, but a mathematician is necessary at some point in the process since no non-trivial generating algorithm can be shown to create only correct proofs and no universal checking algorithm can be created which generates no false positives or negatives.

Considering how complex computer systems are, is it even possible to claim that an algorithm can run bug-free enough to consider correctness of code equivalent to verification that its output is correct in any but trivial cases?

Comment: Re:prove that the program works (Score 1) 189

by ThanatosMinor (#46278715) Attached to: A Mathematical Proof Too Long To Check

Prove that the algorithm works. That's your proof.

Gödel and Turing make strong cases that proving the algorithm works for some inputs that are correct proofs doesn't count as proof it will work for all correct proof inputs. So no, even if you "prove the algorithm works" it is not the same as a rigorous mathematical proof.

Comment: Re:Transfer Stations. (Score 1) 240

by ThanatosMinor (#46222637) Attached to: How To Hack Subway Fares Using Fare Arbitrage

Transfering trains in the BART system, aside from timing, is essentially arbitrary. When transfers are timed you sometimes have to wait less time to get on a different train going in the same or opposite direction, but behavior is the same. Only if the train you're getting on is the last one of the night are you required to transfer at one of those stations, and that's only because those are generally the only places they wait. Any other time of day you can transfer anywhere there are two lines together, but it will probably involve waiting. Yes, less waiting than going all the way out of one's way to a transfer station, but still (for many) too much to make the gain worth the effort.

This whole mess would only make any sense at all if timing were just such that one person's train passes another's exit station at just the right time so they could swap cards through the open door, and BART is not that predictable (though it's WAY more so than any local bus system).

Comment: This could maybe be done with one person (Score 1) 240

by ThanatosMinor (#46220305) Attached to: How To Hack Subway Fares Using Fare Arbitrage

Back when I was poor and could barely afford public transportation when I had to use it, I thought about keeping multiple BART tickets I would use to make it look like all my longer-distance trips were actually short-distance ones that just took a long time, but I never implemented my plan. There are plenty of moral issues with stealing from a public service, but truth is those seem less important when you're a teenager with no money, but I think practicality is what ultimately prevented me from doing it.

Even if the system didn't care that a ticket was used to exit on a different day than it was used to enter (this is a big if, since BART is not a 24-hour service, making it easy to prevent such fraud), I would have to label and keep track of so many tickets and carry them with me whenever I wanted to use the train that it was really never worth it. No way was I going to get someone else involved, and the trouble of having to intentionally get off at the wrong stop sometimes was just too much trouble.

A friend of mine would just buy red children's tickets and use an x-acto knife to cut the magnetic stripe off and glue them onto standard adult blue tickets. Still stealing, still wrong, but much easier than anything suggested here.

Comment: Re:Summary named the sattelite wrong... (Score 2) 61

by ThanatosMinor (#46164935) Attached to: Weird Asteroid Itokawa Has a Dual Personality
It's relevant to the article (very un-/.) but the poster probably didn't notice the summary is a quote or read the article (very /.) or he/she/it would have known that Hayabusa is spelled wrong in the source material. It's the journalist's job to spell-check names, not editors here. Their job is to...umm...something something...whatever, I'm sure it's very important.

Comment: How can he even show his face? (Score 1) 190

by ThanatosMinor (#42264739) Attached to: UT Professor Resigns Over Fracking Conflict of Interest
What gets me is that the lead author has claimed (and UT seems to believe) that his conflict of interest had no impact on the quality or findings of the report. This is unlikely, but possible. I won't belabor that point. But the the only other explanation for allowing his name at the top of this nonsense is gross negligence and/or extreme incompetence, either of which should disqualify him from any academic position ever. At this point he is at best a corporate shill, and at worst an unethical idiotic corporate shill.

Comment: Re:Stego (Score 1) 332

by ThanatosMinor (#39878805) Attached to: German Authorities Find Al Qaeda Plans Disguised In Porn
At least in criminal trials, juries are intended to be finders of fact only, which requires no prior experience or knowledge of the relevant laws. The system was designed this way on purpose and is potentially way more equitable than a system in which someone's job/career/reputation is at stake every time he or she reaches a verdict. 12 strangers may be more emotional than a single judge, but in the long run will probably be more fair.

Nobody wants their case to be decided as soon as they find out they have the judge who thinks everyone is guilty.

BASIC is to computer programming as QWERTY is to typing. -- Seymour Papert

Working...