FDs and confluence

[Claus Reinke]

>> there is no implication that d=Bool (you could add: 
>> 'instance B a b => C [a] b Char' without violating
>> FD consistency).
> 
> These instances (alpha-renamed):
> instance B a1 b1 => C [a1] b1 Bool
> instance B a2 b2 => C [a2] b2 Char
> 
> violate the consistency condition: a substitution that unifies a1 and
> a2 need not unify b1 and b2, because the consistency condition makes
> no mention of the contexts.  (If it did, the instance improvement rule
> would be invalid.)

??
the consistency condition does mention b1 and b2 as t_b and s_b, so 
any substitution that unifies a1 and a2 (t_a and s_a) needs to unify b1 
and b2, independent of context.

note also that we are talking about different things here: I am talking about
FD consistency, you are talking about the FD consistency condition.

let's be concrete:

    class B a b | a -> b
    class C a b c | a -> b

    instance B a1 b1 => C [a1] b1 Bool
    instance B a2 b2 => C [a2] b2 Char

with these declarations, you are concerned about constraints
C [a] b Bool,C [a] c Char, which you claim are substitution instances
of these declaration heads even if b and c differ. but the class instances
of class C are constrained by an FD, and if b and c differ, these two
constraints are _not_ substitution instances under that FD. they would
be substitution instances if that FD wasn't there (*).

the FD consistency condition is an approximation of FD consistency,
and it is a strange approximation at that, because it is neither sufficient
nor necessary (with the alternative CHR translation) for consistency:

- if all instance declarations fulfill the FD consistency condition, the
    constraint store may still be inconsistent, because it may represent
    an inconsistent query; so the condition is not sufficient

- one of the bonuses of a confluent CHR is that deductions on
    inconsistent stores will not terminate successfully (if they terminate, 
    they are certain to fail), so the condition is not necessary, either
    [it was with the old translation, though]

as this example shows once again, there are instance declarations 
for which the FD consistency condition, as currently interpreted by 
Hugs, fails, even though no inconsistent constraints are implied. so I 
fail to see the point of continuing to require the FD consistency
condition in unrevised form.

but my point was that there is no confluence problem. everything
else, with the exception of termination, follows from there.

cheers,
claus


(*) this is similar to patterns and guards in the expression language,
    for instance:

    f a = .. -- some function

    c [a1] b1 Bool | b1 == f [a1] = b a1 b1
    c [a2] b2 Char | b2 == f [a2] = b a2 b2

    now, c [a] b1 Bool and c [a] b2 Char are defined if (b1==f [a])
    and (b2==f [a]) and if b a b1 and b a b2 are defined as well.
    c [a] d Bool with (d/=f[a]) matches the pattern, but fails the 
    guard, so it is not a substitution instance of c's left hand sides
    under the guard.