Existential in Heads of Rules

From RuleML Wiki
Jump to: navigation, search
--Athant (talk) 18:03, 26 February 2014 (AST)

1 Issue Description

Existential rule languages (Datalog[∃]) are extensions of Datalog that are of interest due to increased expressivity while maintaining decidability (under some restrictions). The supremum language of this subfamily is Datalog+, which also allows equations, in a somewhat restricted fashion, and allows falsity in the head. The RuleML schema must be modified if we want a sublanguage, less than FOL, which contains Datalog+.

2 Options

In order to implement a sublanguage corresponding to Datalog[∃], a new module is needed.

This change affects the following components

  1. Relax NG Schemas and their documentation
  2. Examples - a new test suite and an example are needed
  3. MYNG REST interface - new codes are required for the newly-created sublanguages.
  4. MYNG GUI - new items need to be added to existing facets

The Glossary, Content Models, Normalizer are not affect. An Upgrader is not needed for this change.

2.1 Option 1

The new existential-head module would contain the following definition

  ConclusionFormula |= Exists-node.choice

2.2 Option 2

A slightly more complex modification would introduce some new patterns in the implication module:

  ConclusionFormula.choice |=
    Atom-head-node.choice
    | Equal-head-node.choice
    | And-head-node.choice
    | Or-head-node.choice
    | Negation-head-node.choice
    | NegationAsFailure-node.notallowed
    | Implication-head-node.choice
    | Forall-head-node.choice
    | Exists-head-node.choice

These new patterns allow more complete control of the contents of the heads (conclusions) of implications. Initially (prior to implementation of MYNG Expressivity) we would have (also in the implication module)

  Atom-head-node.choice |= Atom-node.choice
  Equal-head-node.choice |= Equal-node.choice
  Or-head-node.choice |= Or-dis-node.choice
  Negation-head-node.choice |= Negation-node.choice
  Implication-head-node.choice |= Implication-fo-node.choice
  Forall-head-node.choice |= Forall-fo-node.choice
  Exists-head-node.choice |= Exists-fo-node.choice

Also, we allow conjunctions in the head - this doesn't change the expressivity of Datalog (because rule with an unquantified conjunctive head can be decomposed into multiple rules with atomic heads). However, in existential rules, a rule with an existentially quantified conjunctive head cannot necessarily be decomposed in this way, so having conjunctions significantly affects expressivity.

Conjunctions in the heads have, in Datalog and Datalog+, a more restricted content model than conjunctions that appear in the body or in facts. Therefore we need a new set of patterns:

  And-head-node.choice |= And-head.Node.def
  And-head.Node.def =
    
    ## within the head of implications
    element And { (And-datt.choice & reAnd.attlist), And.header, And-head.main }
  And-head.main |= formula_And-head-edge.choice*
  formula_And-head-edge.choice |= formula_And-head.edge.def
  formula_And-head.edge.def =
    
    ##
    element formula { formula_And.attlist? & formula_And-head.content }
  formula_And-head.content |= AndHeadFormula.choice
  AndHeadFormula.choice |=
    Atom-node.choice
    | Equal-fo-node.choice
    | And-head-node.choice
    | Or-head-node.choice
    | Negation-head-node.choice
    | NegationAsFailure-node.notallowed
    | Implication-head-node.choice
    | Forall-head-node.choice
    | Exists-head-node.choice

This gives us hooks to make modifications to the head content model at a lower level than ConclusionFormula, but still keeps the integration with the Expressivity Backbone.

