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

OK, I see.  I read this thread in reverse order.  This proposal does boil down 
to adding a third truth value as Michael pointed out.

I think the problem is caused by trying to propagate the error through the truth 
valuation.  Let's talk about it tomorrow.

-Chris

Jos de Bruijn wrote:
> 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.
> 
> 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.
> 
> 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.
> 
> Best, Jos
> 
> [1] http://www.w3.org/2005/rules/wg/wiki/List_of_BLD_built-ins

-- 
Dr. Christopher A. Welty                    IBM Watson Research Center
+1.914.784.7055                             19 Skyline Dr.
cawelty@gmail.com                           Hawthorne, NY 10532
http://www.research.ibm.com/people/w/welty

Received on Tuesday, 5 February 2008 05:05:13 UTC