6nov07 BOTTOM LINE (at the top) A summary of all that goes on below is the following: For boolean-valued q,r: (if p then q) <=> (if p then q else true) <=> (p implies q) <=> (not p or q) (if p then q else r) <=> (p and q or not p and r) For non-boolean-valued q,r: (if p then q) = (if p then q else nil) Note that for non-boolean-valued q and r, the boolean <=> operator does not work, so we use the all-type = operator. 14mar06 RE-REVELATION: I'm back again to the notion that "if p then q" <=> "p and q" is monstrously counter-intutive for boolean p and q, since what we want in that case is "if p then q" <=> "p implies q". The reason is that we want the "don't care" behavior of "p implies q", as in forall (i in [1 .. #r-1]) if r[i].last = r[i+1].last then ... which is the logic for sub-sorting. 8dec05 REVELATION: The entire following discussion is fucked up. The bottom line should be that "if p then q" is NOT equiv to "p => q", but to "if p then q else nil", which is equiv to "p and q or not p and nil", which is equiv to "p and q or nil" which is equiv to "p and q". The claimed undesirability of "if p then q" not being equiv to "p => q" is actually quite wrong-headed. E.g., in Lisp, "(if p q)" is indeed equiv to "(and p q)" for boolean-valued p and q. So, again, the bottom line is that we have a fully uniform treatment of "if p then q" as "if p then q else nil", for p and q of any type, including boolean. To get logical implication out of if-then-else, we use the form "if p then q else t". This form does in fact have the same truth table as "p => q". See ./if-then-else-truth-table.el for some code. FUCKED UP DISCUSSION STARTS HERE The goal here is to get a sensible truth table for if-then and if-then-else for values of all types. The crux of the problem is that the elseless form must have a sensible meaning when the then clause is non-boolean valued. There are a couple alternatives we can choose: (1) have "if x then y" be equivalent to "if x then y else nil" for all values of x and y, including boolean; (2) have "if x they y" be equivalent to "x => y" for boolean-valued y and equivalent to "if x then y else nil" for non-boolean-valued y. The conclusion is that we have chosen (2), as explained and rationalized in the followig discussion. The problem with (1) is that it leads to what I believe is the highly counterintuitive situation where "if x then y" is NOT equivalent to "x implies y" for boolean-valued y, but rather is equivalent to "x and y". The problem with (2) is that it makes elseless if-then effectively overloaded by providing two different interpretations, one for boolean-valued y and another for non-boolean-valued y. Of these two problems, I consider the first to be the more severe, meaning therefore that we'll opt for alternative (2) in RSL. The rationale to mitigate the problem with alternative (2) goes as follows. For boolean-valued y, "if x then y" has a perfectly sensible interpretation as "x implies y". For non-boolean-valued y, "x implies y" does not have a sensible interpretation since implies requires two boolean-valued arguments. Therefore, we must provide a meaningful interpretation of "if x then y" in the case of non-boolean-valued y. Now, if this sensible interpretation happened to yield a serendipitously uniform result for both boolean- and non-boolean-valued y, that would be nice. Unfortunately, this turns out not to be the case. In the end, I believe the heart of problem is what is viewed by some to be the counterintuitive truth table for implication plus the semantic baggage we bring to what we think should be the formal logic interpretation of the phrase "if x then y". Be that as it may, I am convinced that solution (2) above is the correct one for RSL, and we therefore go with it. What follows is a complete logical analysis of the problem and why we end up with the chosen solution. Consider the p=>q truth table and equivalent and/or form: p q p => q not p or q ======================================== 0 0 1 not 0 or 0 = 1 0 1 1 not 0 or 1 = 1 1 0 0 not 1 or 0 = 0 1 1 1 not 1 or 1 = 1 Consider also the truth table for iff and the equiv and/or form: p q p iff q (p => q) and (q => p) (not p or q) and (not q or p) ========================================================================================= 0 0 1 0 => 0 and 0 => 0 = 1 ( 1 or 0) and ( 1 or 0) = 1 0 1 0 0 => 1 and 1 => 0 = 0 ( 1 or 1) and ( 0 or 0) = 0 1 0 0 1 => 0 and 0 => 1 = 0 ( 0 or 0) and ( 1 or 1) = 0 1 1 1 1 => 1 and 1 => 1 = 1 ( 0 or 1) and ( 0 or 1) = 1 Based on this, we can postulate a sensible logical definition of "if p then q else r" to be "p and q or not p and r", for boolean-valued q and r. The truth table looks like this: p q r if p then q else r <=> p and q or not p and r ====================================================================== 0 0 0 0 0 and 0 or not 0 and 0 = 0 0 0 1 1 0 and 0 or not 0 and 1 = 1 0 1 0 0 0 and 1 or not 0 and 0 = 0 0 1 1 1 0 and 1 or not 0 and 1 = 1 1 0 0 0 1 and 0 or not 1 and 0 = 0 1 0 1 0 1 and 0 or not 1 and 1 = 0 1 1 0 1 1 and 1 or not 1 and 0 = 1 1 1 1 1 1 and 1 or not 1 and 1 = 1 For non-boolean valued q and r, the following truth table works: p q r if p then q else r <=> p and q or not p and r ====================================================================== 0 x y y 0 and x or not 0 and y = x 1 x y x 1 and x or not 1 and y = y This is workable because we can force a boolean-valued result of 0 for an expression of the form "0 and x", since "0 and x" = 0 forall x. Now we must postulate a sensible logical def of the elseless form "if p then q". At the if-then-else level, the definition can be "if p then q else nil". In order to obtain a truth-table for this, we must give a boolean interpretation for the value nil, in particular for nil as the argument of logical and. Based on established RSL semantics, the value of "x and nil" is false, for all x. Given these definitions, we get the following truth table for boolean-valued elseless if-then: p q if p then q <=> p and q or not p and nil ================================================================== 0 0 0 0 and 0 or not 0 and 0 = 0 0 1 0 0 and 1 or not 0 and 0 = 0 1 0 0 1 and 0 or not 1 and 0 = 0 1 1 1 1 and 1 or not 1 and 0 = 1 But this is the truth table for logical and, which means that we have arrived at the highly counterintuitive definition of "if p then q" <=> "p and q". Another way to look at this is to say that "if p then q" <=> "(p and q) or nil, which has a truth table like this: p q if p then q <=> (p and q) or nil ======================================================================= 0 x nil (0 and x) or nil = nil 1 x x (1 and x) or nil = x or nil = x If we interpret "x or nil" to be "x forall x", this is the same result, since "(p and q) or nil" <=> to "(p and q) or false" <=> "p and q". If we interpret "x or nil" to be nil, then this truth table doesn't work at all. Either way, the point is that the uniform interpretation of "if p then q" as "if p then q else nil" does NOT yield the boolean interpretation that we'd like, namely "if p then q" <=> "p => q". One more bit to add here is based on the recent (dec04) revelation that the truth table for "if x then y", aka, logical implication, is in fact equivalent to "if x then y else true", as discussed in the 9dec04 entry in imple-notes. Hence, the very idea that elseless if-then might be be equivalent to "if x then y else false" is just plain off the mark. We can prove this as follows, p => q <=> if p then q else true <=> p and q or not p and true -- by above equivalence def <=> p and q or not p -- by (x and true = x) Here's the truth-table proof of the last line: p q p => q <=> p and q or not p ======================================================================= 0 0 1 0 or 1 = 1 0 1 1 0 or 1 = 1 1 0 0 0 or 0 = 0 1 1 1 1 or 0 = 1 From a purely mathematical perspecitive, an argument can be made that nil is questionable as a genuine boolean value. We have made "nil = false" for essentially traditional operational reasons, as is done in Lisp and C. However, from a mathematical perspective, and even an operational perspective, we could consider nil as something distinct from either true or false, such as the traditional mathematical "undefined" or Icon's "failure". From this perspective, the truth table for boolean-valued elseless if-then is as follows: p q if p then q <=> p and q or not p and nil ================================================================================================== 0 0 0 0 and 0 or not 0 and nil = 0 or (1 and nil) = questionable 0 1 0 0 and 1 or not 0 and nil = 0 or (1 and nil) = questionable 1 0 0 1 and 0 or not 1 and nil = 0 or (0 and nil) = 0 for sure 1 1 1 1 and 1 or not 1 and nil = 1 or (0 and nil) = 1 for sure The last two rows in the table can be considered for sure since we can safely say "0 and x" = 0 forall x, and "1 or x" = 1, forall x. The first two can be considered questionable since "1 and nil" might well yield nil instead of 0, which means "undefined" instead of false. This doesn't really resolve things whoely satisfactorily, since I'm pretty hard-pressed to call "1 and nil" true. However this truth table does bring to light the fact that the difference between interpreting elseless if-then as "and" vs "=>" is questionable in exactly the places where the "and" vs "=>" truth tables differ. In one last vein attempt at a boolean-valued interpretation for if-then we could try the equivalence of "if p then q" <=> "(p and q) or true", but this yields the brain-damaged truth table of: p q if p then q <=> (p and q) or true ========================================== 0 0 0 and 0 or 1 = 1 0 1 0 and 1 or 1 = 1 1 0 1 and 0 or 1 = 1 1 1 1 and 1 or 1 = 1 So, we have arrived at the original decision point -- (1) choose a uniform interpretation of elseless if-then which leads to a counterintuitive meaning in the boolean-valued case, or (2) choose separate boolean- and non-boolean-valued interpretations for elseless if-then. As noted at the outset, the decision is (2). To give us some reassurance that we've chosen the right logic for if-then-else, here are truth tables for some alternative formulations, in the form of "p => q and not p => r", "p => q or not p => r", and "p => q xor not p => r", none of which gives a good result: p q r if p then q else r <=> p => q and not p => r ====================================================================== 0 0 0 0 0 => 0 and not 0 => 0 = (1 and not 1) = 0 1 and not 1 1 and 0 = 0 0 0 1 1 0 => 0 and not 0 => 1 = (1 and not 1) = 0 1 and not 1 1 and 0 = 0 0 1 0 0 0 => 1 and not 0 => 0 = (1 and not 1) = 0 1 and not 1 1 and 0 = 0 0 1 1 1 0 => 1 and not 0 => 1 = (1 and not 0) = 0 1 and not 1 1 and 0 = 0 1 0 0 0 1 => 0 and not 1 => 0 = (0 and not 0) = 0 0 and not 0 0 and 1 = 0 1 0 1 0 1 => 0 and not 1 => 1 = (0 and not 1) = 0 0 and not 1 0 and 0 = 0 1 1 0 1 1 => 1 and not 1 => 0 = (1 and not 0) = 1 1 and not 0 1 and 1 = 1 1 1 1 1 1 => 1 and not 1 => 1 = (1 and not 1) = 0 1 and not 1 1 and 0 = 0 p q r if p then q else r <=> p => q or not p => r ====================================================================== 0 0 0 0 0 => 0 or not 0 => 0 = (1 or not 1) = 1 0 0 1 1 0 => 0 or not 0 => 1 = (1 or not 1) = 1 0 1 0 0 0 => 1 or not 0 => 0 = (1 or not 1) = 1 0 1 1 1 0 => 1 or not 0 => 1 = (1 or not 0) = 1 1 0 0 0 1 => 0 or not 1 => 0 = (0 or not 0) = 1 1 0 1 0 1 => 0 or not 1 => 1 = (0 or not 1) = 0 1 1 0 1 1 => 1 or not 1 => 0 = (1 or not 0) = 1 1 1 1 1 1 => 1 or not 1 => 1 = (1 or not 1) = 1 0 0 0 0 0 => 0 xor not 0 => 0 = (1 xor not 1) = 1 0 0 1 1 0 => 0 xor not 0 => 1 = (1 xor not 1) = 1 0 1 0 0 0 => 1 xor not 0 => 0 = (1 xor not 1) = 1 0 1 1 1 0 => 1 xor not 0 => 1 = (1 xor not 0) = 0 1 0 0 0 1 => 0 xor not 1 => 0 = (0 xor not 0) = 1 1 0 1 0 1 => 0 xor not 1 => 1 = (0 xor not 1) = 0 1 1 0 1 1 => 1 xor not 1 => 0 = (1 xor not 0) = 1 1 1 1 1 1 => 1 xor not 1 => 1 = (1 xor not 1) = 1