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₁, ..., p_n), such that 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₁ ... ?V_n(φ) with φ', which is obtained from φ by replacing all occurrences of ?V₁, ..., ?V_n with ?V₁', ..., ?V_n', which are variable symbols not appearing anywhere outside of φ.

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₀ is the root, ψ' ∈ L_a(n₀), L_n(n₀) = false, and for every node n ∈ N we have that

• if some conjunction And(φ₁ ... φ_k) ∈ L_a(n), then φ_i ∈ L_a(n) for every φ_i, 1 ≤ i ≤ k
• if φ is some disjunction in L_a(n) and φ=Or(ψ₁ ... ψ_m), then n has m child nodes n'₁,...,n'_m such that L_a(n'_j)=L_a(n)\φ∪{ψ_j} and L_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'₁ and n'₂ such that L_a(n'₁)=L_a(n)\INeg(φ)∪φ, L_n(n'₁)=true, L_a(n'₂)=L_a(n)\INeg(φ), L_n(n'₂)=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 is bounded in A.
• 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 ith argument of an external atomic formula External(f(t₁,...,t_n)) such that f has a valid binding pattern (p₁, ..., p_n) such that p_i=u and, for every j ∈ {1,...,n}\i, p_j=b iff t_j is bounded in A.
• An external term External(f(t₁,...,t_n)) is bounded in A if f has a valid binding pattern (p₁, ..., p_n) such that p_j=b iff t_j is bounded in A, for 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(φ₁ ... φ_n) is safe if φ₁, ..., and φ_n 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 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.