W3C home > Mailing lists > Public > public-rif-wg@w3.org > August 2008

Re: production rule object creation actions and frame axioms

From: Gary Hallmark <gary.hallmark@oracle.com>
Date: Wed, 13 Aug 2008 12:02:22 -0700
Message-ID: <48A32FBE.4010709@oracle.com>
To: kifer@cs.sunysb.edu
CC: RIF WG <public-rif-wg@w3.org>



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.

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. 
> (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.
Received on Wednesday, 13 August 2008 19:04:26 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 2 June 2009 18:33:53 GMT