FDs and confluence

[tom.schrijvers at cs.kuleuven.be]

On Mon, 10 Apr 2006, Claus Reinke wrote:

>> (see the FunctionalDependencies page for background omitted here)
> 
> which seems to ignore much of the discussion of confluence we had here some 
> weeks ago? I thought this list was for communication with the committee, and 
> since the ticket exists, I had been hoping that the
> type class subcommittee would ensure that the wiki would be updated.
> but it seems I have been talking to myself..

Yes, I wondered what had happened to your previous argument for the memo 
constraint.

>> 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
>> => C a b, C [a] c d (reduce instance)
> 
> CHR-alt:
> 
> B a b <=> infer_B a b, memo_B a b.
> memo_B a b1, memo_B a b2 ==>b1=b2.
> 
> C a b c <=> infer_C a b c, memo_C a b c.
> memo_C a b1 c1, memo_C a b2 c2 ==> b1=b2.
> infer_C [a] b Bool <=> B a b.
> memo_C [a] b' c' ==> b'=b.

What's this last rule for? It mentions a b that does not appear in the head of 
the rule. If you mean the rule

 	memo_C [a] b c, memo_C [a] b' c' ==> b = b'.

then it is already subsumed by the more general

 	memo_C a b1 c1, memo_C a b2 c2 ==> b1=b2.


Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be