Re: More, on backtracking problem..

[td@almeria.inria.fr (Thierry Despeyroux)]

In article <44605@sophia.inria.fr>, brad@cs.adelaide.edu.au (Bradley Alexander) writes:
|> ...
|> Next I press the "step" button and instead of redisplaying the 
|> first rule with "fail" in the status panel the debugger behaves as
|> if I have pressed go and another potential solution is found
|> because it makes four attempts (on this particular program) to find
|> the solution (I'm able to tell because I've inserted write() statements 
|> in my typol definition).
|> 
|> If I press fail when the first rule is displayed then the program
|> fails without attempting any other rules.
|> 
|> Is it possible that there could be some feature in the definition of
|> the rule handling the "let" that causes this behaviour (The debugger
|> is usually very reliable).

The problem comes from two different places:
-the error recovery implementation (I think it is correct, but
 needs some explanations)
-a typol debugger bug(!) that araises during error recovery.
(Were are on April 1st, but sadly this is not a joke)
(Here it is a custom to joke a lot this day)

-1- error recovery implementation

Let's take an example and try to be clear...

set P is
judgement |- L;

R1: |- ... ;

R2: |- ... ;

error recovery

E1: |- ... ;

E2: |- ... ;
end P;

This is equivalent to

set P' is
Pnorm(|- ...)
--------------
|- ... ;

not(Pnorm(|- ...) & Prec(|- ...)
-------------
|- ... ;
end;

where Pnorm contains the rules R1 and R2,
and Prec the error recovery rules.
The same mechanism is used inside the error recovery part
so E2 may be used only if not E1.

This is for the semantics. Now the implementation. How to
implement the negation in a safe way?

1- I can't use a cut, since when Pnorm succeeds I want to
cut the error recovery part, but allow baktracking using the
regular rules. So I prefered a soft_cut.
2- If the proof of Pnorm is not complete (i.e. they are some
delayed goals in this proof) I have to wait until this goals are
woken and proved before executing the soft_cut. This is the case
when a dynamic type-checking occurs on a variable inside the proof
of Pnorm, but this variable is instantiated latter. This may be
also the case if one use the logic preprocessor of MU-Prolog or
something equivalent. The problem is that I don't know how to
implement this with MU-Prolog.
3- So instead of doing that I execute the soft_cut just when the
proof of Pnorm is completed, but check that there are not new
delayed goals during this proof, and emit an error message if this
is not the case.
4- Nothing is done in MU-Prolog to handle the list of delayed goals,
so I have done it myself and the result is very inefficient.
5- I decided that error recovery may be inefficient (the user will
not complain about it), but regular rules must be efficient.
6- So I use an explicit negation not(Pnorm(|- ...), checking that
there is no delayed goals if Pnorm succeeds inside P', and 
soft_cuts (with the same check) inside Prec. So regular rules are
executed at full speed, and only error recovery is slow.

This explain why, when regular rules fail, there is two attempt to
prove Pnorm. And if these rules perform side effects, these side
effects are done more than once. 

If you want to produce error messages and have problems with
backtracking, the easier way is to construct a list of error
messages and emit this list where you are convienced that
there no backtrcking, or return this list as the result of
your Typol program.

2-2 

Now the problem with the debugger. When the negation is performed,
if Pnorm succeeds, you already know it. Your are backtracking not
because there is a failure inside Pnorm but somewhere else, and
the recovery rules will not be used. So you dont want to
see the proof again. If Pnorm fails, you already know that, and
dont want to see this again, but directly go and see if a recovery 
rule is used. So I tried to hide the negation with the debugger, but
obviously, I failed.

I will try to improve the debugger in the futur. This is not easy
since there is more than one prolog clause for one typol rule.

If you want to test/debug your program, without the error recovery
mechanism, you can use
export withoutrecovery(...) as ...;


If you want you can redefine the following prolog predicate that is
in centaur/sources/prolog/pl/typol.pl:
Put it in foo.pl,
then in centaur your type
(prolog)
[-'foo.pl'].
^D

standard definition:

$warn_not(P) :-
	$symbol(debug_hide, S),
	lispcall(0,0,S,_),
	pusharg(3,'Try'),
	$symbol('d-p-s',DPS),
	lispcall(3,1,DPS,_),
	not ($get_sleeping_goals(A), P, 
	     $get_sleeping_goals(B), $warn_delay(A, B, negation)),
	pusharg(3,'Proved'),
	lispcall(3,1,DPS,_).

a version that will not try to hide the negation when debugging
and will not change the behaviour:

$warn_not(P) :-
	not ($get_sleeping_goals(A), P, 
	     $get_sleeping_goals(B), $warn_delay(A, B, negation)).

And to check that redondant side effects come from negation
(but the semantics will be drastically changed because recovery
rules may always apply):
$warn_not(P).


I hope that this will help you.

Thierry.

-- 
Send contributions and compliments to centaur@sophia.inria.fr. Registration
and administrative matters should be sent to centaur-request@sophia.inria.fr.
+---------------------------------------------------------------------------+
|     Thierry Despeyroux      | email: Thierry.Despeyroux@sophia.inria.fr   |
| I.N.R.I.A. Sophia-Antipolis | phone: +33 93 65 77 07 fax: +33 93 65 77 66 |
+---------------------------------------------------------------------------+