lack of model theory for errors in built-ins

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
-- 
Jos de Bruijn            debruijn@inf.unibz.it
+390471016224         http://www.debruijn.net/
----------------------------------------------
Doubt is not a pleasant condition, but
certainty is absurd.
   - Voltaire