Safeness in Core
Intuitively, safeness of rules guarantees that, when performing reasoning in a forward-chaining manner, it is possible to find bindings for all the variables in the rule so that the condition can be evaluated.
To define safeness, we need to define, first, the notion of binding patterns for externally defined terms, as well as under what conditions variables are considered bound.
Definition (Binding pattern). Binding patterns are lists of the form (p_{1}, ..., p_{n}), such that p_{i}=b or p_{i}=u, for 1 ≤ i ≤ n: b stands for a "bound" and u stands for an "unbound" argument. ☐
Each external function or predicate has an associated list of valid binding patterns. We define here the binding patterns valid for the functions and predicates defined in [RIF-DTB].
Every function or predicate f defined in [RIF-DTB] has a valid binding pattern for each of its schemas with only the symbol b such that its length is the number of arguments in the schema. In addition,
- the external predicate pred:iri-string has the valid binding patterns (b, u) and (u, b) and
- the external predicate pred:list-contains has the valid binding pattern (b, u).
The functions and predicates defined in [RIF-DTB] have no other valid binding patterns.
To keep the definitions concise and intuitive, boundedness and safeness are defined, below, for condition formulas in disjunctive normal form, that can be existentially quantified themselves, but that contain, otherwise, no existential sub-formula. The definitions apply to any valid RIF-Core condition formula, because they can always, in principle, be put in that form, by applying the following syntactic transforms, in sequence:
- if f contains existential sub-formulas, all the quantified variables are renamed, if necessary, and given a name that is unique in f, and the scope of the quantifiers is extended to f. Assume, for instance, that f has an existential sub-formula, sf = Exists v_{1}...v_{n} (sf'), n ≥ 1, such that the names v_{1}...v_{n} do not occur in f outside of sf. After the transform, f becomes Exists v_{1}...v_{n} (f'), where f' is f with sf replaced by sf' . The transform is applied iteratively to all the existential sub-formulas in f;
- the (possibly existentially quantified) resulting formula is rewritten in disjunctive normal form ([Mendelson97], p. 30).
Definition (Boundedness). An external function term External(f(t_{1},...,t_{n})) is bound in a condition formula, if and only if f has a valid binding pattern (p_{1}, ..., p_{n}) and, for all j, 1 ≤ j ≤ n, such that p_{j}=b, t_{j} is bound in the formula.
A variable, v, is bound in an atomic formula, a, if and only if
- a is neither an equality nor an external predicate, and v occurs as an argument in a;
- or v is bound in the conjunction formula f = And(a).
A variable, v, is bound in a conjunction formula, f = And(c_{1}...c_{n}), n ≥ 1, if and only if, either
- v is bound in at least one of the conjuncts;
- or v occurs as the j-th argument in a conjunct, c_{i}, that is an externally defined predicate, and the j-th position in a binding pattern that is associated with c_{i} is u, and all the arguments that occur, in c_{i}, in positions with value b in the same binding pattern are bound in f' = And(c_{1}...c_{i-1} c_{i+1}...c_{n});
- or v occurs in a conjunct, c_{i}, that is an equality formula, and v occurs as the term on one side of the equality, and the term on the other side of the equality is bound in f' = And(c_{1}...c_{i-1} c_{i+1}...c_{n}).
A variable, v, is bound in a disjunction formula, if and only if v is bound in every disjunct where it occurs;
A variable, v, is bound in an existential formula, Exists v_{1},...,v_{n} (f'), n ≥ 1, if and only if v is bound in f'. ☐
Notice that the variables, v_{1},...,v_{n}, that are existentially quantified in an existential formula f = Exists v_{1},...,v_{n} (f'), are bound in any formula, F, that contains f as a sub-formula, if and only if they are bound in f, since they do not exist outside of f.
Definition (Safeness). A variable, v, is safe in a condition formula, f, if and only if
- f is an atomic formula and f is not an equality formula in which both terms are variables, and v occurs in f;
- or f is a conjunction, f = And(c_{1}...c_{n}), n ≥ 1, and v is safe in at least one conjunct in f, or v occurs in a conjunct, c_{i}, that is an equality formula in which both terms are variables, and v occurs as the term on one side of the equality, and the variable on the other side of the equality is safe in f' = And(c_{1}...c_{i-1} c_{i+1}...c_{n});
- or f is a disjunction, and v is safe in every disjunct;
- or f is an existential formula, f = Exists v_{1},...,v_{n} (f'), n ≥ 1, and v is safe in f' .
A RIF-Core rule, r is safe if and only if
- r is a variable free atomic formula,
- or r is a universal fact, Forall v_{1},...,v_{n} (f), n ≥ 1, and f is variable free,
- or r is a rule implication, h :- b, and all the variables that occur in h are safe in b, and all the variables that occur in b are bound in b;
- or r is a universal rule, Forall v_{1},...,v_{n} (r'), n ≥ 1, and r' is safe.
A group, Group (s_{1}...s_{n}), n ≥ 0, is safe if and only if
- it is empty, that is, n = 0;
- or s_{1} and ... and s_{n} are safe.
A document is safe if and only if
- it contains a safe group, or no group at all,
- and all the documents that it imports are safe. ☐
Extension of the definitions for PRD
The pre-processing is extended to take negation into account, and the definition of rule safeness is extended to take nested foralls and patterns into account. See below.
All the other definitions remain unchanged. Notice that the definitions are not extended for negation and, followingly, an universally quantified (rule) variable is never bound or safe as a consequence of occurring in a negative formula.
The pre-processing section is extended as follows:
In RIF-Core, the definitions of boundedness and safeness, below, apply to a condition formula, f, after it has been simplified syntactically, by applying the transforms described below, in sequence.
- if f contains existential sub-formulas, all the quantified variables are renamed, if necessary, and given a name that is unique in f, and the scope of the quantifiers is extended to f. Assume, for instance, that f has an existential sub-formula, sf = Exists v_{1}...v_{n} (sf'), n ≥ 1, such that the names v_{1}...v_{n} do not occur in f outside of sf. After the transform, f becomes Exists v_{1}...v_{n} (f). The transform is applied iteratively to all the existential sub-formulas in f;
- the (possibly existentially quantified) resulting formula is rewritten in disjunctive normal form.
In RIF-PRD, these pre-processing steps are modified to take negation into account, as follows:
- if the condition formula under consideration, f, contains negation sub-formulas, existential formulas that occur inside a negated formula are handled as if they were atomic formulas, with respect to the two processing steps. Extending the scope of an existential quantifier beyond a negation would require its transformation into an universal quantifier, and universal formulas are not part of RIF-PRD condition language;
- in addition, the two pre-processing steps are applied, separately, to these existentially quantified formulas, to be able to determine the status of the existentially quantified variables with respect to boundedness.
The definition of rule safeness is replaced by the following one, that extends the one for RIF-Core rules.
Definition (RIF-PRD rule safeness). A RIF-PRD rule, r, is safe if and only if
- r is an unconditional action block, and Var(r) = ∅;
- or r is a conditional action block, If C Then A, and all the variables in Var(A) are safe in C, and all the variables in Var(r) are bound in C;
- or r is a rule with variable declaration, ∀ v_{1}...v_{n} such that p_{1}...p_{m} (r'), n ≥ 1, m ≥ 0, and either
- r' is an unconditional action block, A, and the conditional action block If And(p_{1}...p_{m}) Then A is safe;
- or r' is a conditional action block, If C Then A, and the conditional action block If And(C p_{1}...p_{m}) Then A is safe;
- or r' is a rule with variable declaration, ∀ v'_{1}...v'_{n'} such that p'_{1}...p'_{m'} (r"), n' ≥ 1, m' ≥ 0, and the rule with variable declaration ∀ v_{1}...v_{n} v'_{1}...v'_{n'} such that p_{1}...p_{m} p'_{1}...p'_{m'} (r"), is safe.