Re: Centaur-Barcelona

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

In article <12253@sophia.inria.fr>, mylonakis@lsi.upc.es (Nicos Mylonakis) writes:

|> 	We have found a semantic problem with TYPOL. We haven't found the way 
|> to express negation inside a rule.
|> 
|> 	If we have a rule such as:
|> 
|> 	|- p(X)
|> 	|- q(X)
|> 	------
|> 	|- X
|> 
|> 	and we want to add another rule as
|> 
|> 	|- p(x)
|> 	|- not q(X)
|> 	-------
|> 	|- X
|> 	
|> 	We haven't found any other way to do this that building another set
|> not_q which is the opposite of q.

There is no negation in Typol for many reasons.

Negation is a real problem in logic programming. 
Negation as failure in unsafe when the goal to be negated contains free
variables. Some prolog introduced a safe form of negation that wait until
the negated goal is ground. This is the case in MU-Prolog, NU-Prolog and             
Sepia. But I am afraid that this is to restrictive for Typol specifications.
May be the best answer is given by the constructive negation of Sepia, but I 
have not yet play with it.

There is one more reason, not to have negation in Typol. Even with a sound
negation, you do not get a proof of the negated goal.

What is possible now in Typol?

-Type constraints:
    if f is an operator of type P -> P', 
    P1 and P2 are both included in P, with an empty intersection,
    you can use constrained variables

    var x: P1;
    var y: P2;

    f(x) and f(y) are then two exclusive schemes and this may be use
    to expresse a sort of structural negation.

-diff:
    import diff(_,_) from prolog;
    is also a structural negation

-defining two sets, p and not_p as you did it

-combining these two sets in one, by adding a boolean parameter
   for example  find(e |- x -> "true") or find(e |- x -> "false")

-using "recovery"
   This was designed for error recovery. In a type checker for example, you would
like not to fail, but want to allow the computation to proceed. In this case you 
are not interested in the proof of the negation. The implementation of error
recovery uses negation as failure, soft cuts, and will check that no constraints
(sleeping goals) are generated during the negation or before a soft cut. Error
recovery allow to fill in a hole in the proof tree, giving some default bindings.
Let's say that error recovery rules are not part of the semantics, but are here
to make live easier.



I hope this will help you, and would like to have any suggestion or comment.
   

-- 
+----------------------------------------------------------------------------+
|     Thierry Despeyroux         | email: Thierry.Despeyroux@sophia.inria.fr |
|  I.N.R.I.A. Sophia-Antipolis	 | phone: +33 93 65 77 07		     |
|   2004, Route des Lucioles	 | fax:   +33 93 65 77 66		     |
|           B.P. 109		 | telex: INRIASA 970 050 F		     |
| F-06561 Valbonne Cedex, France |					     |
+----------------------------------------------------------------------------+