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).
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