Further, the new existential-head module would contain

  Exists-head-node.choice |= Exists-head.Node.def
  Exists-head.Node.def =
    
    ## within the head of implications
    element Exists { (Exists-datt.choice & reExists.attlist), Exists.header, Exists-head.main }
  Exists-head.main |= boundVariables.choice, formula_Exists-head-edge.choice
  formula_Exists-head-edge.choice |= formula_Exists-head.edge.def
  formula_Exists-head.edge.def =
    
    ## within the head of implications
    element formula { formula_Exists.attlist? & formula_Exists-head.content }
  
  ##    
  formula_Exists-head.content |= ExistsHeadFormula.choice
  
  ##
  ExistsHeadFormula.choice |=
    Atom-node.choice
    | Equal-fo-node.choice
    | And-head-node.choice
    | Or-dis-node.choice
    | Negation-head-node.choice
    | NegationAsFailure-node.notallowed
    | Implication-fo-node.choice
    | Forall-fo-node.choice
    | Exists-head-node.choice

The new <formula> edges have to be integrated into stripe-skipping:

  formula_And-head-edge.choice |= formula_And-head.content

  formula_Exists-head-edge.choice |= formula_Exists-head.content

And finally, the new patterns must be initialized in the initialization module.

Note that we are only allowing literals or conjunctions of literals within the existential in the head of an implication, prior to FOL. That means Atoms are always allowed, and strong negations are allowed if they are available in the language.

Equations are treated separately from atomic formulas, in contrast to their treatment elsewhere in the syntax. That is, the equations module may be included, which allows equations to be asserted directly as facts, used in the body of implications, and to appear unquantified in the head of an implication. However, it is not allowed in the head of a Datalog+ rule for an equation to be existentially quantified nor can an equation be a head conjunct. Any allowed equation in Datalog+ may contain a variable that is universally quantified.

3 Discussion

Option 2 is selected, because Option 1 does not give sufficient control of the heads of implications to manage the interaction of equations and falsity with existentials in the head.

A difficulty has appeared regarding the XSD version of this sublanguage. Because there is a different content model for <And> in the head and body of a rule, it is not legal in the XSD version to allow stripe skipping of <if> and <then>. We can work around this for now by generating an XSD with no stripe-skipping. However, this disables all stripe-skipping, not just the ones causing difficulty. --WikiSysop (talk) 12:08, 16 March 2014 (ADT)

There is a certain amount of symmetry between conjunctions and disjunction in the heads of rules. This is made more clear as the existential head module is integrated with the disjunctive module. It makes sense to separate out conjunctive heads as its own module, and make the conjunctive head and disjunctive head modules symmetrical. Taking this to the extreme, we would remove disjuntive Hornlog from the backbone, and instead have disjunctive heads as an orthogonal implication option.

4 Resolution

4.1 Relax NG Modules

The existing implication_expansion_module.rnc[1] has been modified, with the existing pattern for ConclusionFormula.choice modified as proposed above for Option 2.

Also, a new module called existential_head_expansion_module.rnc[2] has been added, with code as proposed above for Option 2.

Further changes have been made to stripe-skipping[3] and initialization modules[4], as per Option 2.

All of these change to the Relax NG schema modules have been implemented in one commit[5].

4.2 Relax NG Drivers

The drivers all_ordered.rnc [6] and all_unordered.rnc [7] used to test module compatibility are augmented with the following Relax NG[8].

  include "modules/existential_head_expansion_module.rnc" inherit = ruleml {start |= notAllowed}

Also, a driver[9] is added to test the independent validity of this module[5].

4.3 MYNG Engine

The MYNG engine[10] is augmented with the following lines[11] [12].

  $implies_ex_head = 3;

  $needExHead  = extractBit($bimplies, $implies_ex_head)*(1-$needFO);

  if ($needExHead){
      echo "#\n# EXISTENTIAL HEADS IN IMPLICATIONS ALLOWED\n";
      echo "#\n".'include "' . $modulesLocation .
        'existential_head_expansion_module.rnc"'."$end\n";
  }

4.4 MYNG GUI

The MYNG GUI[13] is augmented with an additional option "Existential Head" in the "Implication Options" facet [11]. The binary encoding for this facet, originally defined in MYNG#GUI is extended on the left by one bit to accommodate the new option. The new maximum value for the query string parameter "implies" is "xf". The semantics of the existing encoding is not changed, as the new option corresponds to greater code values than were previously used.

