Issue-31: Disjoint sorts - sketch of test case

At yesterday's discussion on Issue-31 we thought it would be useful to 
develop a test case to illustrate the translation issues involved in 
choosing between the various disjointness approaches.

I half-volunteered for this. I'm familiar with the corresponding issue 
in OWL but not with the corresponding issue for rule systems. Here is a 
first cut at translating a simplified OWL example into a rule system 
setting.

** Caveats:

I may be misunderstanding the issue in a rule system setting, in which 
case perhaps by attempting to make it concrete that will at least shed 
light on the misunderstanding.

I don't think I care about this issue enough to want to drive it.

So treat this as an initial stimulus for thought. Hopefully someone with 
more experience in rule systems will be able to come up with a better 
test case.

** Notation

I'm using the RIF Core human readable syntax as best I can but using
simple labels rather than sort-tagged IRIs for the constants :-)

The terms DS, ONDS, OS stand for "disjoint sorts", "overlapping-names
disjoint sorts" (aka punning) and "overlapping sorts" as described in
[1].

** Base test case

  Ruleset:
   Forall ( p(a) :- And())             # p(a).
   Forall ( q(b) :- And())             # q(b).
   Forall ( p = q :- And())            # p = q.

  Query: p(?x)

N.B. I'm assuming that the RIF Core atomic term "p = q" treats "p" and
"q" as individuals.

This is intended to be analogous to having "p" and "q" designate OWL
classes, "a" and "b" be OWL individuals, "p(a)" be an rdf:type assertion 
and "=" be owl:sameAs. DS is OWL/DL, ONDS is OWL/DL-1.1, OS is OWL/full.

In which case ...

If the core is DS this is ill-formed.

If the core is ONDS this is well-formed and the query would return
just the binding p(a). The equality statement only asserts equality
between "p" and "q" when used in the syntactic role of individuals and
does not affect their interpretation as unary predicates.

If the core is OS this is well-formed and the query would return the
two bindings p(a) and p(b).

(a) Am I right in understanding that this is what everyone means by
     the DS/ONDS/OS choice?

(b) Is this a legal formulation of a test case in RIF Core?

If the answer to the above are both yes (hah) then we can look at the
translation issues.

** ONDS to DS

The source rule uses the same identifier for distinct objects so the
translator needs to introduce new identifiers:

   Forall ( p_unary_pred(a) :- And())
   Forall ( q_unary_pref(b) :- And())
   Forall ( p_individual = q_individual :- And())

Query: p_unary_pred(?x)

The translation is straightforward but the form of identifiers in the
target system may not be intuitive.

A static analyis could omit the identifier renaming for constants
which are not subject to punning but that leads to a non-monotonic
translation which is undesirable (at least in the OWL setting).

** ONDS to OS

Same as for ONDS to DS, the translator has to introduce new
identifiers.

** OS to DS

Hummm ...

If we can assume an equality operator for predicates (=pred=) then I
guess the translation would be something like:

   Forall ( p_unary_pred(a) :- And())
   Forall ( q_unary_pref(b) :- And())
   Forall ( p_individual =indivdual= q_individual :- And())
   Forall ( p_unary_pred =pred= q_unary_pred)

Query: p_unary_pred(?x)

If not then we would have to rewrite all of the rules involving p and q
to introduce the alias syntactically:

   Forall ( p_unary_pred(a) :- And())
   Forall ( q_unary_pref(a) :- And())
   Forall ( p_unary_pred(b) :- And())
   Forall ( q_unary_pref(b) :- And())
   Forall ( p_individual = q_individual :- And())

Query: p_unary_pred(?x)

** OS to ONDS

Would be either:

   Forall ( p(a) :- And())
   Forall ( q(b) :- And())
   Forall ( p =indivdual= q :- And())
   Forall ( p =pred= q :- And())

Query: p(?x)

or

   Forall ( p(a) :- And())
   Forall ( q(a) :- And())
   Forall ( p(b) :- And())
   Forall ( q(b) :- And())
   Forall ( p = q :- And())

Query: p(?x)

Dave

[1] http://www.w3.org/2005/rules/wg/wiki/Issue-31

-- 
Hewlett-Packard Limited
Registered Office: Cain Road, Bracknell, Berks RG12 1HN
Registered No: 690597 England

Received on Wednesday, 18 April 2007 08:33:52 UTC