FDs and confluence

[Iavor Diatchki]

Hello,

> > I understand the reduction steps.  Are you saying that the problem is
> > that the two sets are not syntactically equal?   To me this does not
> > seem important: we just end up with two different ways to say the same
> > thing (i.e., they are logically equivalent).
>
> If c were mentioned in another constraint, they would not be equivalent.

How so?  A concrete example would really be useful.  I think that the
constraint 'C [a] b d' and 'C [a] c d' are equivalent and I don't see
how the rest of the context can affect this (of course I have been
wrong in the past :-).  The one way to see that is (like I already
said) --- assume the one and prove the other and vice versa.

Another way to see that is as follows:   All the instances of 'C' that
have '[a]' in their first argument must have the same type in the
second argument otherwise the functional dependecy of 'C' will be
violated. Thus 'b' and 'c' above happen to be just different names for
the same thing.

Yet another slightly different way to think of this is that a
functional dependency is a function on types (e.g., associated type
synonyms give us a way to name this function). So lets say that the
functional dependecy on 'C' is called 'F'.  Than we can see that both
'C [a] b d' and 'C [a] c d' are really the same thing, namely 'C [a]
(F [a]) d'.

-Iavor