Safe Rules

In some cases additional constraints have to be placed in rules, to make them finite relations. For example, according to [22], a variable which appears in the head of a rule will only generate infiniteness:

$$lover(Y) \rightarrow loves(X,Y)$$

which means ``all the world loves a lover''. It defines an infinite set of pairs $loves(X,Y)$ (even if the relation $lover/1$ is a finite set) as long as the first argument of $loves/2$ ranges over an infinite set (it is unbounded).

Another case is if a variable appears in a built-in predicate (after [22]) i.e.:

$$X>Y \rightarrow biggerThan(X,Y)$$

It defines an infinite relation if $X$ and $Y$ are allowed to range over an infinite set (i.e.: the integers).

There is a definition of a Safe Rule [22] which states that such a rule creates a finite relation only. A rule is safe when all its variables are limited which is defined as follows:

1. Any variable that appears as an argument in an ordinary predicate of the body is limited.
2. Any variable $X$ that appears in a subgoal $X=a$ or $a=X$, where $a$ is a constant, is limited.
3. Variable $X$ is limited if it appears in a subgoal $X=Y$ or $Y=X$, where $Y$ is a variable already known to be limited.

It is pointed out in [22], that 1 and 2 form a basis for the definition, and 3 can be applied repeatedly to discover more limited variables.