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

Date: Thu, 14 Aug 2008 15:45:57 -0400

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

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

Message-ID: <20080814154557.76541ed8@kiferserv>

Date: Thu, 14 Aug 2008 15:45:57 -0400

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

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

Message-ID: <20080814154557.76541ed8@kiferserv>

Gary, sorry for not being clear. You can NEVER deskolemize into a valid BLD. For instance, Forall X,Y p(X,Y) :- q(f(X,Y)) is deskolemized into Forall X,Y Exists Z p(X,Y) :- q(Z). Note that this is NOT the same as the following valid BLD: Forall X,Y p(X,Y) :- Exists Z q(Z). The latter is equivalent to Forall X,Y,Z p(X,Y) :- q(Z). Deskolemization always results into an existential in the head, which is not legal in BLD. --michael On Thu, 14 Aug 2008 10:03:56 -0700 Gary Hallmark <gary.hallmark@oracle.com> wrote: > > Ok, if I can ask one last thing in this thread: could you please comment > on the following: > > PROPOSAL > > PRD supports logical functions with the following restriction: > > It must be possible to deskolemize each logical function f into an > existentially quantified variable ?v such that either: > a. the resulting syntax is legal BLD/PRD, i.e., f occurs only in the > body of a single rule (in BLD/PRD, Exists ?v may appear only in the body > of a rule), or > b. the original syntax "matches" And(f(...)#T f(...)[...]) :- ... (i.e. > a skolemized existential in the head used for object creation) > > If a PRD translator encounters a logical function which does not obey > the restriction, then it SHOULD/MUST raise an error. > > Michael Kifer wrote: > > Gary, > > it looks like we are loosing focus. You asked: > > > > >> 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)? > > > > and I gave you an example. If you wanted to ask something else, then please do > > so :-) > > > > If you are thinking of a case when there is **only one** function per rule then > > it can always be deskolemized. > > > > In any case, the point I raised was that Skolem or not Skolem we run into a > > possible non-termination if we allow that (even with one function). > > > > I have nothing against your desire to make Core into an intersection. I just > > pointed out that this desire clashes with some other views that were expressed > > in the telecon (people wanted termination). > > > > > > --michael > > > > > > On Wed, 13 Aug 2008 16:14:53 -0700 > > Gary Hallmark <gary.hallmark@oracle.com> wrote: > > > > > >> Michael Kifer wrote: > >> > >>> 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). > >>> > >>> > >> I would not try to deskolemize f or g because they do not include all 3 > >> in-scope universally quantified variables as arguments. I would regard > >> your rule as not in PRD, because neither can be deskolemized with my > >> (probably too simple-minded) notion of skolem function. > >> > >> If we suppose the following rule instead: > >> > >> Forall X,Y,Z: p(f(X,Y,Z),g(X,Y,Z)) :- q(X,Y,Z). > >> > >> It can be deskolemized as > >> > >> Forall X,Y,Z Exists V,W: p(V,W) :- q(X,Y,Z). > >> > >> However, I would regard this as not in PRD either because V and W are in > >> a head but are not in the object position of a classification (or frame) > >> > >>> 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. > >>> > >> yes, but in that case there must also be the same existential in the > >> object position of a classification so I know what class constructor to > >> invoke to create the new object. > >> > >>> 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. > >>> > >>> > >> I suggested that Core be operationally defined as the intersection of > >> real dialects (e.g. BLD and PRD and ??) -- but apparently there are > >> those among us who want to define it "standalone" although I don't know > >> why. My motivation here is to have the intersection of BLD and PRD as > >> large as practically possible, and it would be good to include (simple) > >> skolem functions so that rules that express object creation using skolem > >> functions can be interchanged between production and derivation rule > >> systems. > >> > >> It sounds like we agree that this should be possible. > >> > >> > >> > >> > >Received on Thursday, 14 August 2008 19:46:45 UTC

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