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

>> <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?

If all rules are safe, then this problem would not occur, because it
would be impossible to make statements involving the entire domain.

However, *all* rules would need to be safe, not just those which include
equality.

And indeed, as Chris suggested, if you do not allow equality, then this
problem would not occur; one could also allow equality to only occur in
the body.  This was shown in the 1993 HILOG paper by MichaelK and others.

> 
> 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).

Yes, this embedding would effectively turn the OS language into a DS
language.
I am not sure, however, was there anyone who receives such rules will be
able to make any sense out of them :-)



Best, Jos

> 
> Dave

-- 
Please note my new email address:
                         debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
In heaven all the interesting people are
missing.
  - Friedrich Nietzsche

Received on Wednesday, 2 May 2007 06:05:14 UTC