[Haskell-cafe] Wrong Answer Computing Graph Dominators

[Dan Weston]

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).