From: Michael Kifer <kifer@cs.sunysb.edu>

Date: Wed, 13 Aug 2008 17:06:38 -0400

To: Gary Hallmark <gary.hallmark@oracle.com>

Cc: RIF WG <public-rif-wg@w3.org>

Message-ID: <20080813170638.117e6f25@kiferdesk>

Date: Wed, 13 Aug 2008 17:06:38 -0400

To: Gary Hallmark <gary.hallmark@oracle.com>

Cc: RIF WG <public-rif-wg@w3.org>

Message-ID: <20080813170638.117e6f25@kiferdesk>

On Wed, 13 Aug 2008 13:47:57 -0700 Gary Hallmark <gary.hallmark@oracle.com> wrote: > Can you give an example of a ruleset with a logical function that occurs > only the head or the body (not both) of a single rule but is not a > skolem function (i.e. cannot be replaced with an existentially > quantified variable)? my pint was that almost every function symbol can be treated as a Skolem. Here is an example where it cannot be (I think): Forall X,Y,Z: p(f(X,Z),g(Y,Z)) :- q(X,Y,Z). If we deskolemize f then we get: Forall X,Z Exists V Forall Y: p(V,g(Y,Z)) :- q(X,Y,Z). Now, we cannot deskolemize g because the quantification prefix is linear. We need to somewho have something like Forall Y,Z Exists W (that W is to replace f(Y,Z)), but we cannot squeeze that Forall Y,Z Exists W into what we already have (Forall X,Z Exists V Forall Y) without changing the meaning of the already deskolemized function f). > I was hoping to "support" skolem functions (but no other logical > functions) in PRD by translating skolems in the head (only those that > occur in the "object" position of a classification) to a call to the > class constructor, and translating skolems in the body to an > existentially quantified variable. I think you also need to allow existentials in the object position in the frames. But in any case, you can construct non-terminating examples even with just the classification unless further restrictions are placed. I think it is getting too cumbersome. But if we do not limit ourselves to the core (which some people want to have decidable -- I do not care personally) then there is no problem. --michael > Michael Kifer wrote: > > > > On Wed, 13 Aug 2008 12:02:22 -0700 >> > Gary Hallmark <gary.hallmark@oracle.com> wrote: > > > > > >> > >> Michael Kifer wrote: > >> > >>> On Tue, 12 Aug 2008 15:52:13 -0700 > >>> Gary Hallmark <gary.hallmark@oracle.com> wrote: > >>> > >>> > >>> > >>>> By "skolem function" I meant "logical function used to remove > >>>> existential quantification", e.g. > >>>> > >>>> forall ?X exists ?Y parent(?X,?Y) :- person(?X). > >>>> > >>>> => > >>>> > >>>> forall ?X parent(?X, f01(?X)) :- person(?X). > >>>> > >>>> where f01 is unique in the ruleset. > >>>> > >>>> I think that at least logical functions that are used to skolemize should be > >>>> allowed in Core. > >>>> > >>>> > >>> How do you distinguish skolem functions from other functions? > >>> It is just a unique function symbol -- nothing more. > >>> > >> It's a bit more. It also includes all the in-scope universally > >> quantified variables as arguments. > >> > > > > Any function symbol can be viewed this way. > > > > > > > >> It's easy to distinguish the skolem functions - they are the ones that > >> can be de-skolemized. I.e. > >> all occurrences are in the head of one rule or in the body of one rule. > >> > > > > You can perform the same procedure in many cases for any function symbol. > > If quantification prefix weren't linear then you could have done this in all > > cases. > > > > > >>> (By adding them to BLD I > >>> meant adding syntax and semantics for simplifying their use. Conceptually there > >>> is not much of a diff.) > >>> > >>> What I was trying to say (but forgot to add one rule) is that you can create > >>> nonterminating processes whether the func symbol is unique or not: > >>> > >>> forall ?X parent(?X, f01(?X)) :- person(?X). > >>> forall ?X ?Y person(?Y) :- parent(?X, ?Y). > >>> > >>> so here you go ad infinitum. > >>> > >> Yeah, but its no worse than, e.g. func:concat or func:numeric-add. > >> Unless you also want to remove most of the builtins, you can't get rid > >> of infinity, and skolem functions seem tractable for a PRD translator to > >> implement, that's why I think they should be in Core. > >> > > > > > > For builtins you can come up with more or less reasonable restrictions. > > For skolems you most likely cannot. With existentials the logic becomes > > undecidable and it is not clear what to do here. > > > > The more important point is that you cannot really distinguish skolems from > > non-skolems, as I pointed out above. > > > > michael > > and > > > > >Received on Wednesday, 13 August 2008 21:08:10 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:47:52 UTC
*