On Thursday, 7 August 2014 at 16:56:01 UTC, Ola Fosheim Grøstad
wrote:
On Thursday, 7 August 2014 at 16:36:09 UTC, David Bregman wrote:
Right. So if X is false, the axiom we declare is !P, not
"false" or "a fallacy".
But Pn is always true where you assume…?
No. Remember P is "control flow can reach this assume". If the
assume is unreachable, then P is false. The compiler doesn't
always know that P is false though, so we can use assume(false)
to supply that as an axiom.
Here's an example:
x = rand() & 3; // x is 0,1,2 or 3.
switch(x) {
case 0: foo();
case 1: bar();
case 2: baz();
case 3: qux();
default: assume(false); // hopefully redundant with a decent
compiler.
}
now the compiler can optimize this down to
{foo, bar, baz, qux}[x]();
or even better, a computed jump.
False => X is true for any X, so the axiom we declare is just
a tautology.
I don't follow. If any assumption is false then anything goes…
Using my definition of assume, the axiom declared is P=>x. If P
is false, then the axiom declared is false => x, which is true
for any x.
http://en.wikipedia.org/wiki/Truth_table#Logical_implication
So is the control flow definition / unreachability argument
clear now?
Nope.
Ok, is it clear now? If not, which parts are not clear?
