[mercury-users] Confused about "undefined behaviour" of promise_only_solution

[Fergus Henderson]

On 27-Nov-2004, Kral Stefan <skral at mips.complang.tuwien.ac.at> wrote:
> 
> Suppose, I want to write a committed-choice term rewriting system
> (that does not give actual guarantees about the order in which rules
> are tried), can I actually write nondeterministic code and then 
> commit at every step

Yes, you should be able to use Mercury's committed choice nondeterminism
features to do that.

> > [...]
> > Ahh, it sounds as though what you want is user-defined equality.
> > User-defined equality is useful where, say, you want to represent sets
> > using unordered lists.  In this case you would like Mercury to recognise
> > the following identities: [1, 2, 3] = [1, 3, 2] = [1, 1, 3, 1, 2] = ...
> > You can do this by supplying your own equality predicate for your set
> > type.  The reference manual section on this point is typically terse; if
> > you want some help on this aspect of Mercury just ask on the mailing
> > list.
> That sounds very good, and like a lot of work.
> 
> The actual problem is about optimal instruction selection done by
> a special purpose compiler. Defining equality over sequences of
> instructions would require to consider the binding information of
> variables occuring in these sequences. That's a lot of overhead.

Defining equality over sequences of instructions is indeed a hard problem;
if the instruction set is Turing-complete, then it is undecidable.

However, you don't need to actually implement the equality predicate.
It is enough to just declare that the type has a user-defined equality.
Rather than implementing it, you can define it using a stub that just
throws an exception, e.g.

	:- type program ---> program(list(instruction))
		where equality is foo_equality.

	:- pred program_equality(foo::in, foo::in) is semidet.
	program_equality(_, _) :-
		throw("program_equality not implemented").

> Maybe I should reformulate my original question. 
> My applications usually look something like this:
>    p(S0,S) :-
> 	( multipart1(S0,S1) -> true ),	% some CC term-writing
> 	detpart1(S1,S2),
> 	( multipart2(S2,S3) -> true ),	% some DFID for instr. sel.
> 	detpart2(S3,S4),
> 	...,
> 	detpartN(Sn,S).
> 
> Do I have to fundamentally restructure my application to do this
> in Mercury?

If I understand your application description correctly, no.
It could be as simple as

	:- mode p(in, out) is cc_multi.
	p(S0,S) :-
		multipart1(S0,S1),
		detpart1(S1,S2),
		multipart2(S2,S3),
		detpart2(S3,S4),
		...,
		detpartN(Sn,S).

	:- mode multipart1(in, out) is cc_multi.
	:- mode detpart1(in, out) is det.
	:- mode multipart2(in, out) is cc_multi.
	:- mode detpart2(in, out) is det.
	...
	:- mode detpartN(in, out) is det.

-- 
Fergus Henderson                    |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------