Hello, On 4/12/06, Claus Reinke <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
