Your statement is correct as to the future licenses, but might be a little off with respect to the right to terminate. A license is simply a contract. Since you do not have to pay take a license under the GPL, one could argue that there was no consideration for the rights received under the GPL. A one sided contract (one with no consideration) is generally unenforceable, except if a party has detrimentally relied on the contract. So, you might be able to "terminate" the license under the GPL if the person receiving the license has not relied on it.
Godel showed that in any consistent proof system, there are true statements that the system cannot prove. Take for example the statement: "This proof system cannot prove this statement."
This has nothing to do with undecidability, which deals with functions (or sets), not statements. An undecidable function one that no machine can be built to calculate (an undeciable set one which has no decidable function that determines membership of the set).
Also, you forget when trying to prove a statement, there are more options than proving it it true or proving it is false. You can also prove that it can't be proven either way. This has not been done with the P=NP problem.
Define the problem rigidly and I will give you a reduction to the halting problem, easily.
What you are forgeting is that the halting problem is partially solvable. You can easily make a procedure that says "Yes, this program terminates on this input" for any program that does terminate. It would go something like this:
#!/bin/csh #run using: halt file.c input gcc $1 -o program ./program $2 echo "Yes, this program terminates on this input"
You can even get more complex and create a procedure that can say things like "This program doesn't halt for a while (not for 100M cycles)" and even (for particular program/input combinations) "No, this program doesn't terminate on this input"
This procedure would solve the halting problem that most normal (non-CS) people actually care about -- "Damn, I must have a bug in my tree lookup because it isn't halting"
Similarly you can write a procedure that says "Yes this C program is safe" for most programs and "You might want to take a look at this part" for the others.
Slashdot Mirror
Ok, who let the 1L out of their cage?
Your statement is correct as to the future licenses, but might be a little off with respect to the right to terminate. A license is simply a contract. Since you do not have to pay take a license under the GPL, one could argue that there was no consideration for the rights received under the GPL. A one sided contract (one with no consideration) is generally unenforceable, except if a party has detrimentally relied on the contract. So, you might be able to "terminate" the license under the GPL if the person receiving the license has not relied on it.
IAAL. This is not legal advice.
Godel showed that in any consistent proof system, there are true statements that the system cannot prove. Take for example the statement: "This proof system cannot prove this statement."
This has nothing to do with undecidability, which deals with functions (or sets), not statements. An undecidable function one that no machine can be built to calculate (an undeciable set one which has no decidable function that determines membership of the set).
Also, you forget when trying to prove a statement, there are more options than proving it it true or proving it is false. You can also prove that it can't be proven either way. This has not been done with the P=NP problem.
Actually, Pepsico spunoff their resturants off a few years ago. Now they are owned by "TriCon"
But I don't know what you are talking about... Cheetos rule, Tostitos rule, Sun Chips rule and god knows Pepsi rules. Therefore Pepsico rules.
-Lenza
Define the problem rigidly and I will give you a reduction to the halting problem, easily.
./program $2
What you are forgeting is that the halting problem is partially solvable. You can easily make a procedure that says "Yes, this program terminates on this input" for any program that does terminate. It would go something like this:
#!/bin/csh
#run using: halt file.c input
gcc $1 -o program
echo "Yes, this program terminates on this input"
You can even get more complex and create a procedure that can say things like "This program doesn't halt for a while (not for 100M cycles)" and even (for particular program/input combinations) "No, this program doesn't terminate on this input"
This procedure would solve the halting problem that most normal (non-CS) people actually care about -- "Damn, I must have a bug in my tree lookup because it isn't halting"
Similarly you can write a procedure that says "Yes this C program is safe" for most programs and "You might want to take a look at this part" for the others.