FDs and confluence
Iavor Diatchki
iavor.diatchki at gmail.com
Wed Apr 12 21:00:17 EDT 2006
Hello,
I have been trying to follow this discussion, but I cannot quite
understand the problem.
On 4/10/06, Ross Paterson <ross at soi.city.ac.uk> wrote:
> One of the problems with the relaxed coverage condition implemented
> by GHC and Hugs is a loss of confluence. Here is a slightly cut-down
> version of Ex. 18 from the FD-CHR paper:
>
> class B a b | a -> b
> class C a b c | a -> b
>
> instance B a b => C [a] b Bool
>
> Starting from a constraint set C [a] b Bool, C [a] c d, we have two
> possible reductions:
>
> 1) C [a] b Bool, C [a] c d
> => c = b, C [a] b Bool, C [a] b d (use FD on C)
> => c = b, B a b, C [a] b d (reduce instance)
>
> 2) C [a] b Bool, C [a] c d
> => B a b, C [a] c d (reduce instance)
(changed C to B to fix a typo)
It seems to me that the constraint sets {B a b, C [a] b d} and {B a b,
C [a] c d} are equivalent in the sense that if we assume the first set
we can discharge the constraints in the second, and vice versa. So
why are we saying that we have lost confluence? Is there perhaps a
different example that illustrates the porblem?
-Iavor
PS: To show that C [a] b d |- C [a] c d we can apply the improving
substitution 'b=c' (using the FD on class C), and then solve the goal
by assumption, the proof the other way is symmetric.
More information about the Haskell-prime
mailing list