Re: production rule object creation actions and frame axioms

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