Re: production rule object creation actions and frame axioms

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 Wednesday, 13 August 2008 23:20:22 UTC