DeAL TutorialNegation


Existential Variables

Existential variables are those which only appear once in the rule (alias singleton variables). They have a meaning 'there exists' in positive goals and 'there does not exist' in negated goals.

print_nice_people(X) <- person(X), ~nasty(X).  
print_nice_people(`everybody is nice') <- ~nasty(Y).

The variable Y in the last rule and X in the previous one could be replaced by an underscore; it is called an existential variable. Programs with existential variables in negated goals can be transformed into equivalent programs without. For instance the last rule can be re-written as:

print_nice_people(`everybody is nice') <- ~someonenasty.
someonenasty <- nasty(Y).

This rewriting defines the evaluation used by the system.

Negation: safety rules

The appearance of variables in negated goals does not make them safe. For instance, Y in the following rule is always unsafe (the safety of X depends on the export used)

p(X) <- Y > X, ~r(X, Y).

An unbound variable appearing in a negated goals can never be used in later goals of the rule. For instance

print_nasty_people(X) <- ~nice(X),  person(X).

This rule will not compile. Thus, the order of goals in the rules must be switched.

Last Updated 2014