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

OK, I had to try and capture this while it was in my mind, by tomorrow I will 
have forgotten what I was thinking.

The definition of basic semantic structures is extended as follows:

rif:error is a distinguished element of Const & D.
IC(rif:error) -> rif:error
IF(f)(t1 ... tn)) = rif:error (on error, if f is a builtin function)
IF(f)(... rif:error ...)) = rif:error (if f is a function)

ITruth(Builtin (r ( t1 ... tn ))) = T or F (undefined - on error)
ITruth(r ( ... rif:error ...) = T or F (undefined)

That's all.  All mappings are total, there are no new truth values and rif:error 
is in the domain.  The point is that the spec doesn't tell you the truth value 
of predicates when there is an error.  They have a truth value, so the mappings 
are total, we just don't specify which it is.

This means that errors would not "propagate" through rules, etc, only through 
nested functions.  The message is something like: In reality, we'd expect 
something operational happens on errors, but if you insist on proving something, 
we're not telling you what you prove.



Jos de Bruijn wrote:
> 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]
> 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]
>>> -- 
>>> Jos de Bruijn  
>>> +390471016224
>>> ----------------------------------------------
>>> Doubt is not a pleasant condition, but
>>> certainty is absurd.
>>>    - Voltaire

Dr. Christopher A. Welty                    IBM Watson Research Center
+1.914.784.7055                             19 Skyline Dr.                           Hawthorne, NY 10532

Received on Tuesday, 5 February 2008 05:54:11 UTC