Falsity in Heads of Datalog Rules

From RuleML Wiki
Jump to: navigation, search
--WikiSysop (talk) 14:50, 26 February 2014 (AST)

1 Issue Description

To achieve (only) the expressivity of Datalog[⊥], we need a branching of the expressivity "backbone".

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 affected, as long as the existing construct <Or/> is used to represent falsity. An Upgrader is not needed for this change.

2 Options

2.1 Option 1

The simplest way to get Datalog[⊥] expressivity without a major revision to the modularization and the MYNG interface would be to add an option (called, say, "Negative Constraints") to the implication options facet, allowing empty disjunctions in the heads of rules. The new falsity-head module would contain the following definition

  Or-dis-node.choice |= Or_falsity-node.choice
  Or_falsity-node.choice |= Or_falsity.Node.def

  ## An empty disjunctive expression (falsity)
  Or_falsity.Node.def =
  
    ##
    element Or { Or_falsity.type.def }
    Or_falsity.type.def = (Or-datt.choice & reOr.attlist), Or.header

which simplifies to

  Or-dis-node.choice |= 
    element Or {  (Or-datt.choice & reOr.attlist), Or.header }

2.2 Option 2

A slightly more complex modification would introduce some new patterns in the implication module (see also Existential in Heads of Rules):

  ConclusionFormula.choice |=
    SimpleFormula-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

In this case the new falsity-head module would contain

  Or-head-node.choice |= Or_falsity-node.choice
  Or_falsity-node.choice |= Or_falsity.Node.def

  ## An empty disjunctive expression (falsity)
  Or_falsity.Node.def =
  
    ##
    element Or { Or_falsity.type.def }
    Or_falsity.type.def = (Or-datt.choice & reOr.attlist), Or.header

The existing "dis" module would change to

  Or-head-node.choice |= Or-node.choice

For translation to XSD, the driver schema should not include both the falsity-head and dis modules, because there is overlap in the patterns.

See also MYNG Expressivity.

3 Discussion

Option 1 will be implemented for RuleML 1.01. A more extensive refactorization can happen later.

4 Resolution

Option 1 has been implemented in Version 1.01 See https://github.com/RuleML/deliberation-ruleml/blob/1.01-dev/relaxng/modules/negative_constraint_expansion_module.rnc and https://github.com/RuleML/deliberation-ruleml/commit/98a993c14bd56cf4e8ba69993cf0efa25f6377fb .