# PRD Safeness As Core Extension

### Safeness

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 in the face of external predicates and functions, we define the notion of * binding patterns*, which are lists of the form (

`p`,

_{1}`...`,

`p`), such that

_{n}`p`=

_{i}`b`or

`p`=

_{i}`u`, for

`1 ≤ i ≤ n`. Intuitively,

`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 [DTB].

Every function or predicate `f` defined in [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 [DTB] have no other valid binding patterns.

For dealing with disjunction, existential quantifiers, equality, and negation in rule premises we need a number of preliminary definitions before we can define safeness.

Let `ψ` be a condition formula. With `ψ'` we denote the formula obtained from `ψ` by replacing all subformulas of the form `Exists ?V _{1} ... ?V_{n}(φ)` with

`φ'`, which is obtained from

`φ`by replacing all occurrences of

`?V`with

_{1}, ..., ?V_{n}`?V`, which are variable symbols not appearing anywhere outside of

_{1}', ..., ?V_{n}'`φ`.

The *tree corresponding to* `ψ'`, denoted T_{ψ'} is a labeled tree (N,E,L_{a},L_{n}), where each node n ∈ N is labeled using the labeling function L_{a} with a set of formulas and is also labeled using the labeling function L_{n} with a boolean value. We define T_{ψ'} as the smallest labeled tree such that n_{0} is the root, `ψ'` ∈ L_{a}(n_{0}), L_{n}(n_{0}) = `false`, and for every node n ∈ N we have that

- if some conjunction
`And(φ`∈ L_{1}... φ_{k})_{a}(n), then`φ`∈ L_{i}_{a}(n) for every`φ`,_{i}`1 ≤ i ≤ k` - if
`φ`is some disjunction in L_{a}(n) and`φ=Or(ψ`, then n has_{1}... ψ_{m})`m`child nodes n'_{1},...,n'_{m}such that L_{a}(n'_{j})=L_{a}(n)\`φ`∪{`ψ`} and L_{j}_{n}(n'_{j})=L_{n}(n), for`1 ≤ j ≤ m`. - if some negation
`INeg(φ)`∈ L_{a}(n) and φ is a conjunction, disjunction, or negation, then n has two child nodes n'_{1}and n'_{2}such that L_{a}(n'_{1})=L_{a}(n)\`INeg(φ)`∪φ, L_{n}(n'_{1})=true, L_{a}(n'_{2})=L_{a}(n)\`INeg(φ)`, L_{n}(n'_{2})=L_{n}(n).

With B_{ψ} we denote the collection of sets of atomic formulas in the leaf nodes of T_{ψ'}, i.e., A ∈ B_{ψ} iff A is L_{a}(n), restricted to atomic formulas, for some leaf node n of the T_{ψ'}.

With B'_{ψ} we denote the collection of sets of atomic formulas in the negated leaf nodes of T_{ψ'}, i.e., A' ∈ B'_{ψ} iff A' is L_{a}(n), restricted to atomic formulas, and further restricted to L_{n}(n)=`true`, for some leaf node n of the T_{ψ'}.

Given a set of atomic formulas A, the *equivalence class* E_{?V} of a variable `?V` in A is the smallest set such that `?V` ∈ E_{?V} and for every `?V'` ∈ E_{?V} and every variable `?V''`, if `?V'=?V''` ∈ A or `?V''=?V'` ∈ A, `?V''` ∈ E_{?V}.

Because a negation `INeg(φ)` is not an atomic formula, neither B_{ψ} nor B'_{ψ} may contain a negation, and E_{?V} is unaffected by a formula such as `INeg(?V=?V')`.

**Definition (Safeness).**
Let `ψ` be a condition formula. A variable `?V` is * safe* in

`ψ`if, for every A ∈ B

_{ψ}, a variable

`?V'`in the equivalence class of

`?V`in A appears in an atomic formula in A that is not an equality term involving two variables.

**Definition (Boundedness).**
Given an A ∈ B_{ψ},

- Every constant symbol
`c`isin A.**bounded** - A variable
`?V`is bounded in A if whenever`?V`appears in A, a variable`?V'`in the equivalence class of`?V`in A is one of the following. Note that`INeg(φ)`is not an atomic formula even if`φ`is an atomic formula.- an argument of a non-external atomic formula in A that is not an equality term involving two variables, or
- the
`i`th argument of an external atomic formula`External(f(t`such that_{1},...,t_{n}))`f`has a valid binding pattern (`p`,_{1}`...`,`p`) such that_{n}`p`=_{i}`u`and, for every`j`∈`{1,...,n}\i`,`p`=_{j}`b`iff`t`is bounded in A._{j}

- An external term
`External(f(t`is bounded in A if_{1},...,t_{n}))`f`has a valid binding pattern (`p`,_{1}`...`,`p`) such that_{n}`p`=_{j}`b`iff`t`is bounded in A, for_{j}`1 ≤ j ≤ n`.

If B'_{ψ} is not empty, a variable `?V` is bounded in `ψ` if `?V` is bounded in every A ∈ B'_{ψ}. Otherwise, `?V` is bounded in `ψ` if `?V` is bounded in every A ∈ B_{ψ}.

A document formula `Γ` is * safe* if every group formula in

`Γ`is safe. A group formula

`Group(φ`is safe if

_{1}... φ_{n})`φ`, ..., and

_{1}`φ`are safe. Every variable-free atomic formula is safe. List terms are safe by definition, because they are always ground in PRD, i.e. contain no variables. A universal rule

_{n}`Forall ?V1 ... ?Vn (if ψ then φ)`is safe iff

`if ψ then φ`is safe. A rule implication

`if ψ then φ`is safe iff all variables appearing in

`φ`are safe in

`ψ`and all variables are bounded in

`ψ`. ☐

Consider the following formula:

Forall ?x ?y ?z ?u ( If Or( And( ex:q(?z) INeg(External(pred:iri-string(?x ?z)))) And( ?x=?y INeg(?y=?u) ex:q(?u))) Then ex:p(?x))

One can verify that this formula is not safe, in the following way: the only variable appearing in the action of the rule is `?x`; `?x` is not bound in the first component of the disjunction because it appears only in a negation. Furthermore, `?x` is not safe in the second component of the disjunction because the inequality prevents `?x` and `?u` from being in the same equivalence class.