On 18 Apr 2008, at 20:04, Martin Sulzmann wrote:
Let's consider our running example
class D a b | a -> b instance D a b => D [a] [b]
which we can write in CHR notation
D a b, D a c ==> b=c (FD)
D [a] [b] <=> D a b (Inst)
These rules overlap.
I experimented with translations into GNU Prolog (gprolog). Since "=" is hard to get working in Prolog unless integrated into unification, I tried (using the idea of rewriting unique existence as functions, possible if one assumes the axiom of choice): class(d, A, b(A)). instance(d, l(A), l(B)) :- class(d, A, B). Then: ?- instance(d, l(A), l(B)). B = b(A) ?- instance(d, l(A), C). C = l(b(A)) ?- instance(d, l(A), l(B)), instance(d, l(A), C). B = b(A) C = l(b(A)) Though I am not sure about the intended semantics, it does produce unique solutions. Hans