[Haskell-cafe] Wrong Answer Computing Graph Dominators
Dan Weston
westondan at imageworks.com
Fri Apr 18 15:24:59 EDT 2008
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).
More information about the Haskell-Cafe
mailing list