[Haskell-cafe] Wrong Answer Computing Graph Dominators
Kim-Ee Yeoh
a.biurvOir4 at asuhan.com
Sat Apr 19 14:11:31 EDT 2008
Dan Weston wrote:
>
> f . and == and . map f
> where f = (not x ||)
>
> 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:
>
-- snipped --
Yes, the natural way of defining and [] is, well, natural in more
than one sense of the word.
I initially had a hard time grasping what you meant with the
3 equations that started this discussion. I was sure
you meant something other than what I thought, but I couldn't
work it out. I'm glad Matt Brecknell came to the rescue.
Before I would've merely relied on a monoidal identity argument
like the one Chris had presented. Appealing to uniformity (a la
parametric polymorphism) definitely looks sexier. All the cool kids
seem to be doing it.
--
View this message in context: http://www.nabble.com/Wrong-Answer-Computing-Graph-Dominators-tp16714477p16786100.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
More information about the Haskell-Cafe
mailing list