Re: model theory of error [Yes, proposing one!]

> Michael,
> 
> So, while you were drinking vodka, I paused and tried to think instead 
> of reacting with my reptilian brain; and (thanx to that very useless 
> meeting I have to attend this morning :-) I looked a little bit into 
> something I had had in the back of my head all the time and got too 
> carried out to consider further...
> 
> What if the new truth value E was such that:
>   ~E = E/\F = E/\T = E\/F = E\/T
>      = E :- T = E :- F = T :- E = F :- E
>      = Forall E = Exists E
>      = E
> so that as soon as you have an E somewhere, everything becomes E (so, 
> the intuitive semantics of E is more like "undefined" than "error")?

This is not a truth table for undefined (U). With the U value, U/\F=F and
U\/T=T.  In any case, it is not very clear what the truth table should
really be. In my proposal the only diff with yours was E\/T=T, but I think
I made a typo there (do not remember what I was thinking).

> Would that lead somewhere?

It might or it might not. This is why I said that it might take over a week,
full time, to check. There are many things to check for compatibility: FOL,
various major LP dialects (well-founded, stable model semantics), how does
it affect our OWL compatibility, the SWRL dialect, etc.

So, I consider this a risky path given our time constraints.

> The intuition is that such an E would allow us to say that a RIF dialect 
> does not guarantee any useful meaning if rules retrieved from the format 
> are used in a way that is not supported by the dialect.

No. The purpose of E is just to define what happens when a variable gets
(inevitably) bound to an out-of-domain value.  Let's assume that we have
this:


   q(1).
   p(?X,?Y) :- q(?X) /\ add(?X,1,?Y).

I am using a builtin predicate, add, since truth valuation is the main
issue here.

If ?X is bound to "csma", then q(csma) is F and add(csma,1,...) is E.  So,
the whole rule instance has truth value E. It does not mean that the above
ruleset is incorrect --- it is correct as far as you and I are concerned,
and it should derive p(1,2). But some instances of this rule have the truth
value E. So, we need to redefine a lot of things in the model theory,
redefine fixpoints, and other stuff, as I indicated above.  I do not
know if all this would hold water, because it means checking a lot of
things.


> In the present case, it would allow us to say that BLD does not carry 
> any useful meaning as soon as a builtin is applied to an out-of-domain 
> argument, thus allowing one implementation to throw an exception, 
> another one to add an error fact in a fact base, yet another to continue 
> drawing inferences at its own risk (possibly notifying the user that 
> these inferences are not necessarily intended by the producer of the 
> rules retrieved from RIF) etc.
> 
> Would that be a workable direction to explore?

See above. It is an interesting direction to explore, but it may turn out
unworkable. If somebody volunteers to do this -- nice. I do not have the
time.


> > 4. The builtin functions will be defined so that they will return rif:error
> >    whenever their arguments are of the wrong type.
> 
> Another question I had in mind (but I am not sure how important it is) 
> is: can we do without introducing rif:error?

Yes. This is probably not necessary.

> That is, specify directly 
> something like:
>                            /
>                            | I_F(f)(I(t1),...,I(tn)) if all args are ok
>      I(f ( t1 ... tn )) = <
>                            | _|_ if one argument is of the wrong type
>                            \
> 
> > Comments? (esp. if anyone can see whether option (a) breaks somewhere)

It is not easy to "see" something like that. One needs to check, which is
very time consuming.  My crystal ball says that the chances of breakage are
over 50%.


	--michael  

> Ideally, we should specify E in suc a way that extensions (standard or 
> user-defined) of BLD could give it stronger semantics, e.g. 
> corresponding to options (a) or (b).
> 
> Christian

Received on Saturday, 12 January 2008 00:29:45 UTC