Re: Issue-31: Disjoint sorts - sketch of test case

Jos de Bruijn wrote:
> <snip/>
> 
>> ** 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.
> 
> No, this would not work.
> 
> Say you have a rule and a fact:
> 
> Forall x,y (x=y).
> p(a).
> 
> Under ONDS, this entails p(a), but not q(a).
> Under OS, this entails both p(a) and q(a).
> 
> You can rename your symbols as much as you want, but every symbol will
> be interpreted as the same symbol.

Good point, I glossed over this translation case too quickly.

I guess I was assuming some notion of safe rules (all variables must 
occur in at least one body atom) which would avoid that particular 
example. Would that be sufficient to allow symbol renaming to work?

Otherwise the translation would have to carry over the static type 
information and use that to qualify things like equality operators:

    unary_pred(p_unary_pred).
    individual(a_individual).

    Forall x, y: (x = y) :- And( individual(x), individual(y) )

    p_unary_pred(a_individual).

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

> Conclusion: translations from DS and ONDS to OS do not work in the
> general case.


> 
> 
> Best, Jos
> 
>> ** 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
>>
>

Received on Tuesday, 1 May 2007 17:16:27 UTC