FDs and confluence

[Iavor Diatchki]

Hello,

On 4/12/06, Claus Reinke <claus.reinke at talk21.com> wrote:
> 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.

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).  I think there would
really be a problem if we could do some reduction and end up with two
non-equivalent constraint sets, then I think we would have lost
confluence.  But can this happen?

> 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 -
I just used this notion of equivalance, becaue it is what we usually
use in logic.  Do you think we should use something else?

> you cannot use constraints from one set to help discharging
> constraints in the other.
I don't understand this, why not?  If I want to prove that 'p iff q' I
assume 'p' to prove 'q', and vice versa.  Clearly I can use 'p' while
proving 'q'.  We must be talking about different things :-)

-Iavor