Re: production rule object creation actions and frame axioms

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