Screen Shot 2014-03-11 at 6.30.46 AM.png

4.5 XSDs

An XSD for the datalogex_min sublanguage

datalogex_min_normal.xsd [14]

was auto-generated using Jing/Trang and added to the xsd directory[15].

4.6 Unit Tests

Several unit tests were added to the test suite folder. The unit tests were implemented in the following commits: [16] [5], including

<!-- The heads and bodies of existential rules can contain conjunctions. -->
    <!-- Every employee who directs a department is a manager, and supervises at least another employee who works in the same department -->
    <Forall>
      <Var>E</Var>
      <Var>P</Var>
      <Implies>
        <if>
          <And>
            <Atom>
              <Rel>employee</Rel>
              <Var>E</Var>
            </Atom>
            <Atom>
              <Rel>directs</Rel>
              <Var>E</Var>
              <Var>P</Var>
            </Atom>
          </And>
        </if>
        <then>
          <Exists>
            <Var>E'</Var>
            <And>
              <Atom>
                <Rel>manager</Rel>
                <Var>E</Var>
              </Atom>
              <Atom>
                <Rel>supervises</Rel>
                <Var>E</Var>
                <Var>E'</Var>
              </Atom>
              <Atom>
                <Rel>works_in</Rel>
                <Var>E'</Var>
                <Var>P</Var>
              </Atom>
            </And>
          </Exists>
        </then>
      </Implies>
    </Forall>

Some test cases that are expected to fail validation are also included:

 <!-- An existential head cannot contain disjunctions. -->
    <Forall>
      <Var>x</Var>
      <Implies>
        <if>
          <Atom>
            <Rel>mother</Rel>
            <Ind>Jane</Ind>
            <Var>x</Var>
          </Atom>
        </if>
        <then>
          <Exists>
            <Var>y</Var>
            <Or>
              <Atom>
                <Rel>son</Rel>
                <Var>x</Var>
                <Var>y</Var>
              </Atom>
              <Atom>
                <Rel>married</Rel>
                <Var>y</Var>
              </Atom>
            </Or>
          </Exists>
        </then>
      </Implies>
    </Forall>
    <!-- An existential head cannot contain equations. -->
    <Forall>
      <Var>x</Var>
      <Implies>
        <if>
          <Atom>
            <Rel>mother</Rel>
            <Ind>Jane</Ind>
            <Var>x</Var>
          </Atom>
        </if>
        <then>
          <Exists>
            <Var>y</Var>
              <Equal>
                <Var>x</Var>
                <Var>y</Var>
              </Equal>
          </Exists>
        </then>
      </Implies>
    </Forall>

4.7 Examples

Pedagogical examples that validates directly from the server has been added[12][15].

4.8 htaccess

The .htaccess files [17][18] were modified in order to implement redirections[12].

5 References

  1. implication_expansion_module.rnc
  2. existential_head_expansion_module.rnc
  3. stripe-skipping_expansion_module.rnc
  4. init_expansion_module.rnc
  5. 5.0 5.1 5.2 commit fc55833d4a
  6. all_ordered.rnc
  7. all_unordered.rnc
  8. commit 8cec3e6043
  9. https://github.com/RuleML/deliberation-ruleml/blob/1.01-dev/relaxng/indep_valid_modules/existential_head_expansion_module.rnc
  10. MYNG engine
  11. 11.0 11.1 commit 83ca0d650d
  12. 12.0 12.1 12.2 commit b671b8bd05
  13. MYNG GUI
  14. datalogex_min_normal.xsd
  15. 15.0 15.1 commit 48118d6f38
  16. commit b40313e
  17. https://github.com/RuleML/deliberation-ruleml/blob/1.01-dev/.htaccess
  18. https://github.com/RuleML/deliberation-ruleml/blob/1.01-dev/relaxng/.htaccess