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

[Fergus Henderson]

On 06-Jan-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> I came away from reading the HAL Herbrand types paper with the
> impression that adding support for delayed goals on Herbrand variables
> makes a fairly insignificant impact on performance and that, therefore,
> when adding Herbrand types to Mercury we might as well make them support
> delay as well.
> 
> It occurs to me now that delayed goals can cause all manner of problems
> in the conditions of if-then-else goals (and negated contexts in
> general.)

Yes.  Special care is needed to handle that properly.

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

So, in grades where trailing is enabled, Mercury will check for
floundering at this point.  Provided that the implementation of delayed
goals is done correctly (as it is in e.g. extras/trailed_update/var.m),
this check will fail, leading to a run-time error.

The check for floundering is done by calling all the function trail entries
for constraints added during the condition of the if-then-else.
When a delayed constraint is posted, it should add a function trail entry.
Whenever Mercury commits to a solution, it will call the function with
a untrail reason of "MR_solve" or "MR_commit" (depending on whether it
is a soft or hard commit).

For more details, see the "Trailing" section of the "C interface" chapter
of the Mercury language reference manual (and you may also want to have
a glance at runtime/mercury_trail.h to get an idea of some more of the
implementation details).

> The goal (not (X /= Y)) also looks like a source of trouble: how should
> constraints posted in a negated context be handled?

Same technique.  This goal should flounder.

> Given that delay has been around for decades, I assume there are
> solutions to these problems so I'd be very grateful if someone could
> someone point me towards a decent paper on the matter.

Several of Lee Naish's papers discuss the notion of floundering.
See in particular [1], and [2] may also be relevant.

The details of how we handle floundering detection in Mercury have
not been documented in any paper yet (but please feel free to write
one that does!).  I think there may perhaps be similar interfaces in
the C interfaces for other Prolog systems that support delayed goals,
such as SICstus Prolog.


References

[1] Negation and Control in Prolog, volume 238 of Lecture Notes in Computer
    Science. Springer-Verlag, Berlin, Germany, September 1986.

[2] @TechReport{flounder,
        Author = { Naish, Lee },
        Title = { A declarative view of floundering},
        Number = { 98/18 },
        Institution = { Department of Computer Science, University of
                Melbourne },
        Address = { Melbourne, Australia },
        pages = {12?},
        Month = {January},
        Year = {1999},
	subcat =  {G4},
	authorcode = {433,13,00,FW,MD,M},
        abstractURL = "http://www.cs.mu.oz.au/~lee/papers/flounder/"
    }

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