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

Re: lack of model theory for errors in built-ins

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>

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


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

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

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