Re: model theory of error

> Michael Kifer wrote:
> > 
> > So, if it is a compliance clause, then we pushed the problem to the next level.
> > Does it mean that I can now go back to work on the document?
> 
> Yes, I think that the benefits and drawbacks of the three options are 
> clear enough and we should now make a decision.

Judging by what you wrote, I am afraid the options are still not clear.

Option (a) is easy to implement. Option (b) can be considered ONLY if
somebody volunteers at least 50 hours of work to check if this is sound.

Option (c) is **unsound** at the level of the model-theoretic semantics, so
it cannot be considered as an option.

If option (c) is considered at the level of compliance, then it is not an
alternative to (a) and (b) and cannot be considered as an option at the
same level. So, these are the real options:

Model theory:
   (0) Not give any semantics to builtins, and pretend that this is anon-issue.
   (a) The true/false option
   (b) The true/false/error option.
       Anybody who votes for this option should also commit at least 50
       work hours to checking it out.

Compliance:
   (c) Say something here informally (but hopefully something that makes
       some sense)
   (d) Not say anything and pretend this is not an issue.
   


	--michael



> I have no sense of where the WG is leaning, though?
> 
> *Sandro*, would it be possible to set up a quick WBS poll to see what 
> kind of resolution would have the best chances? As I understand it, the 
> options are:
> 
> a. Add a special constant, e.g. rif:error, and a distinguished elements 
> _|_ in the domain of interpretation of any semantic structure, such that 
> all semantic structures will be required to interpret rif:error as _|_; 
> define builtin functions so that they will return rif:error whenever 
> their arguments are of the wrong type; and say that a predicate, 
> p(a,b,c,...), is false if any of its arguments evaluates to _|_ in the 
> interpretation;
> 
> b. Same as (a) as regards builtin functions. 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 one of the args is _|_;
> 
> c. Support builtins (and evaluated functions and predicates in general) 
> syntactically, and semantically within their domains of definition, but 
> leave their semantics on error (and the semantics of predicates where 
> one arguments is an evaluated function with an out-of-domain argument) 
> implementation dependent.
> 
> Whether or not silent processing of such cases should be forbidden is a 
> different issue. It depends on how difficult that requirement would be 
> to implement, as I see it.
> 
> Christian
> 
>

Received on Thursday, 10 January 2008 20:11:32 UTC