[HAL-dev] Re: [m-dev.] Delayed goals and if-then-else goals

[Fergus Henderson]

On 07-Jan-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Fergus Henderson, Wednesday,  7 January 2004:
> > On 06-Jan-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > 
> > > Consider the following goal, where X and Y are unbound variables
> > > belonging to a Herbrand type and /= is implemented by posting a
> > > constraint (i.e. a delayed goal) in the case that either of X or Y is
> > > not bound.
> > > 
> > > 	( if X /= Y then false else X = Y )
> > > 
> > > The denotational semantics of this is
> > > 
> > > 	( X /= Y, false ; not (X /= Y), X = Y )
> > > 
> > > However, the operational semantics in Mercury are different in this
> > > case: the condition is only tested once, hence the if-then-else as a
> > > whole will fail rather than succeed unifying X and Y as per the
> > > denotational reading.
> > 
> > That operational semantics would indeed be unsound.
> > So a conforming Mercury implementation can't do that.
> > 
> > The right thing for an implementation to do at this point
> > is to _flounder_; that is, to report a run-time error or exception.
> > Well, it is possible that there might be better alternatives,
> > but this is at least the best current practice.
> 
> Just to fill the group in on an explanation from Fergus: if the
> condition of an if-then-else succeeds, posting some constraints along
> the way, then it must be the case that those constraints are
> *necessarily* true before the then-goal is tested.  If they are only
> *possibly* true then the implementation should flounder (i.e. halt with
> an error.)

Actually, on further discussion, it turns out to be a bit more subtle.

The first requirement is that if the condition of an if-then-else adds
any constraints which are not provably satisfiable, then the computation
should flounder.  And we do implement that correctly.

But that's not sufficient.  In the example Ralph posted above, the
constraint "X /= Y" is provably satisfiable.

There is an additional requirement, namely that if the condition of an
if-then-else adds *any* constraints on *non-local* variables, then it
should get a mode error [*]; condition of an if-then-else is never allowed
to bind non-local variables, and adding a constraint is the same thing in
this context.

Currently we do not implement this additional requirement properly.
For example:

	:- module v.
	:- interface.
	:- import_module io.

	:- pred main(io__state::di, io__state::uo) is det.

	:- implementation.
	:- import_module var.

	main -->
		{ var__init(A) },  
		( { A = var(42) } ->
			{ Result = "foo" }
		;
			{ Result = "bar" }
		),
		print(Result), nl.

Here, logically there should be two valid solutions to the if-then-else,
but the Mercury implementation does not report any mode error, determinism
error, or run-time error, and computes only the first solution ("foo"),
not the second one ("bar").

It might be acceptable to report the problem as a run-time (dynamic)
mode error, a.k.a. floundering, rather than a compile-time mode error.
But currently we don't even do that.  The mode system is for some reason
not complaining about the possibility that A (which has inst `any')
might get bound in the condition of the if-then-else.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- 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
--------------------------------------------------------------------------