Hello,
On 4/12/06, Claus Reinke
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