Re: production rule object creation actions and frame axioms

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 00:31:53 UTC