FDs and confluence
tom.schrijvers at cs.kuleuven.be
tom.schrijvers at cs.kuleuven.be
Mon Apr 10 14:45:34 EDT 2006
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
More information about the Haskell-prime
mailing list