Matthew Brecknell wrote:
Dan Weston wrote:
Here, "any path" means all paths, a logical conjunction:
and [True, True] = True and [True ] = True and [ ] = True
Kim-Ee Yeoh wrote:
Hate to nitpick, but what appears to be some kind of a limit in the opposite direction is a curious way of arguing that: and [] = True.
Surely one can also write
and [False, False] = False and [False ] = False and [ ] = False ???
No. I think what Dan meant was that for all non-null xs :: [Bool], it is clearly true that:
and (True:xs) == and xs -- (1)
It therefore makes sense to define (1) to hold also for empty lists, and since it is also true that:
and (True:[]) == True
We obtain:
and [] == True
Since we can't make any similar claim about the conjuctions of lists beginning with False, there is no reasonable argument to the contrary.
Also, (and I know none of this is original, but it's worth repeating...) It is not just the definition of "and" at stake here. Logical propositions that extend painlessly to [] if (and [] == True) become inconsistent for [] if (and [] == False) and would have to be checked in program calculation. For instance, in propositional logic, you can prove (using Composition, Distribution[2], Material Implication) that for nonnull ys = [y0,y1,..,yn], implying everthing implies each thing: x -> (y0 && y1 && ... yn) <--> (x -> y0) && (x -> y1) && ... && (x -> yn) Writing this in Haskell and using the fact that x -> y means (not x || y), this says that not x || and ys == and (map (not x ||) ys) or in pointfree notation: f . and == and . map f where f = (not x ||) This should look familiar to origamists everywhere. "and" can be defined in terms of foldr iff (and [] == True) [Try it!]. Why is this important? If and is defined with foldr, then the above can be proven for all well-typed f, and for f = (not x ||) in particular, even if ys is null. The law is painlessly extended to cover the null case automatically (and is therefore consistent): LHS: not x || (and []) == not x || True == True RHS: and (map (not x ||) []) == and [] == True Therefore True |- True, an instance of x |- x If (and [] == False), then the law becomes inconsistent: LHS: not x || (and []) == not x || False == not x RHS: and (map (not x ||) []) == and [] == False Since not x == False, then x == True Therefore, True |- x ==> -| x (everything is derivable) so we would have to exclude the null case for this law (and many others). Uck! Better stick with (and [] == True) Naturally, similar reasoning justifies (or [] == False).