Path: utzoo!utgpu!water!watmath!clyde!rutgers!cmcl2!nrl-cmf!mailrus!ames!pasteur!ucbvax!decvax!decwrl!sun!quintus!ok
From: ok@quintus.UUCP (Richard A. O'Keefe)
Newsgroups: comp.lang.prolog
Subject: Re: Programming Quickie
Message-ID: <826@cresswell.quintus.UUCP>
Date: 27 Mar 88 10:29:15 GMT
References: <1600011@otter.hple.hp.com>
Organization: Quintus Computer Systems, Mountain View, CA
Lines: 58

In article <1600011@otter.hple.hp.com>, ijd@otter.hple.hp.com (Ian Dickinson) writes:

> Assume a relation "Y is contained in X", specified as:
> 	contains( ?X, ?Y ).
> Assume also, two global predicates p/1 and q/1. (As is always the case in 
> these problems, p and q are expensive to compute :-).
> The problem is to define a predicate exactly_one/2:
> 	exactly_one( +X, ?Y )
> 	is true if X contains Y,  Y satisfies p/1 and all of the other
> 	Y' contained by X satisfy q/1.

Let's start like this:

	exactly_one(X, Y) :-
		setof(Z, contains(X, Z), Zs),
		p_and_qs(Y, Zs).

This much is straightforward.  In the context of your actual problem, it
may be easy to compute Zs directly.  The tricky thing is p_and_qs.  You
do not say whether it is possible for p/1 and q/1 to be true of the same
term.  There are three cases:
    1.	there is exactly one element Z of Zs for which q(Z) is false and
	p(Z) is true of that Z.  In this case Y=Z.

    2.	q(Z) is true of every element Z of Zs, and p(Z) is true of at
	least one such Z.  This this case, Y is any of the Zs for which p(Y).

    3.	There is no solution for Y.

In order to tell which of the first two cases we've got, we'll write a
predicate to return the longest suffix of Zs whose head does not
satisfy q/1, or the empty list if every element of Zs satisfies q/1.
Then if we get a non-empty list, p must be true of the first element
and q of all the rest.  If we get an empty list, any member of Zs which
satisfies p/1 will do.

	p_and_qs(Y, Zs) :-
		first_non_q(Zs, RestZs),
		p_and_qs(RestZs, Y, Zs).

	first_non_q([Z|Zs], RestZs) :-
		q(Z),
		!,
		first_non_q(Zs, RestZs).
	first_non_q(RestZs, RestZs).		

	p_and_qs([Y|Qs], Y, _) :-
		p(Y),
		first_non_q(Qs, []).
	p_and_qs([], Y, Zs) :-
		member(Y, Zs),
		p(Y).

This checks q(Z) once for each Z, and checks p(Y) either once or once
for each Z unifying with Y.  Without more information about p and q I
don't think this can be reduced.

I have tested this code.  It can solve for X as well as Y.