FDs and confluence

[Claus Reinke]

that's why Ross chose a fresh variable in FD range position:
in the old translation, the class-based FD improvement rule no 
longer applies after reduction because there's only one C constraint
left, and the instance-based FD improvement rule will only instantiate  
the 'b' or 'c' in the constraint with a fresh 'b_123', 'b_124', .., 
unrelated to 'b', 'c', or any previously generated variables in the
constraint store.

hth,
claus

another way to interpret your message: to show equivalence of 
the two constraint sets, you need to show that one implies the 
other, or that both are equivalent to a common constraint set - 
you cannot use constraints from one set to help discharging
constraints in the other. 

>         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.
_______________________________________________
Haskell-prime mailing list
Haskell-prime at haskell.org
http://haskell.org/mailman/listinfo/haskell-prime