Re: model theory of error

Michael Kifer wrote:
> Last Tuesday we were unable to resolve the issue of builtin functions
> because we could not decide on their semantics. The problem is that builtin
> functions are partial and are supposed to return an error if given wrong
> arguments.
>
> One approach we considered was to simulate them using predicates by
> translating functional expressions into formulas that involve builtin
> predicates. Unfortunately, this has a problem that occurrences of such
> functions in the conclusions of rules must have a different translation
> than the occurrences in rule premises. This was perceived as a problem if
> we were to consider BLD as a subset of the (future) first-order dialect,
> since the first-order dialect will not have such a distinction.
>
> I thought a bit about a direct model-theoretic semantics, and there is at
> least one solution that does not seem too complicated. Comments are welcome.
>
> 1. We need a special constant (not sure if it should be in rif:IRI or
>    in its own symbol space) of the form rif:error.
>
> 2. The domain of interpretation of any semantic structure will also have a
>    special distinguished element called _|_.
>
> 3. All semantic structures will be required to interpret rif:error as _|_
>    (i.e., I_const(rif:error) = _|_)
>
> 4. The builtin functions will be defined so that they will return rif:error
>    whenever their arguments are of the wrong type.
>   
This assumes all builtin functions to be total. Is that true? It might 
be a need to allow functions to throw errors even their arguments are 
appropriate i.e. to assume partial functions.
> 5. For predicates, we have two options.
>    a. The simplest option is to say that a predicate, p(a,b,c,...), is false if
>       any of its arguments evaluates to _|_ in the interpretation.
>   
This is the case when a predicate has an argument interpreted as error. 
This makes no distinction between false atoms with  wrong arguments and 
false atoms with proper arguments.
For example, I(succ(2)>26)=false as well as I(pred(0)>2)=false while in 
the second case pred(0) is interpreted as error. This is an example of a 
partial function which might be interpreted as _|_ even its arguments 
are not interpreted as errors.

I try one more example:  I("rif" >  23.3) should be false even if 
I('"rif")="Rule Interchange Format" and I(23.3)=23.3 i.e. the arguments 
are not interpreted to _|_

>    b. This option introduces a new truth value, called E (error) such that 
>       ~E = E, E/\F=F, E/\T=E, E\/F=E, E\/T=T. Then we can say that
>       p(a,b,c,...) has truth value E if at least of of the args is _|_.
>
>   The advantage of option (b) over option (a) is that we have an explicit
>   representation for errors. 
>   The disadvantage is that it is much more complicated. Many results need
>   to be ported to account for this new truth value, and I did not check
>   this carefully. Quite possible that this idea breaks somewhere.
>
>   I think option (b) is too much work for very little gain.
>   
I suppose that E/\E=E and E\/E=E.
If ~E=E then both the law of excluded middle and law of 
noncontradiction  does not  work.
In this case consider again,  I('"rif")="Rule Interchange Format" and 
I(23.3)=23.3 i.e. they are not interpreted in error, but I guess  
I("rif" >  23.3) should be E
>
> Comments? (esp. if anyone can see whether option (a) breaks somewhere)
>
>
> 	--michael  
>
>   
-Adrian Giurca

Received on Saturday, 5 January 2008 21:02:25 UTC