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

[Ralph Becket]

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

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