[m-dev.] for review: add `do_while/4' to std_util.m

[Fergus Henderson]

On 20-Oct-1999, Ralph Becket <rbeck at microsoft.com> wrote:
> Just one point...
> 
> > :- pred q(int::out, int::out) is nondet.
> > 
> > q(X, Y) :-
> > 	p(X),
> > 	(if some [Y1] p(Y1) then
> > 		Y = Y1
> > 	else
> > 		Y = 42
> > 	).
> 
> I find the quantification here a tad confusing.  My intuition says that
> the quantification `some [Y1]' has scope just in the condition of the
> if-then-else - which would make `Y1' free in the then clause - but it
> clearly extends into the then clause.

Yes, it does.  We need some special syntax which allows the variable to
scope over the condition and the then, but not the else.
The logical meaning of this `if some [Vars] Cond then Then else Else'
is

	( some [Vars] (Cond, Then)
	; (not some [Vars] Cond), Else
	)

Writing it that way is ugly, because it repeats the condition and the
variables, so we need a special syntax.  The syntax that Mercury uses
was pioneered by NU-Prolog; a similar syntax was also used by Goedel.

> I would write this along the
> lines of
> 
> 	Y = some [Y1] (if p(Y1) then Y1 else 42)

That is a syntax error.  Expressions can't contain quantifiers,
only goals can contain quantifiers.  It doesn't make any sense
for expressions to contain quantifiers.

So you would need to write it as

 	some [Y1] (if p(Y1) then Y = Y1 else Y = 42)
or
 	some [Y1] Y = (if p(Y1) then Y1 else 42)

But even then, that would be a mode error: you are trying to bind
a non-local variable in the condition of an if-then-else, which is
not allowed.  The error arises because this logical formula is different
to the one above.  Logically this would be equivalent to

	some [Y1] (p(Y1), Y = Y1 ; not p(Y1), Y = 42)

which is NOT what you really intend.
That is equivalent to

	(some [Y1] (p(Y1), Y = Y1)) ; (some [Y1] not p(Y1)), Y = 42
	
but it is NOT equivalent to

	(some [Y1] (p(Y1), Y = Y1)) ; (not some [Y1] p(Y1)), Y = 42

because the order of the `not' and the `some' is different.

-- 
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.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------