PRD Safeness As Core Extension

From RIF
Jump to: navigation, search

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 (p1, ..., pn), such that pi=b or pi=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 ?V1 ... ?Vn(φ) with φ', which is obtained from φ by replacing all occurrences of ?V1, ..., ?Vn with ?V1', ..., ?Vn', which are variable symbols not appearing anywhere outside of φ.

The tree corresponding to ψ', denoted Tψ' is a labeled tree (N,E,La,Ln), where each node n ∈ N is labeled using the labeling function La with a set of formulas and is also labeled using the labeling function Ln with a boolean value. We define Tψ' as the smallest labeled tree such that n0 is the root, ψ' ∈ La(n0), Ln(n0) = false, and for every node n ∈ N we have that

  • if some conjunction And(φ1 ... φk) ∈ La(n), then φi ∈ La(n) for every φi, 1 ≤ i ≤ k
  • if φ is some disjunction in La(n) and φ=Or(ψ1 ... ψm), then n has m child nodes n'1,...,n'm such that La(n'j)=La(n)\φ∪{ψj} and Ln(n'j)=Ln(n), for 1 ≤ j ≤ m.
  • if some negation INeg(φ) ∈ La(n) and φ is a conjunction, disjunction, or negation, then n has two child nodes n'1 and n'2 such that La(n'1)=La(n)\INeg(φ)∪φ, Ln(n'1)=true, La(n'2)=La(n)\INeg(φ), Ln(n'2)=Ln(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 La(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 La(n), restricted to atomic formulas, and further restricted to Ln(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(t1,...,tn)) such that f has a valid binding pattern (p1, ..., pn) such that pi=u and, for every j{1,...,n}\i, pj=b iff tj is bounded in A.
  • An external term External(f(t1,...,tn)) is bounded in A if f has a valid binding pattern (p1, ..., pn) such that pj=b iff tj 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(φ1 ... φn) is safe if φ1, ..., 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.