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

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