Linear TGDs

From RuleML Wiki
(Redirected from Linear Rules)
Jump to: navigation, search

--Athant (talk) 23:19, 4 March 2014 (AST)

1 Issue Description

If guarded TGDs (tuple-generating dependencies) are restricted to have just one Atom in the body, this is called a linear TGD. (see Section 4 of http://www.sciencedirect.com/science/article/pii/S1570826812000388).

The guard restriction also means that non-ground facts are not allowed. This is why it is not possible to "cheat" by creating a universal predicate that always holds, and then using it for a guard.

This restriction is known to restore decidability to Datalog plus Existential Rules, Non-conflicting Keys and Negative Constraints.

2 Options

First, I would suggest we start with a smaller sublanguage, as described in A_Minimal_Datalog_Sublanguage In particular,

  1. <Forall> cannot be nested.
  2. <Forall> can only contain an implication.


Then ...

2.1 Option 1.

We could adopt the guard syntax of Reaction RuleML (in advance of the full integration). RR allows the <guard> edge element to be used in several places, including <Rulebase> (it then applies to all "rules", so it is like a "map" version of guardedness), <Rule> and in some other places within the metadata framework. None of these is available within datalog_min (which does not even include <Rulebase>).

However, we could adopt the content model of <guard> (or a restricted version consisting of a single Atom) and allow one guard child within Implies.

Note 1: it is up to the user to construct a guard that actually meets the requirements (sufficiently restricts all the universally quantified variables in the rule) according to the flavor of guardedness the user is implementing.

Note 2: the guard element in Reaction RuleML is actually a different concept. Therefore we do not want to conflate these two very different concepts by using the same syntax for both

2.2 Option 2.

In addition to the syntax in Option 1, the "simple" guarded (and "linear") case could be implemented in RuleML by having the bound variables of the universal be implicitly extracted from the argument sequence of the <guard> child of the quantified implication. This would allow the guardedness restrictions to be validated without using Schematron. The linear case would constrain the content of <if> to be just <And/>.

Restrictions required

  1. the bound variable list is empty. Instead <Forall> contains an attribute @guarded = "guarded" to indicate these semantics.

Note: Relax NG can implement the supremum language that allows the guarded or unguarded universal ( a choice between an attribute and a child element patter) but XSD cannot express that supremum precisely.

2.3 Option 3.

An implication syntax of lower expressivity could be used, where only Atoms are allowed in the body. It would then be necessary to have a module where the content model for the body is relaxed to allow conjunctions and disjunctions. This requires a backward-incompatible change to the MYNG encoding, and so should be postponed until there is a larger overhaul of MYNG.

3 Discussion

3.1 Floating Variables

In either option, syntactic validation in Relax NG or XSD would not catch the case of a "floating" var - a <Var> that occurs in some formula but is not bound.

Examples:

  1. a <Var> appears in the head, but not the body, and is not in the list of existentially bound head variables.
  2. a <Var> appears in a fact.
  3. a <Var> appears in the body in a <formula> that is not a guard, and it does not occur in the guard. This can't occur in the linear case.

Note that we are not using implicit closure in minimal Datalog, so floating <Var>s is already a problem, even without considering guards. This problem does not arise in the RuleML CL subfamily, because there is no separate syntax for variables.

3.2 Different Semantics of Guards

Because to the use of the guard element already in Reaction RuleML for a different concept of guard than what we are talking about here, we will not implement either Option 1 or 2.

4 Resolution