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

Date: Thu, 14 Aug 2008 10:03:56 -0700

Message-ID: <48A4657C.5070001@oracle.com>

To: kifer@cs.sunysb.edu

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

Date: Thu, 14 Aug 2008 10:03:56 -0700

Message-ID: <48A4657C.5070001@oracle.com>

To: kifer@cs.sunysb.edu

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

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 17:06:19 UTC

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