FDs and confluence
iavor.diatchki at gmail.com
Thu Apr 13 15:07:53 EDT 2006
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 :-)
More information about the Haskell-prime