PRD Safeness Operational

All excerpts about safeness, including related definitions, from this version of the PRD draft.

Overview

...

Production rule interchange

...

The semantics of condition formulas and the semantics of rules and rule sets make no assumption regarding how condition formulas are evaluated. In particular, they do not require that condition formula be evaluated using pattern matching. However, RIF-PRD conformance, as defined in the section Conformance and interoperability, requires only support for safe rules, that is, forward-chaining rules where the conditions can be evaluated based on pattern matching only.

...

Conditions

Abstract syntax

Terms

...

The function Var(e) that maps a term e to the set of its free variables is defined as follows:

• if e ∈ Const, then Var(e) = {};
• if e ∈ Var, then Var(e) = {e};
• if f(arg₁...arg_n), n ≥ 0, is a positional term, then, Var(f(arg₁...arg_n) = ∪_i=1...n Var(arg_i);

Atomic formulas

...

The function Var, that was defined for terms, is extended to map an atomic formula to the set of its free variables:

• if p(arg₁...arg_n), n ≥ 0, is an atom, then, Var(p(arg₁...arg_n) = Var(External(p(arg₁...arg_n)) = ∪_i=1...n Var(arg_i);
• if t₁ and t₂ are terms, then Var(t₁ [=|#|##] t₂) Var(t₁) ∪ Var(t₂);
• if o', k_i, i = 1...n, and v_i, i = 1...n, n ≥ 1, are terms, then Var(o[k₁->v₁ ... k_n->v_n]) Var(o) ∪_i=1...n Var(k_i) ∪_i=1...n Var(v_i).

RIF-PRD does not require that a conformant consumer be capable of constraint resolution to evaluate condition formulas. To help specify the corresponding syntactic restriction on RIF-PRD condition formulas, we define, for any atomic formula, a, the two following sets:

• a set UBV(a), of the unconditionally bindable variables of a, that is, of the variables that occur in a and that are guaranteed to be bound without constraint resolution is a is satisfied;
• and a set, CBV(a), of conditionally bindable variables. Each variable, v ∈ CBV(a) is associated with the set, BCOND(v, a), that contains the set of the variables occuring in a that guarantee, if they are bound when a is evaluated, that v can be bound without constraint resolution, if a is satisfied.

The sets UBV(a) and CBV(a) of the unconditionally and conditionally bindable variables in an atomic formula a are defined as follows:

• if a is an atom, p(t₁...t_n), n ≥ 0, a frame, t₁[t₂->t₃], a membership formula, t₁#t₂, or a subclass formula, t₁##t₂, then either
  • the only variables in a are arguments of the atomic formula itself: Var(a) ⊆ {t₁...t_n}, and UBV(a) = Var(a) and CBV(a) = ∅;
  • or no argument of the atomic formula is a variable: Var(a) ∩ {t₁...t_n} = ∅, and UBV(a) = CBV(a) = ∅;
  • otherwise, that is, if some of the arguments of a are variables, but others are terms that contain variables, then UBV(a) = ∅ and either
    • the conditional bindability of none of these variables depends on itself, that is, varg ∩ cond = ∅, where varg = Var(a) ∩ {t₁...t_n} and cond = ∪_{∀ ti=1..n ∉ Var(a)} Var(t_i), and CBV(a) = varg, and, ∀ v ∈ CBV(a), BCOND(v, a) = {cond};
    • or CBV(a) = ∅;
• else if a is an equality formula, t₁ = t₂, or an externally defined equality predicate: pred:numeric-equal(t₁, t₂), pred:boolean-equal(t₁, t₂), pred:dateTime-equal(t₁, t₂), pred:date-equal(t₁, t₂), pred:time-equal(t₁, t₂), pred:duration-equal(t₁, t₂), pred:XMLLiteral-equal(t₁, t₂); or the externally defined predicate pred:iri-string(t₁, t₂), then either
  • t₁ and t₂ are, both, variables, and UBV(a) = ∅ and CBV(a) = {t₁, t₂}, with BCOND(t₁, a) = {{t₂}} and BCOND(t₂, a) = {{t₁}};
  • or only t₁ is a variable, and either
    • Var(t₂) = ∅, and UBV(a) = {t₁} and CBV(a) = ∅;
    • or t₁ ∈ Var(t₂), and UBV(a) = ∅ and CBV(a) = ∅;
    • or UBV(a) = ∅ and CBV(a) = {t₁}, and BCOND(t₁, a) = {Var(t₂)};
  • or only t₂ is a variable, and either
    • Var(t₁) = ∅, and UBV(a) = {t₂} and CBV(a) = ∅;
    • or t₂ ∈ Var(t₁), and UBV(a) = ∅ and CBV(a) = ∅;
    • or UBV(a) = ∅ and CBV(a) = {t₂}, and BCOND(t₂, a) = {Var(t₁)};
  • otherwise UBV(a) = CBV(a) = ∅;
• else if a is the externally defined predicate pred:list-contains(l, e), then either
  • e is a variable, and either
    • Var(l) = ∅, and UBV(a) = {e} and CBV(a) = ∅;
    • or e ∈ Var(l), and UBV(a) = CBV(a) = ∅;
    • or CBV(a) = {e}, with BCOND(e, a) = {Var(l)}, and UBV(a) = ∅;
  • or e is not a variable, and UBV(a) = CBV(a) = ∅;
• else if a is any other externally defined predicate, then UBV(a) = CBV(a) = ∅.

Formulas

...

The function Var, that was defined for atomic formulas, is extended to map a condition formula to the set of its free variables:

• if f_i, i = 0...n, n ≥ 0, are condition formulas, then Var([And|Or](f₁...f_n)) ∪_i=0...n Var(f_i);
• if f is a condition formula, then Var(Not(f)) Var(f);
• if f is a condition formula and x_i ∈ Var for i = 1...n, then, Var(Exists x₁ ... x_n (f)) = Var(f) - {x_i | i = 1...n}.

...

The definition of the set UBV(f) of the unconditionally bindable variables and the set CBV(f) of the conditionally bindable variables, that have been defined for atomic formulas is also extended to any condition formula.

When condition formulas are combined, a variable, x, that was conditionally bindable in one component, depending on another variable, y being bound, may become unconditionally bindable in the combination, e.g. because y is unconditionally bindable in the combination, or because the combination is a conjunction, and x, itself, is unconditionally bindable in another conjunct.

To take care of that, we define, first, the function reduceBCV, that updates ietratively the status of conditionally bindable variables in a formula, f, based on the state of the set of unconditionally bindable variables in f:

reduceCBV (f)

While ∃ v ∈ CBV(f), ∃ c ∈ BCOND(v, f), such that c ⊆ UBV(f)
  BCV(f) := BCV(f)\v
  UBV(f) := UBV(f) + v

The definition of the sets UBV(f) and CBV(f) is extended recursively, as follows, to a condition formula f:

• if f is a conjunction, And(f₁...f_n), n ≥ 0, then
  1. UBV(f) and CBV(f) are initialized with ∪_i=1..n UBV(f_i) and ∪_i=1..n CBV(f_i) - UBV(f), respectively,
  2. ∀ v ∈ CBV(f), BCOND(v, f) = ∪_fi=1..n BCOND(v, f_i): the bindability conditions associated to the variables in CBV(f) are updated, taking into account that a conditionally bindable variable can be bound if the variables in any bindability condition from any of the conjuncts are bound;
  3. and reduceCBV(f) is executed to update UBV(f) and CBV(f), removing from CBV(f) and adding to UBV(f) all the variables that are conditionally bindable in some conjunct, conditioned on the bindability of variables that are unconditionally bindable in some other conjunct;
• else if f is a disjunction, Or(f₁...f_n), n ≥ 0, then UBV(f) = ∩_i=1..n UBV(f_i), CBV(f) = ∩_i=1..n CBV(f_i), and ∀ v ∈ CBV(f), BCOND(v, f) = ∪_fi=1..n BCOND(v, f_i). Since only the variables that are unconditionally bindable in all the disjuncts are in UBV(f), CBV(f) cannot be reduced;
• else if f is a negation, INeg(f'), and UBV(f) = CBV(f) = ∅;
• else if is an existentially quantified condition formula, Exists v₁...v_n (f'), then either
  • {v₁...v_n} ⊆ UBV(f'), that is, all the quantified variables are unconditionally bindable in f' , and
    1. UBV(f) = UBV(f') - {v₁...v_n};
    2. CBV(f) = CBV(f');
    3. ∀ v ∈ CBF(f), BCOND(v, f) = BCOND(v, f') - {c ∈ BCOND(v, f')| c ∩ {v₁...v_n} ≠ ∅}: bindability conditions that depend on variables that are existentially quantified in f are useless outside of f, and they are, accordingly, removed;
  • or it is guaranteed that some of the quantified variables cannot be bound, at least not without constraint resolution, and UBV(f) = CBV(f) = ∅. We call such an existential formula unsafe, by extension of the notion of safeness that is defined in [RIF-Core].

The definition of unconditionally bindable variables in RIF-PRD condition formulas extends the definition of restricted variables in [LEE08]. We extend the definition of a safe formula accordingly.

Definition (Safe condition formula). A RIF-PRD condition formula, f, is safe if and only if, either

• f is an existential condition formula, ∃ {v₁...v_n} (f'), and {v₁...v_n} ⊆ UBV(f');
• or f does not contain any existential sub-formula,
• or all the existential sub-formulas of f are safe.   ☐

...

Operational semantics of condition formulas

...

The semantics is specified in terms of matching substitutions in the sections below. The specification makes no assumption regarding how matching substitutions are determined, and safeness if, therefore, not required from well-formed condition formulas. However, RIF-PRD conformance requires processing of safe condition formulas only.

...

Actions

...

Production rules and rule sets

Abstract synatx

...

Well-formed rules and groups

The function Var(f), that has been defined for condition formulas and extended to actions, is further extended to rules, as follows:

• if f is an action block that declares action variables ?v₁ ... ?v_n, n ≥ 0, and that contains actions a₁ ... a_m, m ≥ 1, then Var(f) = ∪_{1 ≤ i ≤ m} Var(a_i) \ {?v₁ ... ?v_n};
• if f is a conditional action block where c is the condition formula and a is the action block, then Var(f) = Var(c) ∪ Var(a);
• if f is a quantified rule where ?v₁ ... ?v_n, n > 0, are the declared variables; p₁ ... p_m, m ≥ 0, are the binding patterns, and r is the rule, then Var(f) = (Var(r) ∪ Var(p₁) ∪ ... ∪ Var(p_m)) \ {?v₁ ... ?v_n}.

If f is a rule, Var(f) is the set of the free variables in f. In addition, we define the functions CVar(r) and AVar(r), that return, respectively, the set of the condition variables and the of the action variables in a rule, r:

• if r is an action block that declares action variables ?v₁ ... ?v_n, n ≥ 0, and that contains actions a₁ ... a_m, m ≥ 1, then CVar(r) = ∅ and AVar(r) = ∪_{1 ≤ i ≤ m} Var(a_i) \ {?v₁ ... ?v_n};
• if r is a conditional action block where c is the condition formula and a is the action block, then CVar(r) = Var(c) and AVar(r) = AVar(a);
• if r is a rule with quantified variables, Forall ?v1...?vn such that (p₁...p_m) (r'), n ≥ 1, m ≥ 0, then AVar(r) = AVar(r') and CVar(r) = CVar(r') ∪ Var(p₁) ∪ ... ∪ Var(p_m).

The definition of the sets UBV(r) and CBV(r), that have been defined for condition formulas, is extended to any rule, r, as follows:

• if r is an unconditional action block, then UBV(r) = CBV(r) = ∅; or
• else if r is a conditional action block, if C then A, then UBV(r) = UBV(C) and CBV(r) = CBV(C); or
• else if r is a rule with declared variables, Forall ?v1...?vn such that (f₁...f_m-1) (f_m), where n ≥ 1, m ≥ 1, and f_n, is a rule, then consider the formula f' = And(f₁...f_m), and compute UBV(f') and CBV(f') (according to the definition in the section Formulas). Either
  • if {v₁...v_n} ⊆ UBV(f'), that is, all the quantified variables are unconditionally bindable in f' , then
    1. UBV(f) = UBV(f') - {v₁...v_n};
    2. CBV(f) = CBV(f');
    3. ∀ v ∈ CBF(f), BCOND(v, f) = BCOND(v, f') - {c ∈ BCOND(v, f')| c ∩ {v₁...v_n} ≠ ∅}: bindability conditions that depend on variables that are universally quantified in f are useless outside of f, and they are, accordingly, removed;
  • else it is guaranteed that some of the quantified variables cannot be bound, at least not without constraint resolution, and UBV(f) = CBV(f) = ∅. We call such a rule unsafe, by extension of the notion of safeness that is defined in [RIF-Core].

RIF-PRD extends the definition of safeness in [RIF-Core] as follows.

Definition (Safe rule). A RIF-PRD rule, r, is safe if and only if and, either

• it is an unconditional or a conditional action block,
• or it is a rule with quantified variables, Forall ?v1...?vn such that (p₁...p_m) (r'), n ≥ 1, m ≥ 0, and
  • {v₁...v_n} ⊆ UBV(And(p₁, ..., p_m, r')),
  • and the binding patterns, p₁, ..., p_m, if any, are all safe condition formulas,
  • and the rule in the scope of the quantifier, r' , is safe,
  • and either Var(r) ≠ ∅ or AVar(r) ⊆ CVar(r).   ☐

A safe rule set contains only safe rules.

Definition (Well-formed rule). A rule, r, is a well-formed rule if and only if either

• r is an unconditional well-formed action block, a,
• or r is a conditional action block where the condition formula, c, is a well-formed condition formula, and the action block, a, is a well-formed action block,
• or r is a quantified rule (with or without binding patterns), Forall V [such that P](r'), and
  • each of the binding patterns, p_i ∈ P = {p₁,...,p_n}, n ≥ 0, is a well-formed condition formula,
  • and the quantified rule, r', is a well-formed rule.   ☐

Definition (Well-formed group). A well-formed group is either:

• a group that contains no rule or group (an empty group), or
• a group, G that contains only well-formed groups, g₁...g_n, n ≥ 0, and well-formed rules, r₁...r_m, m ≥ 0, such that ∀ r_i ∈ G, Var(r_i) = ∅ and AVar(r_i) ⊆ CVar(r_i).   ☐

The set of the well-formed groups contains all the production rule sets that can be meaningfully interchanged using RIF-PRD.

The specification of the operational semantics of rules and rule sets assumes that all the variables that occur in the action blocks of a rule are bound during the evaluation the condition or binding patterns of the same rule. It makes no assumption regarding how condition formulas, in the rules, are evaluated: it is not required, therefore, that a well-formed group contains only safe rules. RIF-PRD conformance, however, requires only processing of safe rules.

...

Conformance and interoperability

...

Conformance Clauses

Definition (RIF-PRD conformance).

• A RIF processor is a conformant RIF-PRD_Τ,Ε,C,H consumer iff it implements a semantics-preserving mapping from the set of all safe RIF-PRD_Τ,Ε,C,H rule sets to the language L of the processor;
• A RIF processor is a conformant RIF-PRD_Τ,Ε,C,H producer iff it implements a semantics-preserving mapping from a subset of the language L of the processor to a set of safe RIF-PRD_Τ,Ε,C,H rule sets;
• An admissible document is an XML document that conforms to all the syntactic constraints of RIF-PRD, including ones that cannot be checked by an XML Schema validator;
• A conformant RIF-PRD consumer is a conformant RIF-PRD_Τ,Ε,C,H consumer in which Τ consists only of the symbol spaces and datatypes, Ε consists only of the externally defined functions and predicates, C consists only of the conflict resolution strategies, and H consists only of halting tests that are required by RIF-PRD. The required symbol spaces are rif:iri and rif:local, and the datatypes and externally defined terms (built-ins) are the ones specified in [RIF-DTB] and in the section Built-in actions. The required conflict resolution strategy is the one that is identified as rif:forwardChaining, as specified in section Conflict resolution; and the required halting test is the one specified in section Halting test. A conformant RIF-PRD consumer must reject all inputs that do not match the syntax of RIF-PRD. If it implements extensions, it may do so under user control -- having a "strict RIF-PRD" mode and a "run-with-extensions" mode;
• A conformant RIF-PRD producer is a conformant RIF-PRD_Τ,Ε,C,H producer which produces documents that include only the symbol spaces, datatypes, externals, conflict resolution strategies and halting tests that are required by RIF-PRD.   ☐

...