[m-dev.] Re: Assocative predicates

[Fergus Henderson]

Hi,

Sorry if anyone gets this twice.  It appears that the time
I sent this out it vanished into the bit bucket, so I'm resending it.

On 20-Apr-1998, Harald Sondergaard <harald at cs.mu.OZ.AU> wrote:
> Fergus Henderson <fjh at cs.mu.OZ.AU> writes:
> 
> >If you're using explicit existential quantification, then the
> >natural thing is to push the quantifiers down into the formula:
> 
> >	:- pragma assert(
> >		some [ABs] (append(As, Bs, ABs), append(ABs, Cs, ABCs)) <=>
> >		some [BCs] (append(Bs, Cs, BCs), append(As, BCs, ABCs))
> >	).
> 
> Care is necessary here.  
...
> I think that you do indeed want the formula as you gave it, but it is
> not right to think of it as a result of "pushing the quantifier in".

Woops, you're right of course.

> >In contrast, if you're using explicit universal quantification,
> >then you'll just use a single quantifier at the top-level:
> 
> >	:- pragma assert(all [As, Bs, Cs, ABCs] (
> >		(append(As, Bs, ABs), append(ABs, Cs, ABCs)) <=>
> >		(append(Bs, Cs, BCs), append(As, BCs, ABCs))
> >	)).
> 
> But then it has to be understood that the intended meaning is the
> formula you gave above.  It seems nicer to simply use that formula.

The intended meaning is version which has *both* universal and
existential quantifiers:

	:- pragma assert(all [As, Bs, Cs, ABCs] (
		some [ABs] (append(As, Bs, ABs), append(ABs, Cs, ABCs)) <=>
		some [BCs] (append(Bs, Cs, BCs), append(As, BCs, ABCs))
	)).

Either of the versions above are abbreviations for this.
In either case, the programmer needs to know what convention
we are using for implicit quantification.
This may be an argument against the use of implicit quantification at all,
but I don't think it is a good argument for implicit universal
rather than implicit existential quantification or vice versa.

When Harald say "It seems nicer to simply use that formula", I think that
Harald is probably just so used to the convention of implicit universal
quantification that he has forgotten that we are using it.
But to someone who does more Mercury or Prolog programming than
they do logic theory, the opposite convention of implicit existential
quantification in goals may seem more natural.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.