Re: Problems with TYPOL

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

In article <39972@sophia.inria.fr>, jperez@lsi.upc.es (Javier Perez) writes:
|> 
|> 
|> Hello
|> 
|> We are using TYPOL to implement a complex type checker. For us is unavoidable 
|> to have some kind of negation in order to save hundreds of lines of code.
|> 
|> Recently we have built an strategy to simulate negation taking advantadge of
|> the recovery rules. To make a predicate and its negation we make a predicate
|> that always succeeds and returns a value . If the predicate applies we
|> make the predicate return a 1, and if not a 0.
|> 
|> To do this we implement predicate with the same rules that would have normally,
|> and in these rules we return a one, then we put a recovery rule (the most 
|> general rule) that returns a 0. I have enclosed an example that will
|> show this more clearly.
|> 
|> The problem is that under certain circumstances this doesn't work, sometimes
|> the program stops in the half of the execution as if it would have finished
|> normally.

I have tried your example assuming that you run it in debug mode.
The execution is correct, but there is a bug in the debugger that makes
it skip to the end. You can see this printing some results. R1 is 1
and R2 and R3 are 0.

equal_sets(|- set_i[int 4, int 5], set_i[int 5, int 4] : R1)  &
equal_sets(|- set_i[int 4], set_i[int 5, int 4] : R2)  &
equal_sets(|- set_i[int 4, int 5], set_i[int 5] : R3)
----------------
|- GLI : GLI ;
         do writeln(R1)  &  writeln(R2)  &  writeln(R3);

However, in this example you need only one rule for recovery as you don't need
to negate includes_set and belongs_set to negate equal_sets. 

program testrec is
use test;
-- Test for recovery rules.
import diff(_, _) from prolog;

export test_recovery(|- T : T2) as testrec(T) = T2 ;

   set test_recovery is
   judgement |- test : test;

   equal_sets(|- set_i[int 4, int 5], set_i[int 5, int 4] : R1)  &
   equal_sets(|- set_i[int 4], set_i[int 5, int 4] : R2)  &
   equal_sets(|- set_i[int 4, int 5], set_i[int 5] : R3)
   ----------------
   |- GLI : GLI ;
   end test_recovery;

   set equal_sets is
   judgement |- SET, SET : INT;

   -- Returns 1 if both sets contain the same elements and 0 if not. 
   includes_set(|- SET, SET2)  &  includes_set(|- SET2, SET)
   ----------------
   |- SET, SET2 : int 1 ;

   recovery
      |- X, Y : int 0 ;
   end equal_sets;

   set includes_set is
   judgement |- SET, SET;

   |- set_i[], SET2 ;

   belongs_set(|- ELT, SET2)  &  |- ELTR, SET2
   ----------------
   |- set_i[ELT.ELTR], SET2 ;
   end includes_set;

   set belongs_set is
   judgement |- INT, SET;

   |- ELT, set_i[ELT.ELTR] ;

   diff(ELT, ELT2)  &  |- ELT, ELTR
   ----------------
   |- ELT, set_i[ELT2.ELTR] ;
   end belongs_set;
end testrec;

I don't know why the debugger works correctly with these rules!

If for some reason you need to negate also includes_set, for example, I would prefer
to have a second judgement:

   set includes_set is
   judgement |- SET, SET;
   judgement |- SET, SET : INT;

   |- set_i[], SET2 ;

   belongs_set(|- ELT, SET2)  &  |- ELTR, SET2
   ----------------
   |- set_i[ELT.ELTR], SET2 ;

   |- S1, S2
   ----------------
   |- S1, S2 : int 1;

   recovery
   |- S1, S2 :int 0;
   end includes_set;

Be carreful not to have the boolean instantiated in the call.
For example
   |- set_i[int 4], set_i[4] : int 0
will be proved. It can not be proved using the regular rules, so
it will be with the recovery rule.
All logical problems due to negation as failure and cuts will be
inherited. Only proofs that do not use recovery rules are real proofs.




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