- From: Gary Hallmark <gary.hallmark@oracle.com>
- Date: Wed, 13 Aug 2008 12:02:22 -0700
- 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 UTC