Re: production rule object creation actions and frame axioms

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