[m-dev.] Quantifiers ...

[Fergus Henderson]

Michael David WINIKOFF, you wrote:
> 
> Can someone point me at an example of a Mercury program containing "all"?

Here's a simple example:

	string_is_upper(String) :-
		all [C] string__contains_char(C) => char__is_upper(C).

> Is it the case that "all [X] p(X)" can never be compiled?

Only if `p' has mode `unused' (free -> free)... but those examples
aren't very useful.

> [It's defined to be "not (some [X] (not p(X)))" and p(X) can't bind X since
>  it's in a negation]

Universal quantification is generally useful only when used with
implication.  The above example is equivalent to

	string_is_upper(String) :-
		not (some [C] (not (not
			(string__contains_char(C), not char__is_upper(C))))).

and it is mode-correct because the double negation is (must be, according
to the language reference manual) eliminated before mode checking.

-- 
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.