From: Jos de Bruijn <debruijn@inf.unibz.it>

Date: Sun, 03 Feb 2008 11:40:29 +0100

Message-ID: <47A59A1D.3070502@inf.unibz.it>

To: Michael Kifer <kifer@cs.sunysb.edu>

CC: RIF WG <public-rif-wg@w3.org>

Received on Sunday, 3 February 2008 10:41:03 GMT

Date: Sun, 03 Feb 2008 11:40:29 +0100

Message-ID: <47A59A1D.3070502@inf.unibz.it>

To: Michael Kifer <kifer@cs.sunysb.edu>

CC: RIF WG <public-rif-wg@w3.org>

Michael, You're right. The definitions don't work. If we would fix them, we end up with your option (b). So we're back where we started, with the two choices you described in [1]. Best, Jos [1] http://lists.w3.org/Archives/Public/public-rif-wg/2007Dec/0099.html Michael Kifer wrote: > Jos, > thanks for the proposal. I have serious doubts that it holds water. > Please see below. > >> Dear all, >> >> In the telephone conference last Tuesday I mentioned that I had an idea >> for dealing with errors in built-in predicates and functions by not >> defining the semantics in case errors occur. >> >> My proposed solution is the following: >> >> For the purpose of this definition I assume that built-in predicates and >> functions are written as ' Builtin ( ' Uniterm ' ) ', following the >> proposal "syntactic representation of built-ins in RIF" at [1]. >> >> The definition of basic semantic structures is extended as follows: >> I(Builtin(f(t1 ... tn))=IFb(f)(I(t1),...,I(tn)) >> ITruth(Builtin(r ( t1 ... tn ))) = IRb(r)(I(t1),...,I(tn)) >> >> This is merely a routine extension of the interpretation of terms and >> atomic formulas to that of built-in terms and atomic formulas. Note that >> we use the mappings IFb and IRb for the interpretation of built-in >> functions and predicates; it would have also been possible to extend the >> current interpretation functions, but in this case are both that >> introducing new mappings which make things clearer. >> >> Now for the interpretation of built-in functions and predicates: >> >> IFb is a mapping from Const to partial functions from D* into D >> >> IRb is a mapping from Const to partial truth-valued mappings D* TV >> >> Note that the difference with the definitions of IF and IR is that the >> functions and truth value mappings are *partial*. >> >> A consequence of the fact that these mappings are partial is that the >> truth valuation function ITruth may become undefined in case any errors >> in built-in functions or predicates occur. >> >> >> Let's now consider satisfaction of rules, which is defined as follows >> (from the document): >> >> I |= then :- if >> >> iff ITruth(then) =t ITruth(if). >> >> If ITruth(then) or ITruth(if) is undefined, ITruth(then) =t ITruth(if) >> will also be undefined. Therefore, I |= then :- if is undefined. This >> extends to satisfaction of rule sets I |= R. > > Let the rule set be > > p(1). > q(abc). > > r(?Y) :- add(1,?X,?Y), p(?X). > > You did not say how things work with universal quantifiers, but the > definition certainly will look weird a bit. Moreover, universal > quantification should be treated as (a possibly) infinite conjunction > so if one extends your definition in the logical way then the above will > have no models. > >> Now consider an entailment, which is defined as follows: >> >> S |= f >> >> iff for every semantic structure I, such that I |= S, it is the case >> that Itruth(f)=t. >> >> If there is an error in the rule set S, then I |= S is undefined, so >> clearly S |= f is undefined. If there is an error in f, then clearly >> ITruth(f) is undefined, so S |= f is undefined. > > No, from what you said it follows that it is not the case that (S |= f). > >> So, the model theory simply does not interpret rule sets or conditions >> with errors in built-ins. >> >> We should probably include a remark saying that implementations should >> return an error whenever they encounter a rule set which is not interpreted. > > You should probably check that all the theories of minimal, WF, and stable > models hold. You should also probably check if this holds water for the FOL > case. > > I suspect that it does not because of the aforesaid universal > quantification problem. > > This was just my 30-second reaction. Here is my 45-sec reaction. > > Say, "a" is true, "b" false, and "c" is undefined. What's the values of > > Itruth (a \/ c) = ? > Itruth (b /\ c) = ? > > If it's true/false, then this is exactly the same as adding the undefined > truth value and a 3-valued logic. We discussed this before. > > If it is undefined, then this is unacceptable, because it would mean that > the following ruleset would have no models: > > q :- (p, a) \/ (r, c). > p. > > > > > --michael > > >> Best, Jos >> >> [1] http://www.w3.org/2005/rules/wg/wiki/List_of_BLD_built-ins >> -- >> Jos de Bruijn debruijn@inf.unibz.it >> +390471016224 http://www.debruijn.net/ >> ---------------------------------------------- >> Doubt is not a pleasant condition, but >> certainty is absurd. >> - Voltaire > -- debruijn@inf.unibz.it Jos de Bruijn, http://www.debruijn.net/ ---------------------------------------------- One man that has a mind and knows it can always beat ten men who haven't and don't. -- George Bernard Shaw

- application/x-pkcs7-signature attachment: S/MIME Cryptographic Signature

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